OAI/Combinatorics/StripMass/HoneycombTiles.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.ValidTriangle line 14
  2. lemma OAI.CriticalStrip.Diagram.ValidTriangle.not_three line 17
  3. lemma OAI.CriticalStrip.Diagram.ValidTriangle.one_off line 21
  4. lemma OAI.CriticalStrip.Diagram.ValidTriangle.of_not_three_not_one line 26
  5. def OAI.CriticalStrip.Diagram.Tile.middle line 36
  6. def OAI.CriticalStrip.Diagram.Tile.upperUsed line 40
  7. def OAI.CriticalStrip.Diagram.Tile.lowerUsed line 44
  8. lemma OAI.CriticalStrip.Diagram.Tile.physical_up line 48
  9. lemma OAI.CriticalStrip.Diagram.Tile.physical_down line 54
  10. lemma OAI.CriticalStrip.Diagram.Tile.upperUsed_iff line 60
  11. lemma OAI.CriticalStrip.Diagram.Tile.lowerUsed_iff line 65
  12. lemma OAI.CriticalStrip.Diagram.Tile.physical_ext line 70
  13. theorem OAI.CriticalStrip.Diagram.Tile.existsUnique_physical line 77
  14. lemma OAI.CriticalStrip.Diagram.Tile.physical_weight line 109
  15. abbrev OAI.CriticalStrip.Cell line 127
  16. def OAI.CriticalStrip.upDownWire line 131
  17. def OAI.CriticalStrip.tileGraph line 138
  18. lemma OAI.CriticalStrip.tileGraph_allowed line 145
  19. lemma OAI.CriticalStrip.tileGraph_middle line 156
  20. lemma OAI.CriticalStrip.tileGraph_west line 160
  21. lemma OAI.CriticalStrip.tileGraph_south line 164
  22. lemma OAI.CriticalStrip.tileGraph_up line 172
  23. structure OAI.CriticalStrip.HoneycombAssignment line 190
  24. def OAI.CriticalStrip.HoneycombAssignment.graph line 200
  25. lemma OAI.CriticalStrip.HoneycombAssignment.up_neighbors line 202
  26. lemma OAI.CriticalStrip.HoneycombAssignment.down_neighbors line 209
  27. lemma OAI.CriticalStrip.atMostTwo_of_three line 234
  28. lemma OAI.CriticalStrip.HoneycombAssignment.two line 246
  29. lemma OAI.CriticalStrip.HoneycombAssignment.bottom_one line 263
  30. lemma OAI.CriticalStrip.HoneycombAssignment.bottom_used line 272
  31. lemma OAI.CriticalStrip.HoneycombAssignment.top_one line 279
  32. lemma OAI.CriticalStrip.HoneycombAssignment.top_used line 290
  33. lemma OAI.CriticalStrip.validTriangle_of_neighbors line 307
  34. lemma OAI.CriticalStrip.validTriangle_with_port line 334
  35. inductive OAI.CriticalStrip.BoundaryPort line 362
  36. def OAI.CriticalStrip.BoundaryPort.vertex line 369
  37. lemma OAI.CriticalStrip.BoundaryPort.vertex_ne_source line 373
  38. lemma OAI.CriticalStrip.BoundaryPort.up_eq_iff line 379
  39. lemma OAI.CriticalStrip.BoundaryPort.down_eq_iff line 383
  40. def OAI.CriticalStrip.WireConfiguration.south line 392
  41. def OAI.CriticalStrip.WireConfiguration.west line 395
  42. def OAI.CriticalStrip.WireConfiguration.middle line 398
  43. def OAI.CriticalStrip.WireConfiguration.east line 401
  44. def OAI.CriticalStrip.WireConfiguration.north line 404
  45. lemma OAI.CriticalStrip.WireConfiguration.up_nonterminal line 407
  46. lemma OAI.CriticalStrip.WireConfiguration.down_nonterminal line 413
  47. lemma OAI.CriticalStrip.WireConfiguration.up_valid line 419
  48. lemma OAI.CriticalStrip.WireConfiguration.down_valid line 454
  49. lemma OAI.CriticalStrip.WireConfiguration.flags_outside line 496