OAI/Combinatorics/StripMass/ThreeBoxCertificates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.ThreeBox.rootTable line 15
  2. def OAI.CriticalStrip.Diagram.ThreeBox.parentTable line 113
  3. def OAI.CriticalStrip.Diagram.ThreeBox.rankTable line 211
  4. def OAI.CriticalStrip.Diagram.ThreeBox.ForestConditions line 309
  5. instance OAI.CriticalStrip.Diagram.ThreeBox.forestConditionsDecidable line 314
  6. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_0 line 317
  7. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_1 line 322
  8. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_2 line 327
  9. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_3 line 332
  10. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_4 line 337
  11. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_5 line 342
  12. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_6 line 347
  13. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_7 line 352
  14. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions_8 line 357
  15. theorem OAI.CriticalStrip.Diagram.ThreeBox.forestConditions line 362
  16. def OAI.CriticalStrip.Diagram.ThreeBox.certificate line 375
  17. theorem OAI.CriticalStrip.Diagram.ThreeBox.reach_iff_root_eq line 383