OAI/Combinatorics/StripMass/RibbonLocal.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.HoneycombBranch.slot line 15
  2. def OAI.CriticalStrip.HoneycombBranch.lane line 20
  3. def OAI.CriticalStrip.HoneycombBranch.localGauge line 23
  4. lemma OAI.CriticalStrip.HoneycombBranch.slot_injective line 26
  5. lemma OAI.CriticalStrip.HoneycombBranch.lane_injective line 30
  6. lemma OAI.CriticalStrip.HoneycombBranch.lane_cover line 40
  7. lemma OAI.CriticalStrip.HoneycombBranch.local_turn line 43
  8. def OAI.CriticalStrip.HoneycombBranch.passes line 58
  9. lemma OAI.CriticalStrip.HoneycombBranch.passes_nil line 62
  10. lemma OAI.CriticalStrip.HoneycombBranch.passes_cons line 63
  11. lemma OAI.CriticalStrip.HoneycombBranch.passes_vertices line 66
  12. lemma OAI.CriticalStrip.HoneycombBranch.passes_append line 72
  13. lemma OAI.CriticalStrip.HoneycombBranch.passes_shift line 78
  14. lemma OAI.CriticalStrip.HoneycombBranch.passes_mem_vertex line 87
  15. lemma OAI.CriticalStrip.HoneycombBranch.passes_ne line 92
  16. def OAI.CriticalStrip.HoneycombBranch.routes line 107
  17. lemma OAI.CriticalStrip.HoneycombBranch.mem_routes line 110
  18. lemma OAI.CriticalStrip.HoneycombBranch.routes_nil line 113
  19. lemma OAI.CriticalStrip.HoneycombBranch.routes_cons line 116
  20. lemma OAI.CriticalStrip.HoneycombBranch.routes_append line 123
  21. def OAI.CriticalStrip.HoneycombBranch.swapPass line 127
  22. lemma OAI.CriticalStrip.HoneycombBranch.passes_reverseTurns line 129
  23. lemma OAI.CriticalStrip.HoneycombBranch.routes_reverseTurns line 140
  24. lemma OAI.CriticalStrip.HoneycombBranch.routes_empty_of_notMem line 153
  25. lemma OAI.CriticalStrip.HoneycombBranch.routes_singleton_of_nodup line 159
  26. def OAI.CriticalStrip.HoneycombBranch.ribbonArcs line 175
  27. lemma OAI.CriticalStrip.HoneycombBranch.ribbonArcs_empty line 178
  28. lemma OAI.CriticalStrip.HoneycombBranch.ribbonArcs_union line 179
  29. lemma OAI.CriticalStrip.HoneycombBranch.ribbon_singleton line 182
  30. lemma OAI.CriticalStrip.HoneycombBranch.ribbon_double line 185
  31. lemma OAI.CriticalStrip.HoneycombBranch.ribbon_joint line 189
  32. def OAI.CriticalStrip.HoneycombBranch.RibbonSimple line 195
  33. lemma OAI.CriticalStrip.HoneycombBranch.ribbonSimple_of_nodup line 198
  34. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.Inside line 219
  35. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.vertex line 222
  36. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.vertex_inside line 224
  37. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.col line 231
  38. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.row line 232
  39. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.vertex_col_row line 234
  40. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.col_vertex line 242
  41. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.row_vertex line 246
  42. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.up line 253
  43. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.down line 254
  44. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.node line 256
  45. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.up_time line 259
  46. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.down_time line 264
  47. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.at_vertex line 272
  48. abbrev OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.start line 281
  49. abbrev OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.graph line 282
  50. abbrev OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.turnEdge line 283
  51. abbrev OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.boundary line 284
  52. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.arc_edge line 287
  53. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.arc_turn line 299
  54. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.Matches line 312
  55. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.interior_matches line 315
  56. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.physical_matches line 343
  57. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.node_eq line 356
  58. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.node_of_vertex line 360
  59. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.up_wire line 370
  60. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.wire line 424
  61. def OAI.CriticalStrip.HoneycombBranch.ribbon line 478
  62. lemma OAI.CriticalStrip.HoneycombBranch.ribbon_arc line 481
  63. lemma OAI.CriticalStrip.HoneycombBranch.ribbon_occupied line 490
  64. lemma OAI.CriticalStrip.HoneycombBranch.ribbon_incoming line 511
  65. lemma OAI.CriticalStrip.HoneycombBranch.ribbon_outgoing line 519
  66. lemma OAI.CriticalStrip.HoneycombBranch.route_shift_iff line 527
  67. lemma OAI.CriticalStrip.HoneycombBranch.neighbor_bool line 552
  68. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.route_interior_match line 559
  69. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.ribbon_matches line 573