OAI/Combinatorics/StripMass/TurnRectangleMatching.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.TurnRectangle.PhysicalMatches line 19
  2. lemma OAI.CriticalStrip.Diagram.TurnRectangle.physical_matches line 35
  3. lemma OAI.CriticalStrip.Diagram.TurnRectangle.compatible line 90
  4. def OAI.CriticalStrip.Diagram.TurnStarter.left line 104
  5. def OAI.CriticalStrip.Diagram.TurnStarter.right line 105
  6. lemma OAI.CriticalStrip.Diagram.TurnStarter.left_injective line 107
  7. lemma OAI.CriticalStrip.Diagram.TurnStarter.right_injective line 113
  8. lemma OAI.CriticalStrip.Diagram.TurnStarter.left_lt_right line 119
  9. lemma OAI.CriticalStrip.Diagram.TurnStarter.cover line 122
  10. def OAI.CriticalStrip.Diagram.TurnStarter.pairing line 135
  11. lemma OAI.CriticalStrip.Diagram.TurnStarter.adj_iff line 158
  12. lemma OAI.CriticalStrip.Diagram.TurnStarter.across line 171
  13. lemma OAI.CriticalStrip.Diagram.TurnStarter.occupied_left line 175
  14. lemma OAI.CriticalStrip.Diagram.TurnStarter.occupied_right line 185
  15. abbrev OAI.CriticalStrip.Diagram.TurnRectangle.edges line 209
  16. abbrev OAI.CriticalStrip.Diagram.TurnRectangle.turns line 210
  17. def OAI.CriticalStrip.Diagram.TurnRectangle.cellNode line 212
  18. lemma OAI.CriticalStrip.Diagram.TurnRectangle.local_edge line 215
  19. lemma OAI.CriticalStrip.Diagram.TurnRectangle.local_turn line 221
  20. lemma OAI.CriticalStrip.Diagram.TurnRectangle.up_edge line 228
  21. lemma OAI.CriticalStrip.Diagram.TurnRectangle.up_turn line 232
  22. lemma OAI.CriticalStrip.Diagram.TurnRectangle.down_edge line 237
  23. lemma OAI.CriticalStrip.Diagram.TurnRectangle.down_turn line 241
  24. lemma OAI.CriticalStrip.Diagram.TurnRectangle.diagonal_edge line 249
  25. lemma OAI.CriticalStrip.Diagram.TurnRectangle.diagonal_turn line 255
  26. lemma OAI.CriticalStrip.Diagram.TurnRectangle.enter_edge line 262
  27. lemma OAI.CriticalStrip.Diagram.TurnRectangle.enter_turn line 272
  28. lemma OAI.CriticalStrip.Diagram.TurnRectangle.vertical_edge line 284
  29. lemma OAI.CriticalStrip.Diagram.TurnRectangle.vertical_turn line 293
  30. lemma OAI.CriticalStrip.Diagram.TurnRectangle.horizontal_edge line 303
  31. lemma OAI.CriticalStrip.Diagram.TurnRectangle.horizontal_turn line 316
  32. def OAI.CriticalStrip.Diagram.TurnRectangle.southRay line 337
  33. def OAI.CriticalStrip.Diagram.TurnRectangle.westRay line 339
  34. lemma OAI.CriticalStrip.Diagram.TurnRectangle.southRay_div line 342
  35. lemma OAI.CriticalStrip.Diagram.TurnRectangle.southRay_mod line 344
  36. lemma OAI.CriticalStrip.Diagram.TurnRectangle.westRay_div line 346
  37. lemma OAI.CriticalStrip.Diagram.TurnRectangle.westRay_mod line 348
  38. lemma OAI.CriticalStrip.Diagram.TurnRectangle.ray_cover line 351
  39. def OAI.CriticalStrip.Diagram.TurnRectangle.starterActive line 370
  40. def OAI.CriticalStrip.Diagram.TurnRectangle.startPairing line 374
  41. lemma OAI.CriticalStrip.Diagram.TurnRectangle.active_south line 376
  42. lemma OAI.CriticalStrip.Diagram.TurnRectangle.active_west line 382
  43. lemma OAI.CriticalStrip.Diagram.TurnRectangle.southSlot_right line 387
  44. lemma OAI.CriticalStrip.Diagram.TurnRectangle.westSlot_right line 394
  45. lemma OAI.CriticalStrip.Diagram.TurnRectangle.start_matches_south line 402
  46. lemma OAI.CriticalStrip.Diagram.TurnRectangle.start_matches_west line 407
  47. def OAI.CriticalStrip.Diagram.TurnRectangle.InteriorMatches line 415
  48. lemma OAI.CriticalStrip.Diagram.TurnRectangle.starter_physical line 423
  49. lemma OAI.CriticalStrip.Diagram.TurnRectangle.starter_arc_turn line 429
  50. lemma OAI.CriticalStrip.Diagram.TurnRectangle.starter_edge line 441
  51. lemma OAI.CriticalStrip.Diagram.TurnRectangle.starter_turn line 448
  52. lemma OAI.CriticalStrip.Diagram.TurnRectangle.south_edge line 458
  53. lemma OAI.CriticalStrip.Diagram.TurnRectangle.south_turn line 470
  54. lemma OAI.CriticalStrip.Diagram.TurnRectangle.west_edge line 482
  55. lemma OAI.CriticalStrip.Diagram.TurnRectangle.west_turn line 499
  56. lemma OAI.CriticalStrip.Diagram.TurnDisk.edgeTurn_reverse line 524
  57. lemma OAI.CriticalStrip.Diagram.TurnNetwork.edgeTurn_reverse line 549