OAI/Combinatorics/StripMass/TurnDisk.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.BoundaryInsert.equiv line 16
  2. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.equiv_old line 28
  3. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.equiv_fresh line 30
  4. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.pairing_adj line 33
  5. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.pairing_old_adj line 40
  6. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.pairing_fresh_adj line 50
  7. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.pairing_cross_adj line 60
  8. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.pairing_old_occupied line 69
  9. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.pairing_fresh_occupied line 79
  10. def OAI.CriticalStrip.Diagram.BoundaryInsert.unionGraph line 90
  11. instance OAI.CriticalStrip.Diagram.BoundaryInsert.(instance at line 96) line 96
  12. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.reach_left line 104
  13. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.reach_right line 115
  14. def OAI.CriticalStrip.Diagram.BoundaryInsert.boundary line 126
  15. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.boundary_old line 129
  16. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.boundary_fresh line 135
  17. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.boundary_injective line 141
  18. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.realizes line 153
  19. def OAI.CriticalStrip.Diagram.BoundaryInsert.gauge line 201
  20. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.gauge_old line 204
  21. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.gauge_fresh line 208
  22. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.potential line 213
  23. lemma OAI.CriticalStrip.Diagram.GraphRealizes.restrict_boundary line 243
  24. abbrev OAI.CriticalStrip.Diagram.BoundaryErase.keep line 261
  25. abbrev OAI.CriticalStrip.Diagram.BoundaryErase.left line 262
  26. abbrev OAI.CriticalStrip.Diagram.BoundaryErase.right line 263
  27. lemma OAI.CriticalStrip.Diagram.BoundaryErase.adjacent line 265
  28. lemma OAI.CriticalStrip.Diagram.BoundaryErase.distinct line 269
  29. lemma OAI.CriticalStrip.Diagram.BoundaryErase.cover line 275
  30. lemma OAI.CriticalStrip.Diagram.BoundaryErase.occupied_cover line 283
  31. lemma OAI.CriticalStrip.Diagram.BoundaryErase.restrict_realizes line 291
  32. lemma OAI.CriticalStrip.Diagram.BoundaryErase.keep_ne_left line 297
  33. lemma OAI.CriticalStrip.Diagram.BoundaryErase.keep_ne_right line 299
  34. lemma OAI.CriticalStrip.Diagram.BoundaryErase.potential line 302
  35. def OAI.CriticalStrip.Diagram.BoundarySew.tile line 320
  36. lemma OAI.CriticalStrip.Diagram.BoundarySew.tile_no_outputs line 322
  37. lemma OAI.CriticalStrip.Diagram.BoundarySew.tile_inputs line 325
  38. lemma OAI.CriticalStrip.Diagram.BoundarySew.output_vacant line 329
  39. theorem OAI.CriticalStrip.Diagram.BoundarySew.transport line 344
  40. def OAI.CriticalStrip.Diagram.BoundarySew.graph line 418
  41. instance OAI.CriticalStrip.Diagram.BoundarySew.(instance at line 421) line 421
  42. def OAI.CriticalStrip.Diagram.BoundarySew.project line 428
  43. lemma OAI.CriticalStrip.Diagram.BoundarySew.project_edge line 435
  44. lemma OAI.CriticalStrip.Diagram.BoundarySew.include_edge line 460
  45. lemma OAI.CriticalStrip.Diagram.BoundarySew.used_port line 481
  46. def OAI.CriticalStrip.Diagram.BoundarySew.equivalence line 498
  47. theorem OAI.CriticalStrip.Diagram.BoundarySew.transport_direct line 547