OAI/Combinatorics/StripMass/NorthGluing.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_box line 12
  2. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_reflection line 28
  3. lemma OAI.CriticalStrip.Diagram.map_occupancySign line 39
  4. lemma OAI.CriticalStrip.Diagram.sourceGlue_signTwist line 45
  5. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_eval line 64
  6. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_parity line 77
  7. lemma OAI.CriticalStrip.Diagram.perm_reflect_ratio line 87
  8. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_reflected_covariance line 94
  9. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_exchange line 129
  10. def OAI.CriticalStrip.Diagram.northSeparatorMoment line 145
  11. lemma OAI.CriticalStrip.Diagram.sourceGlue_scale line 149
  12. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_eval_moment line 157
  13. lemma OAI.CriticalStrip.Diagram.Pairing.adj_interior line 177
  14. lemma OAI.CriticalStrip.Diagram.Pairing.fully_matched_interval_even line 195
  15. def OAI.CriticalStrip.Diagram.Pairing.shiftedVisitAdj line 215
  16. def OAI.CriticalStrip.Diagram.Pairing.visitWiring line 219
  17. lemma OAI.CriticalStrip.Diagram.Pairing.adj_closed_interval line 222
  18. lemma OAI.CriticalStrip.Diagram.Pairing.shiftedVisitAdj_closed_interval line 239
  19. lemma OAI.CriticalStrip.Diagram.Pairing.odd_initial_arc_impossible line 246
  20. theorem OAI.CriticalStrip.Diagram.Pairing.single_component_visits_consecutive line 273