OAI/Combinatorics/HoneycombChords/ChordSystems.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Chord systems for critical honeycomb strips.

The formulas follow the finite strip transfer calculation in the companion paper on uniform marked polygon estimates.

  1. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.first_edge line 15
  2. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.last_edge line 17
  3. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.source_selected line 20
  4. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.target_selected line 25
  5. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.sources_nodup line 31
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.length_le_width line 44
  7. def OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.code line 73
  8. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.spins_restrict line 75
  9. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.code_injective line 78
  10. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.boundaryChordFintype line 97
  11. def OAI.CriticalHoneycomb.Transfer.RasterGrid.EndPort line 100
  12. def OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord line 102
  13. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.hardChordFintype line 103
  14. def OAI.CriticalHoneycomb.Transfer.RasterGrid.singleSystemMass line 107
  15. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.endPort_of_selected line 109
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.hard_endpoints line 118
  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.endPort_inside_injective line 132
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord.trace_injective line 141
  19. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundaryChord_to_halfRect line 157
  20. def OAI.CriticalHoneycomb.Transfer.RasterGrid.bottomArchOf line 163
  21. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.bottomEnds_distinct line 167
  22. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.topTurn_involution line 171
  23. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.topTurn_trace line 174
  24. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.topTurn_north line 184
  25. def OAI.CriticalHoneycomb.Transfer.RasterGrid.topArchOf line 188
  26. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.topEnds_distinct line 193
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundaryChord_to_rect line 199
  28. def OAI.CriticalHoneycomb.Transfer.RasterGrid.upBridgeOf line 205
  29. def OAI.CriticalHoneycomb.Transfer.RasterGrid.downBridgeOf line 209
  30. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.ArchPool line 217
  31. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.BridgePool line 218
  32. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.OnePathPool line 219
  33. def OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord.encode line 221
  34. def OAI.CriticalHoneycomb.Transfer.RasterGrid.poolTrace line 240
  35. def OAI.CriticalHoneycomb.Transfer.RasterGrid.recoverTrace line 245
  36. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord.recover_encode line 250
  37. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord.encode_injective line 257
  38. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord.encode_length line 262
  39. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.archEndsFintype line 275
  40. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archPoolWeight line 281
  41. def OAI.CriticalHoneycomb.Transfer.RasterGrid.bridgePoolWeight line 282
  42. def OAI.CriticalHoneycomb.Transfer.RasterGrid.poolWeight line 283
  43. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archPoolMass line 284
  44. def OAI.CriticalHoneycomb.Transfer.RasterGrid.bridgePoolMass line 285
  45. def OAI.CriticalHoneycomb.Transfer.RasterGrid.poolMass line 286
  46. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archPool_summable line 288
  47. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.pool_hasSum line 293
  48. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.pool_summable line 302
  49. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.poolWeight_nonnegative line 304
  50. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.bridgePoolMass_eq line 306
  51. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.poolMass_eq line 309
  52. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.bridgePoolMass_limit line 313
  53. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.poolMass_limit line 318
  54. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.singleSystemMass_le line 323