OAI/Combinatorics/StripMass/TurnWideGate.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.old_val line 16
  2. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.fresh_val line 18
  3. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.boundary_before line 21
  4. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.boundary_between line 30
  5. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.boundary_after line 39
  6. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.gauge_before line 49
  7. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.gauge_between line 58
  8. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.gauge_after line 67
  9. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.used_left line 77
  10. lemma OAI.CriticalStrip.Diagram.BoundaryInsert.used_right line 87
  11. lemma OAI.CriticalStrip.Diagram.BoundarySew.used_iff line 99
  12. lemma OAI.CriticalStrip.Diagram.TurnDisk.sew_used line 114
  13. def OAI.CriticalStrip.Diagram.TurnDisk.vertexGauge line 122
  14. lemma OAI.CriticalStrip.Diagram.TurnDisk.vertexGauge_boundary line 128
  15. def OAI.CriticalStrip.Diagram.TurnDisk.gate4 line 150
  16. def OAI.CriticalStrip.Diagram.TurnDisk.Gate4.skip line 156
  17. def OAI.CriticalStrip.Diagram.TurnDisk.Gate4.input line 158
  18. def OAI.CriticalStrip.Diagram.TurnDisk.Gate4.output line 159
  19. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.finite_four_or line 161
  20. abbrev OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage0 line 180
  21. abbrev OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage1 line 181
  22. abbrev OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage2 line 182
  23. abbrev OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage3 line 183
  24. def OAI.CriticalStrip.Diagram.TurnDisk.Gate4.slot line 185
  25. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage1_left line 187
  26. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage1_right line 192
  27. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage2_left line 201
  28. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage2_right line 213
  29. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage3_left line 228
  30. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage3_right line 241
  31. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage4_left line 257
  32. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage4_right line 271
  33. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.boundary_slot line 288
  34. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.boundary_outside line 306
  35. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.gauge_slot line 332
  36. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.gauge_outside line 336
  37. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.match1 line 345
  38. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage1_used line 355
  39. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.match2 line 359
  40. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage2_used line 369
  41. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.match3 line 373
  42. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.stage3_used line 383
  43. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.match4 line 387
  44. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.used line 397
  45. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.compatible line 401
  46. def OAI.CriticalStrip.Diagram.TurnDisk.Gate4.wire line 432
  47. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.wiring line 436