OAI/Combinatorics/StripMass/ThreeBoxSplitPolynomial.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.ThreeBox.deletionTile line 14
  2. def OAI.CriticalStrip.Diagram.ThreeBox.swapTile line 18
  3. def OAI.CriticalStrip.Diagram.ThreeBox.mergeNumerator line 22
  4. def OAI.CriticalStrip.Diagram.ThreeBox.commonNumerator line 27
  5. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_0 line 30
  6. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_14 line 37
  7. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_22 line 44
  8. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_23 line 53
  9. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_27 line 60
  10. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_30 line 69
  11. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_48 line 78
  12. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_49 line 87
  13. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator_50 line 94
  14. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_0 line 103
  15. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_1 line 110
  16. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_7 line 119
  17. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_8 line 128
  18. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_9 line 137
  19. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_14 line 146
  20. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_17 line 155
  21. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_19 line 162
  22. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_22 line 171
  23. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_23 line 180
  24. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_25 line 189
  25. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_27 line 198
  26. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_30 line 207
  27. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_35 line 216
  28. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_38 line 225
  29. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_39 line 232
  30. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_41 line 241
  31. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_42 line 250
  32. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_48 line 259
  33. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_49 line 268
  34. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator_50 line 277
  35. def OAI.CriticalStrip.Diagram.ThreeBox.diagramExterior line 295
  36. theorem OAI.CriticalStrip.Diagram.ThreeBox.realizes_boundary_reach line 299
  37. theorem OAI.CriticalStrip.Diagram.ThreeBox.realizes_compressed line 309
  38. theorem OAI.CriticalStrip.Diagram.ThreeBox.substitute_reach line 316
  39. theorem OAI.CriticalStrip.Diagram.ThreeBox.substitute_drains line 323
  40. theorem OAI.CriticalStrip.Diagram.ThreeBox.profile_exists_of_drains line 336
  41. def OAI.CriticalStrip.Diagram.ThreeBox.exteriorTest line 356
  42. def OAI.CriticalStrip.Diagram.ThreeBox.patchTest line 363
  43. theorem OAI.CriticalStrip.Diagram.ThreeBox.patchTest_iff line 370