OAI/Combinatorics/StripMass/TurnShelling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.Graph.reach_before_sewing line 16
  2. lemma OAI.CriticalStrip.Diagram.Graph.drains_before_sewing line 29
  3. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.drains_old line 44
  4. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.drains_fresh line 58
  5. inductive OAI.CriticalStrip.Diagram.TurnDisk line 77
  6. def OAI.CriticalStrip.Diagram.TurnDisk.Vertex line 88
  7. def OAI.CriticalStrip.Diagram.TurnDisk.boundary line 94
  8. def OAI.CriticalStrip.Diagram.TurnDisk.gauge line 100
  9. def OAI.CriticalStrip.Diagram.TurnDisk.wiring line 106
  10. instance OAI.CriticalStrip.Diagram.TurnDisk.(instance at line 114) line 114
  11. def OAI.CriticalStrip.Diagram.TurnDisk.Compatible line 129
  12. def OAI.CriticalStrip.Diagram.TurnDisk.edgeTurn line 139
  13. lemma OAI.CriticalStrip.Diagram.TurnDisk.boundary_injective line 151
  14. theorem OAI.CriticalStrip.Diagram.TurnDisk.potential line 160