OAI/Combinatorics/HoneycombChords/ReflectionEquation.lean

GitHub source file

205 declarations, 0 contain sorry, 0 declared as axioms

Polynomial matrix verification of the two-boundary reflection equation.

The specialization at a sixteenth root of minus one gives the honeycomb reflection identity in the finite strip transfer calculation.

  1. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Pair line 17
  2. def OAI.CriticalHoneycomb.Transfer.Reflection.rNumerator line 18
  3. def OAI.CriticalHoneycomb.Transfer.Reflection.dConstant line 46
  4. def OAI.CriticalHoneycomb.Transfer.Reflection.dLinear line 48
  5. def OAI.CriticalHoneycomb.Transfer.Reflection.slot1 line 50
  6. def OAI.CriticalHoneycomb.Transfer.Reflection.slot2 line 52
  7. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionLeft0 line 54
  8. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionRight0 line 56
  9. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionLeft1 line 58
  10. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionRight1 line 61
  11. def OAI.CriticalHoneycomb.Transfer.Reflection.dValue line 64
  12. lemma OAI.CriticalHoneycomb.Transfer.Reflection.mul_slot1_constant line 66
  13. lemma OAI.CriticalHoneycomb.Transfer.Reflection.mul_slot2_constant line 70
  14. lemma OAI.CriticalHoneycomb.Transfer.Reflection.slot2_constant_mul line 74
  15. lemma OAI.CriticalHoneycomb.Transfer.Reflection.mul_slot1_linear line 78
  16. lemma OAI.CriticalHoneycomb.Transfer.Reflection.mul_slot2_linear line 85
  17. lemma OAI.CriticalHoneycomb.Transfer.Reflection.slot2_linear_mul line 92
  18. lemma OAI.CriticalHoneycomb.Transfer.Reflection.core0_apply line 99
  19. lemma OAI.CriticalHoneycomb.Transfer.Reflection.core1_apply line 103
  20. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionFinThreeTwo line 109
  21. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.reflectionAdd line 110
  22. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.reflectionMul line 111
  23. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.reflectionPow line 112
  24. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00000 line 117
  25. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00001 line 124
  26. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00002 line 130
  27. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00010 line 136
  28. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00011 line 142
  29. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00012 line 148
  30. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00020 line 154
  31. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00021 line 160
  32. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00022 line 166
  33. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00100 line 172
  34. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00101 line 178
  35. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00102 line 185
  36. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00110 line 191
  37. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00111 line 198
  38. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00112 line 204
  39. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00120 line 210
  40. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00121 line 216
  41. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00122 line 222
  42. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00200 line 228
  43. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00201 line 234
  44. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00202 line 240
  45. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00210 line 247
  46. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate00211 line 252
  47. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00211 line 254
  48. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00212 line 263
  49. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00220 line 269
  50. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00221 line 276
  51. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent00222 line 282
  52. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01000 line 288
  53. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01001 line 294
  54. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01002 line 301
  55. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01010 line 307
  56. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01011 line 314
  57. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01012 line 320
  58. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01020 line 326
  59. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01021 line 332
  60. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01022 line 338
  61. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01100 line 344
  62. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01101 line 350
  63. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate01102 line 355
  64. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01102 line 357
  65. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01110 line 366
  66. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01111 line 372
  67. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01112 line 379
  68. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate01120 line 384
  69. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01120 line 386
  70. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01121 line 395
  71. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01122 line 401
  72. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01200 line 407
  73. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01201 line 413
  74. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01202 line 419
  75. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01210 line 425
  76. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01211 line 431
  77. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01212 line 437
  78. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01220 line 444
  79. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01221 line 450
  80. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent01222 line 457
  81. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02000 line 463
  82. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02001 line 469
  83. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02002 line 475
  84. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02010 line 482
  85. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate02011 line 487
  86. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02011 line 489
  87. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02012 line 498
  88. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02020 line 504
  89. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02021 line 511
  90. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02022 line 517
  91. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02100 line 523
  92. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02101 line 529
  93. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02102 line 535
  94. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02110 line 541
  95. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02111 line 547
  96. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02112 line 553
  97. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02120 line 560
  98. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02121 line 566
  99. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02122 line 573
  100. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02200 line 579
  101. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02201 line 585
  102. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02202 line 591
  103. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02210 line 597
  104. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02211 line 603
  105. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02212 line 609
  106. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02220 line 615
  107. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02221 line 621
  108. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent02222 line 627
  109. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10000 line 634
  110. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate10001 line 639
  111. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10001 line 641
  112. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10002 line 650
  113. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10010 line 656
  114. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10011 line 663
  115. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10012 line 669
  116. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10020 line 675
  117. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10021 line 681
  118. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10022 line 687
  119. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10100 line 693
  120. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10101 line 699
  121. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate10102 line 704
  122. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10102 line 706
  123. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10110 line 715
  124. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate10111 line 720
  125. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10111 line 722
  126. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10112 line 731
  127. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate10120 line 736
  128. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10120 line 738
  129. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10121 line 747
  130. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10122 line 753
  131. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10200 line 759
  132. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10201 line 765
  133. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10202 line 771
  134. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10210 line 777
  135. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10211 line 783
  136. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate10212 line 788
  137. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10212 line 790
  138. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10220 line 799
  139. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate10221 line 804
  140. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10221 line 806
  141. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent10222 line 815
  142. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11000 line 821
  143. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11001 line 827
  144. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate11002 line 832
  145. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11002 line 834
  146. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11010 line 843
  147. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate11011 line 848
  148. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11011 line 850
  149. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11012 line 859
  150. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate11020 line 864
  151. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11020 line 866
  152. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11021 line 875
  153. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11022 line 881
  154. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11100 line 887
  155. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11101 line 893
  156. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11102 line 899
  157. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11110 line 905
  158. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11111 line 911
  159. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate11112 line 916
  160. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11112 line 918
  161. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11120 line 927
  162. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate11121 line 932
  163. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11121 line 934
  164. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11122 line 943
  165. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11200 line 949
  166. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11201 line 955
  167. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11202 line 961
  168. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11210 line 967
  169. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11211 line 973
  170. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11212 line 979
  171. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11220 line 985
  172. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11221 line 991
  173. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent11222 line 997
  174. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12000 line 1004
  175. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12001 line 1010
  176. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12002 line 1016
  177. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12010 line 1022
  178. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12011 line 1028
  179. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate12012 line 1033
  180. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12012 line 1035
  181. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12020 line 1044
  182. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate12021 line 1049
  183. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12021 line 1051
  184. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12022 line 1060
  185. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12100 line 1066
  186. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12101 line 1072
  187. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12102 line 1078
  188. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12110 line 1084
  189. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12111 line 1090
  190. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12112 line 1096
  191. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12120 line 1102
  192. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12121 line 1108
  193. def OAI.CriticalHoneycomb.Transfer.Reflection.reflectionCertificate12122 line 1113
  194. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12122 line 1115
  195. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12200 line 1124
  196. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12201 line 1130
  197. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12202 line 1136
  198. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12210 line 1142
  199. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12211 line 1148
  200. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12212 line 1154
  201. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12220 line 1160
  202. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12221 line 1166
  203. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflectionComponent12222 line 1172
  204. theorem OAI.CriticalHoneycomb.Transfer.Reflection.reflection_constant line 1177
  205. theorem OAI.CriticalHoneycomb.Transfer.Reflection.reflection_linear line 1263