OAI/Combinatorics/StripMass/ThreeBoxProfiles.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.ThreeBox.diagram line 16
  2. def OAI.CriticalStrip.Diagram.ThreeBox.profile line 69
  3. def OAI.CriticalStrip.Diagram.ThreeBox.Clean line 159
  4. def OAI.CriticalStrip.Diagram.ThreeBox.BoundaryData line 162
  5. instance OAI.CriticalStrip.Diagram.ThreeBox.cleanDecidable line 166
  6. instance OAI.CriticalStrip.Diagram.ThreeBox.boundaryAdjDecidable line 168
  7. instance OAI.CriticalStrip.Diagram.ThreeBox.boundarySupportDecidable line 170
  8. instance OAI.CriticalStrip.Diagram.ThreeBox.boundaryDataDecidable line 172
  9. def OAI.CriticalStrip.Diagram.ThreeBox.ProfileCorrect line 175
  10. instance OAI.CriticalStrip.Diagram.ThreeBox.profileCorrectDecidable line 179
  11. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_0 line 182
  12. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_1 line 185
  13. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_2 line 188
  14. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_3 line 191
  15. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_4 line 194
  16. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_5 line 197
  17. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_6 line 200
  18. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_7 line 203
  19. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect_8 line 206
  20. theorem OAI.CriticalStrip.Diagram.ThreeBox.profileCorrect line 209
  21. theorem OAI.CriticalStrip.Diagram.ThreeBox.diagram_injective line 222
  22. theorem OAI.CriticalStrip.Diagram.ThreeBox.diagram_upper line 224
  23. theorem OAI.CriticalStrip.Diagram.ThreeBox.realizes_iff_conditions line 227
  24. theorem OAI.CriticalStrip.Diagram.ThreeBox.realizes_unique line 245
  25. theorem OAI.CriticalStrip.Diagram.ThreeBox.profile_some_iff line 268