OAI/Combinatorics/StripMass/TurnGate.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.Pairing.gateTurn line 17
  2. lemma OAI.CriticalStrip.Diagram.Pairing.gateTurn_reverse line 23
  3. lemma OAI.CriticalStrip.Diagram.Pairing.cap_arcTurn_general line 27
  4. lemma OAI.CriticalStrip.Diagram.Pairing.arcTurn_congr line 35
  5. lemma OAI.CriticalStrip.Diagram.Pairing.turnOrder_embedding line 39
  6. structure OAI.CriticalStrip.Diagram.Pairing.GatePotentials line 44
  7. def OAI.CriticalStrip.Diagram.Pairing.gateBoundary line 56
  8. lemma OAI.CriticalStrip.Diagram.Pairing.gateBoundary_left line 59
  9. lemma OAI.CriticalStrip.Diagram.Pairing.gateBoundary_right line 61
  10. lemma OAI.CriticalStrip.Diagram.Pairing.gateBoundary_other line 64
  11. lemma OAI.CriticalStrip.Diagram.Pairing.gatePotentials_vacant line 68
  12. lemma OAI.CriticalStrip.Diagram.Pairing.gatePotentials_through line 84
  13. lemma OAI.CriticalStrip.Diagram.Pairing.gatePotentials_cup line 114
  14. lemma OAI.CriticalStrip.Diagram.Pairing.gatePotentials_swap line 141
  15. lemma OAI.CriticalStrip.Diagram.Pairing.gatePotentials_cap_general line 176
  16. theorem OAI.CriticalStrip.Diagram.Pairing.gatePotentials_of_step line 247
  17. theorem OAI.CriticalStrip.Diagram.CompactGate.transport_potential line 332
  18. inductive OAI.CriticalStrip.Diagram.Circuit.TurnGauges line 364
  19. def OAI.CriticalStrip.Diagram.Circuit.TurnGauges.final line 371
  20. def OAI.CriticalStrip.Diagram.Circuit.TurnGauges.Compatible line 375
  21. def OAI.CriticalStrip.Diagram.Circuit.TurnGauges.edgeTurn line 381
  22. theorem OAI.CriticalStrip.Diagram.Circuit.TurnGauges.potential line 391
  23. def OAI.CriticalStrip.Diagram.BoundaryInsert.old line 451
  24. def OAI.CriticalStrip.Diagram.BoundaryInsert.fresh line 457
  25. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.disjoint line 462
  26. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.cover line 468
  27. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.not_cross line 491
  28. def OAI.CriticalStrip.Diagram.BoundaryInsert.pairing line 500