OAI/Combinatorics/StripMass/TurnEvolution.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.TurnNetwork.lift line 17
  2. lemma OAI.CriticalStrip.Diagram.TurnNetwork.lift_refl line 21
  3. lemma OAI.CriticalStrip.Diagram.TurnNetwork.lift_trans line 23
  4. lemma OAI.CriticalStrip.Diagram.TurnNetwork.lift_old line 26
  5. lemma OAI.CriticalStrip.Diagram.TurnNetwork.old_eq_lift line 29
  6. lemma OAI.CriticalStrip.Diagram.TurnNetwork.lift_injective line 31
  7. lemma OAI.CriticalStrip.Diagram.TurnNetwork.lift_edge line 44
  8. lemma OAI.CriticalStrip.Diagram.TurnNetwork.lift_turn line 51
  9. lemma OAI.CriticalStrip.Diagram.TurnNetwork.boundary_untouched line 60
  10. lemma OAI.CriticalStrip.Diagram.TurnNetwork.boundary_last line 69
  11. lemma OAI.CriticalStrip.Diagram.TurnNetwork.gauge_untouched line 78
  12. lemma OAI.CriticalStrip.Diagram.TurnNetwork.gauge_slot line 88
  13. def OAI.CriticalStrip.Diagram.TurnNetwork.namedGauge line 95
  14. lemma OAI.CriticalStrip.Diagram.TurnNetwork.namedGauge_old line 100
  15. lemma OAI.CriticalStrip.Diagram.TurnNetwork.namedGauge_lift line 102
  16. lemma OAI.CriticalStrip.Diagram.TurnNetwork.namedGauge_vertex line 105
  17. lemma OAI.CriticalStrip.Diagram.TurnNetwork.namedGauge_boundary line 115
  18. def OAI.CriticalStrip.Diagram.TurnNetwork.Matches line 121
  19. lemma OAI.CriticalStrip.Diagram.TurnNetwork.Matches.mono line 127
  20. lemma OAI.CriticalStrip.Diagram.TurnNetwork.occupied_iff_used line 131
  21. lemma OAI.CriticalStrip.Diagram.TurnNetwork.gate_matches line 163
  22. lemma OAI.CriticalStrip.Diagram.TurnNetwork.compatible line 176
  23. lemma OAI.CriticalStrip.Diagram.TurnNetwork.wire_edge line 191
  24. def OAI.CriticalStrip.Diagram.TurnRectangle.width line 217
  25. def OAI.CriticalStrip.Diagram.TurnRectangle.ports line 218
  26. def OAI.CriticalStrip.Diagram.TurnRectangle.position line 221
  27. lemma OAI.CriticalStrip.Diagram.TurnRectangle.position_bound line 223
  28. lemma OAI.CriticalStrip.Diagram.TurnRectangle.position_time line 229
  29. lemma OAI.CriticalStrip.Diagram.TurnRectangle.time_lt line 236
  30. abbrev OAI.CriticalStrip.Diagram.TurnRectangle.box line 245
  31. abbrev OAI.CriticalStrip.Diagram.TurnRectangle.bdry line 246
  32. def OAI.CriticalStrip.Diagram.TurnRectangle.southSlot line 248
  33. def OAI.CriticalStrip.Diagram.TurnRectangle.westSlot line 250
  34. lemma OAI.CriticalStrip.Diagram.TurnRectangle.southSlot_val line 253
  35. lemma OAI.CriticalStrip.Diagram.TurnRectangle.westSlot_val line 257
  36. lemma OAI.CriticalStrip.Diagram.TurnRectangle.south_initial_untouched line 264
  37. lemma OAI.CriticalStrip.Diagram.TurnRectangle.west_initial_untouched line 271
  38. lemma OAI.CriticalStrip.Diagram.TurnRectangle.west_previous_untouched line 280
  39. lemma OAI.CriticalStrip.Diagram.TurnRectangle.south_initial line 310
  40. lemma OAI.CriticalStrip.Diagram.TurnRectangle.west_initial line 319
  41. lemma OAI.CriticalStrip.Diagram.TurnRectangle.south_previous line 327
  42. lemma OAI.CriticalStrip.Diagram.TurnRectangle.west_previous line 341
  43. lemma OAI.CriticalStrip.Diagram.TurnRectangle.retained_boundary line 375
  44. def OAI.CriticalStrip.Diagram.TurnRectangle.eastSlot line 383
  45. def OAI.CriticalStrip.Diagram.TurnRectangle.northSlot line 385
  46. lemma OAI.CriticalStrip.Diagram.TurnRectangle.eastSlot_val line 388
  47. lemma OAI.CriticalStrip.Diagram.TurnRectangle.northSlot_val line 393
  48. lemma OAI.CriticalStrip.Diagram.TurnRectangle.east_untouched line 400
  49. lemma OAI.CriticalStrip.Diagram.TurnRectangle.north_untouched line 412
  50. lemma OAI.CriticalStrip.Diagram.TurnRectangle.east_boundary line 425
  51. lemma OAI.CriticalStrip.Diagram.TurnRectangle.north_boundary line 432
  52. def OAI.CriticalStrip.Diagram.TurnRectangle.starterGauge line 449
  53. lemma OAI.CriticalStrip.Diagram.TurnRectangle.starterGauge_south line 454
  54. lemma OAI.CriticalStrip.Diagram.TurnRectangle.starterGauge_west line 460
  55. lemma OAI.CriticalStrip.Diagram.TurnRectangle.south_gauge line 468
  56. lemma OAI.CriticalStrip.Diagram.TurnRectangle.west_gauge line 484
  57. lemma OAI.CriticalStrip.Diagram.TurnRectangle.input_gauge line 502
  58. lemma OAI.CriticalStrip.Diagram.TurnRectangle.input_gauge_all line 514