OAI/Combinatorics/StripMass/TurnRhombus.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.TurnDisk.sew_edge line 15
  2. lemma OAI.CriticalStrip.Diagram.TurnDisk.sew_edgeTurn line 17
  3. lemma OAI.CriticalStrip.Diagram.TurnDisk.sew_zeroTurn line 21
  4. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.old_edge line 28
  5. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.new_edge line 31
  6. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.old_edgeTurn line 34
  7. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.new_edgeTurn line 42
  8. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.cross_edgeTurn line 50
  9. lemma OAI.CriticalStrip.Diagram.TurnDisk.Gate4.cross_edgeTurn_reverse line 53
  10. def OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.upGauge line 62
  11. def OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.downGauge line 63
  12. def OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.disk line 65
  13. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.boundary_left line 70
  14. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.boundary_right line 82
  15. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.input_boundary line 99
  16. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.output_boundary line 101
  17. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.gauge_input line 104
  18. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.gauge_output line 109
  19. abbrev OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.stage line 115
  20. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.first_left line 116
  21. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.first_right line 118
  22. abbrev OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.joined line 120
  23. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.second_left line 121
  24. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.second_right line 125
  25. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.match1 line 132
  26. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.stage_used line 139
  27. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.match2 line 142
  28. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.used line 151
  29. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.compatible line 154
  30. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.wiring line 163
  31. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.up_edge line 181
  32. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.down_edge line 183
  33. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.up_turn line 185
  34. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.down_turn line 191
  35. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.cross_turn line 197
  36. lemma OAI.CriticalStrip.Diagram.TurnDisk.Rhombus.cross_turn_reverse line 199
  37. abbrev OAI.CriticalStrip.Diagram.TurnNetwork.Local line 211
  38. abbrev OAI.CriticalStrip.Diagram.TurnNetwork.Node line 212
  39. def OAI.CriticalStrip.Diagram.TurnNetwork.old line 214
  40. def OAI.CriticalStrip.Diagram.TurnNetwork.fresh line 217
  41. lemma OAI.CriticalStrip.Diagram.TurnNetwork.old_injective line 219
  42. lemma OAI.CriticalStrip.Diagram.TurnNetwork.fresh_injective line 228
  43. lemma OAI.CriticalStrip.Diagram.TurnNetwork.old_ne_fresh line 231
  44. lemma OAI.CriticalStrip.Diagram.TurnNetwork.cover line 241
  45. def OAI.CriticalStrip.Diagram.TurnNetwork.disk line 258
  46. def OAI.CriticalStrip.Diagram.TurnNetwork.names line 264
  47. lemma OAI.CriticalStrip.Diagram.TurnNetwork.names_old line 286
  48. lemma OAI.CriticalStrip.Diagram.TurnNetwork.names_fresh line 288
  49. lemma OAI.CriticalStrip.Diagram.TurnNetwork.inv_old line 290
  50. lemma OAI.CriticalStrip.Diagram.TurnNetwork.inv_fresh line 294
  51. def OAI.CriticalStrip.Diagram.TurnNetwork.graph line 299
  52. def OAI.CriticalStrip.Diagram.TurnNetwork.edgeTurn line 302
  53. def OAI.CriticalStrip.Diagram.TurnNetwork.boundary line 305
  54. instance OAI.CriticalStrip.Diagram.TurnNetwork.(instance at line 308) line 308
  55. lemma OAI.CriticalStrip.Diagram.TurnNetwork.boundary_zero line 310
  56. lemma OAI.CriticalStrip.Diagram.TurnNetwork.boundary_slot line 311
  57. lemma OAI.CriticalStrip.Diagram.TurnNetwork.boundary_outside line 319
  58. lemma OAI.CriticalStrip.Diagram.TurnNetwork.old_edge line 327
  59. lemma OAI.CriticalStrip.Diagram.TurnNetwork.old_turn line 332
  60. lemma OAI.CriticalStrip.Diagram.TurnNetwork.fresh_edge line 337
  61. lemma OAI.CriticalStrip.Diagram.TurnNetwork.fresh_turn line 342
  62. lemma OAI.CriticalStrip.Diagram.TurnNetwork.wire_turn line 347
  63. lemma OAI.CriticalStrip.Diagram.TurnNetwork.wire_turn_reverse line 352
  64. def OAI.CriticalStrip.Diagram.TurnNetwork.Occupied line 360
  65. lemma OAI.CriticalStrip.Diagram.TurnNetwork.occupied_old line 366
  66. lemma OAI.CriticalStrip.Diagram.TurnNetwork.occupied_fresh line 370
  67. lemma OAI.CriticalStrip.Diagram.TurnNetwork.used_equiv line 376
  68. theorem OAI.CriticalStrip.Diagram.TurnNetwork.potential line 387