OAI/Combinatorics/StripMass/RibbonWalk.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.route_reach line 19
  2. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.last_inside line 56
  3. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.route_turn line 64
  4. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.node_occupied line 115
  5. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.cover_node line 127
  6. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.starter_drains line 151
  7. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.ribbon_drains line 166
  8. def OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottomIndex line 195
  9. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottomIndex_val line 198
  10. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottomIndex_lt line 205
  11. abbrev OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.gauge line 212
  12. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottom_boundary line 215
  13. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottom_gauge line 219
  14. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.top_boundary line 230
  15. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.top_gauge line 236
  16. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottom_connector line 247
  17. lemma OAI.CriticalStrip.HoneycombBranch.last_pass line 285
  18. lemma OAI.CriticalStrip.HoneycombBranch.first_occupied line 299
  19. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.endpoint_turn line 308
  20. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottom_outside line 343
  21. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.bottom_turn line 348
  22. def OAI.CriticalStrip.HoneycombBranch.closeStem line 395
  23. lemma OAI.CriticalStrip.HoneycombBranch.closeStem_depart line 398
  24. lemma OAI.CriticalStrip.HoneycombBranch.closeStem_terminal line 407
  25. lemma OAI.CriticalStrip.HoneycombBranch.closeStem_routes line 413
  26. lemma OAI.CriticalStrip.HoneycombBranch.closeStem_simple line 432
  27. lemma OAI.CriticalStrip.HoneycombBranch.closeStem_visits line 464
  28. lemma OAI.CriticalStrip.HoneycombBranch.closeStem_turn line 475