OAI/Combinatorics/StripMass/ThreeBoxWeights.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.ThreeBox.fiber line 15
  2. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_0 line 68
  3. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_1 line 72
  4. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_2 line 76
  5. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_3 line 80
  6. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_4 line 84
  7. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_5 line 88
  8. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_6 line 92
  9. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_7 line 96
  10. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_8 line 100
  11. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_9 line 104
  12. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_10 line 108
  13. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_11 line 112
  14. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_12 line 116
  15. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_13 line 120
  16. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_14 line 124
  17. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_15 line 128
  18. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_16 line 132
  19. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_17 line 136
  20. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_18 line 140
  21. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_19 line 144
  22. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_20 line 148
  23. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_21 line 152
  24. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_22 line 156
  25. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_23 line 160
  26. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_24 line 164
  27. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_25 line 168
  28. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_26 line 172
  29. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_27 line 176
  30. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_28 line 180
  31. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_29 line 184
  32. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_30 line 188
  33. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_31 line 192
  34. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_32 line 196
  35. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_33 line 200
  36. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_34 line 204
  37. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_35 line 208
  38. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_36 line 212
  39. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_37 line 216
  40. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_38 line 220
  41. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_39 line 224
  42. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_40 line 228
  43. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_41 line 232
  44. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_42 line 236
  45. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_43 line 240
  46. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_44 line 244
  47. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_45 line 248
  48. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_46 line 252
  49. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_47 line 256
  50. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_48 line 260
  51. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_49 line 264
  52. theorem OAI.CriticalStrip.Diagram.ThreeBox.fiber_correct_50 line 268
  53. theorem OAI.CriticalStrip.Diagram.ThreeBox.mem_fiber_iff line 272
  54. def OAI.CriticalStrip.Diagram.ThreeBox.coefficient line 326
  55. def OAI.CriticalStrip.Diagram.ThreeBox.literalCoefficient line 329
  56. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_eq_literal line 333
  57. def OAI.CriticalStrip.Diagram.ThreeBox.mirrorIndex line 341
  58. theorem OAI.CriticalStrip.Diagram.ThreeBox.mirrorIndex_involutive line 343
  59. def OAI.CriticalStrip.Diagram.ThreeBox.reverseSlots line 347
  60. theorem OAI.CriticalStrip.Diagram.ThreeBox.diagram_mirror line 349
  61. def OAI.CriticalStrip.Diagram.ThreeBox.tileNumerator line 356
  62. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_0 line 364
  63. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_1 line 368
  64. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_2 line 372
  65. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_3 line 376
  66. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_4 line 380
  67. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_5 line 384
  68. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_6 line 388
  69. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_7 line 392
  70. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_8 line 396
  71. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_9 line 400
  72. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_10 line 404
  73. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_11 line 408
  74. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_12 line 412
  75. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_13 line 416
  76. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_14 line 420
  77. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_15 line 424
  78. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_16 line 428
  79. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_17 line 432
  80. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_18 line 436
  81. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_19 line 440
  82. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_20 line 444
  83. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_21 line 448
  84. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_22 line 452
  85. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_23 line 456
  86. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_24 line 460
  87. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_25 line 464
  88. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_26 line 468
  89. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_27 line 472
  90. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_28 line 476
  91. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_29 line 480
  92. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_30 line 484
  93. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_31 line 488
  94. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_32 line 492
  95. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_33 line 496
  96. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_34 line 500
  97. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_35 line 504
  98. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_36 line 508
  99. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_37 line 512
  100. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_38 line 516
  101. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_39 line 520
  102. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_40 line 524
  103. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_41 line 528
  104. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_42 line 532
  105. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_43 line 536
  106. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_44 line 540
  107. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_45 line 544
  108. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_46 line 548
  109. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_47 line 552
  110. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_48 line 556
  111. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_49 line 560
  112. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_50 line 564