OAI/Combinatorics/StripMass/CollisionLeaf.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.HoneycombBranch.lastVisited_mem line 14
  2. lemma OAI.CriticalStrip.HoneycombBranch.exists_split_visit line 23
  3. lemma OAI.CriticalStrip.HoneycombBranch.collision_port_not_first line 36
  4. lemma OAI.CriticalStrip.HoneycombBranch.collision_port_not_stem line 59
  5. lemma OAI.CriticalStrip.HoneycombBranch.collision_index_eq line 79
  6. def OAI.CriticalStrip.HoneycombBranch.collisionIndex line 90
  7. def OAI.CriticalStrip.HoneycombBranch.collisionReverse line 93
  8. lemma OAI.CriticalStrip.HoneycombBranch.collisionReverse_split line 96
  9. lemma OAI.CriticalStrip.HoneycombBranch.collision_split line 104
  10. lemma OAI.CriticalStrip.HoneycombBranch.collisionReverse_mem line 114
  11. lemma OAI.CriticalStrip.HoneycombBranch.collisionReverse_involutive line 132
  12. lemma OAI.CriticalStrip.HoneycombBranch.collisionReverse_weight line 146
  13. theorem OAI.CriticalStrip.HoneycombBranch.collisionMass_zero_of_turns line 160
  14. def OAI.CriticalStrip.Diagram.Pairing.turnOrder line 210
  15. def OAI.CriticalStrip.Diagram.Pairing.arcTurn line 213
  16. lemma OAI.CriticalStrip.Diagram.Pairing.turnOrder_self line 216
  17. lemma OAI.CriticalStrip.Diagram.Pairing.turnOrder_reverse line 219
  18. lemma OAI.CriticalStrip.Diagram.Pairing.arcTurn_reverse line 223
  19. def OAI.CriticalStrip.Diagram.Pairing.turnPotential line 230
  20. lemma OAI.CriticalStrip.Diagram.Pairing.turnPotential_of_adj line 233
  21. lemma OAI.CriticalStrip.Diagram.Pairing.cap_partner_orders line 246
  22. lemma OAI.CriticalStrip.Diagram.Pairing.cap_turn_order line 256
  23. lemma OAI.CriticalStrip.Diagram.Pairing.cap_arcTurn line 266
  24. lemma OAI.CriticalStrip.Diagram.Pairing.cap_loop_turn line 276
  25. def OAI.CriticalStrip.Diagram.Pairing.swapGauge line 285
  26. lemma OAI.CriticalStrip.Diagram.Pairing.swapGauge_left line 288
  27. lemma OAI.CriticalStrip.Diagram.Pairing.swapGauge_right line 290
  28. lemma OAI.CriticalStrip.Diagram.Pairing.swapGauge_other line 292
  29. lemma OAI.CriticalStrip.Diagram.Pairing.cup_arcTurn line 296
  30. lemma OAI.CriticalStrip.Diagram.Pairing.adjacent_turnOrder line 303
  31. lemma OAI.CriticalStrip.Diagram.Pairing.diagonal_lower_arcTurn line 308
  32. lemma OAI.CriticalStrip.Diagram.Pairing.diagonal_upper_arcTurn line 316
  33. lemma OAI.CriticalStrip.Diagram.Pairing.vertical_lower_arcTurn line 324
  34. lemma OAI.CriticalStrip.Diagram.Pairing.vertical_upper_arcTurn line 330
  35. def OAI.CriticalStrip.Diagram.Graph.boundaryConstant line 350
  36. lemma OAI.CriticalStrip.Diagram.Graph.boundaryConstant_eq line 353
  37. lemma OAI.CriticalStrip.Diagram.Graph.boundaryConstant_boundary line 362
  38. lemma OAI.CriticalStrip.Diagram.Graph.boundaryConstant_edge line 367
  39. lemma OAI.CriticalStrip.Diagram.Graph.renormalize_potential line 376