OAI/Combinatorics/HoneycombChords/SpectralRows.lean

GitHub source file

334 declarations, 0 contain sorry, 0 declared as axioms

Spectral monodromy rows and boundary exchange identities

Formalized from Uniform marked polygon estimates and sharp finite bridge moments (OpenAI, September 26, 2026).

  1. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.local_source_fusion line 17
  2. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.local_source_quotient_fusion line 29
  3. def OAI.CriticalHoneycomb.Transfer.RowExchange.exactSites line 36
  4. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.source_row_fusion line 39
  5. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.source_row_quotient_fusion line 51
  6. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflected_Q line 70
  7. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflected_A line 74
  8. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflected_H line 76
  9. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflected_V line 77
  10. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflected_C line 79
  11. lemma OAI.CriticalHoneycomb.Transfer.Reflection.reflected_D line 82
  12. def OAI.CriticalHoneycomb.Transfer.Reflection.spinValue line 85
  13. lemma OAI.CriticalHoneycomb.Transfer.Reflection.spinValue_rev line 86
  14. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent00 line 88
  15. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent01 line 94
  16. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent02 line 101
  17. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent10 line 110
  18. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent11 line 118
  19. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent12 line 127
  20. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent20 line 134
  21. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent21 line 143
  22. lemma OAI.CriticalHoneycomb.Transfer.Reflection.crossingCrossingComponent22 line 151
  23. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_crossing line 158
  24. abbrev OAI.CriticalHoneycomb.BoundaryJet.Jet line 178
  25. def OAI.CriticalHoneycomb.BoundaryJet.C line 179
  26. def OAI.CriticalHoneycomb.BoundaryJet.eL line 180
  27. def OAI.CriticalHoneycomb.BoundaryJet.eR line 181
  28. def OAI.CriticalHoneycomb.BoundaryJet.base line 182
  29. def OAI.CriticalHoneycomb.BoundaryJet.left line 183
  30. def OAI.CriticalHoneycomb.BoundaryJet.right line 184
  31. def OAI.CriticalHoneycomb.BoundaryJet.both line 185
  32. lemma OAI.CriticalHoneycomb.BoundaryJet.jet_ext line 186
  33. lemma OAI.CriticalHoneycomb.BoundaryJet.base_mul line 191
  34. lemma OAI.CriticalHoneycomb.BoundaryJet.left_mul line 192
  35. lemma OAI.CriticalHoneycomb.BoundaryJet.right_mul line 194
  36. lemma OAI.CriticalHoneycomb.BoundaryJet.both_mul line 196
  37. lemma OAI.CriticalHoneycomb.BoundaryJet.base_add line 200
  38. lemma OAI.CriticalHoneycomb.BoundaryJet.left_add line 201
  39. lemma OAI.CriticalHoneycomb.BoundaryJet.right_add line 202
  40. lemma OAI.CriticalHoneycomb.BoundaryJet.both_add line 203
  41. lemma OAI.CriticalHoneycomb.BoundaryJet.base_C line 204
  42. lemma OAI.CriticalHoneycomb.BoundaryJet.left_C line 205
  43. lemma OAI.CriticalHoneycomb.BoundaryJet.right_C line 206
  44. lemma OAI.CriticalHoneycomb.BoundaryJet.both_C line 207
  45. lemma OAI.CriticalHoneycomb.BoundaryJet.eL_sq line 208
  46. lemma OAI.CriticalHoneycomb.BoundaryJet.eR_sq line 209
  47. def OAI.CriticalHoneycomb.BoundaryJet.form line 211
  48. lemma OAI.CriticalHoneycomb.BoundaryJet.base_form line 212
  49. lemma OAI.CriticalHoneycomb.BoundaryJet.left_form line 213
  50. lemma OAI.CriticalHoneycomb.BoundaryJet.right_form line 214
  51. lemma OAI.CriticalHoneycomb.BoundaryJet.both_form line 215
  52. lemma OAI.CriticalHoneycomb.BoundaryJet.form_coords line 216
  53. def OAI.CriticalHoneycomb.BoundaryJet.baseAdd line 218
  54. def OAI.CriticalHoneycomb.BoundaryJet.leftAdd line 219
  55. def OAI.CriticalHoneycomb.BoundaryJet.rightAdd line 220
  56. def OAI.CriticalHoneycomb.BoundaryJet.bothAdd line 221
  57. lemma OAI.CriticalHoneycomb.BoundaryJet.base_sum line 222
  58. lemma OAI.CriticalHoneycomb.BoundaryJet.left_sum line 224
  59. lemma OAI.CriticalHoneycomb.BoundaryJet.right_sum line 226
  60. lemma OAI.CriticalHoneycomb.BoundaryJet.both_sum line 228
  61. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0 line 239
  62. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.K1 line 241
  63. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.K line 244
  64. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulkRows line 245
  65. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.T line 249
  66. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.coefficient line 252
  67. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K_left line 256
  68. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K_right line 258
  69. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.T_coefficients line 261
  70. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Nonsingular line 269
  71. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.GlobalSpectralCommutation line 273
  72. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.GlobalSpectralFusion line 277
  73. lemma OAI.CriticalHoneycomb.Transfer.Reflection.point_reflected_mul line 289
  74. lemma OAI.CriticalHoneycomb.Transfer.Reflection.alphaMinus_C_poly line 294
  75. lemma OAI.CriticalHoneycomb.Transfer.Reflection.alphaMinus_H_poly line 300
  76. lemma OAI.CriticalHoneycomb.Transfer.Reflection.alphaMinus_V_poly line 310
  77. lemma OAI.CriticalHoneycomb.Transfer.Reflection.alphaMinus_A_poly line 315
  78. lemma OAI.CriticalHoneycomb.Transfer.Reflection.alphaMinus_poly line 320
  79. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_swap_constant_scalar line 325
  80. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_swap_linear_scalar line 336
  81. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.boundarySwapPhaseFourRelation line 355
  82. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.source_K0_swap line 358
  83. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.source_K1_swap line 372
  84. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_forwardPair line 396
  85. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_backwardPair line 403
  86. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_pair_exchange line 410
  87. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_auxBC line 421
  88. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_auxAC line 427
  89. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_auxBD line 433
  90. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_auxAD line 439
  91. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_auxTrain line 444
  92. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.square_zero_tensor line 449
  93. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_right_jet line 463
  94. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.map_left_jet line 478
  95. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.JRow line 501
  96. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.forward_JRow line 503
  97. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.T_closePair line 508
  98. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.backward_JRow line 513
  99. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing00 line 525
  100. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing01 line 531
  101. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing02 line 538
  102. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing10 line 546
  103. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing11 line 553
  104. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing12 line 561
  105. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing20 line 568
  106. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing21 line 576
  107. lemma OAI.CriticalHoneycomb.Transfer.Reflection.transposeCrossingTransposeCrossing22 line 583
  108. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_transpose_crossing line 590
  109. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Scalar line 611
  110. def OAI.CriticalHoneycomb.Transfer.Reflection.pairMatrix line 612
  111. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pairMatrix_mul line 614
  112. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pairMatrix_transpose line 626
  113. def OAI.CriticalHoneycomb.Transfer.Reflection.bulkJet line 628
  114. def OAI.CriticalHoneycomb.Transfer.Reflection.boundaryJet line 630
  115. def OAI.CriticalHoneycomb.Transfer.Reflection.jetSlot1 line 632
  116. def OAI.CriticalHoneycomb.Transfer.Reflection.jetSlot2 line 634
  117. lemma OAI.CriticalHoneycomb.Transfer.Reflection.jetSlot1_pair line 636
  118. lemma OAI.CriticalHoneycomb.Transfer.Reflection.jetSlot2_pair line 639
  119. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_reflection line 643
  120. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceWbar_reverse line 661
  121. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceWbar_spin line 664
  122. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceWbar_crossing_phase line 669
  123. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sum_fin_rev line 680
  124. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Spin3 line 690
  125. def OAI.CriticalHoneycomb.Transfer.Reflection.boundaryVector line 691
  126. def OAI.CriticalHoneycomb.Transfer.Reflection.crossedBC line 693
  127. def OAI.CriticalHoneycomb.Transfer.Reflection.crossedADt line 696
  128. def OAI.CriticalHoneycomb.Transfer.Reflection.unbend line 699
  129. lemma OAI.CriticalHoneycomb.Transfer.Reflection.phase_cancellation line 701
  130. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sandwich12 line 706
  131. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sandwich21 line 714
  132. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unbend_BC line 722
  133. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unbend_ADt line 744
  134. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_flip_transpose line 774
  135. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_spin line 778
  136. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_phase_conservation line 783
  137. def OAI.CriticalHoneycomb.Transfer.Reflection.actAC line 796
  138. def OAI.CriticalHoneycomb.Transfer.Reflection.actBDt line 798
  139. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unbend_injective line 800
  140. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unbend_add line 806
  141. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unbend_AC line 810
  142. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unbend_BDt line 819
  143. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_boundary_pair_constant line 840
  144. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_boundary_pair_linear line 851
  145. def OAI.CriticalHoneycomb.Transfer.angle line 875
  146. def OAI.CriticalHoneycomb.Transfer.bigAngle line 876
  147. def OAI.CriticalHoneycomb.Transfer.sine2 line 877
  148. def OAI.CriticalHoneycomb.Transfer.denominator line 878
  149. def OAI.CriticalHoneycomb.Transfer.a line 881
  150. def OAI.CriticalHoneycomb.Transfer.h line 883
  151. def OAI.CriticalHoneycomb.Transfer.v line 885
  152. def OAI.CriticalHoneycomb.Transfer.c line 887
  153. def OAI.CriticalHoneycomb.Transfer.d line 889
  154. def OAI.CriticalHoneycomb.Transfer.phase line 892
  155. def OAI.CriticalHoneycomb.Transfer.blockOne line 894
  156. def OAI.CriticalHoneycomb.Transfer.blockZero line 897
  157. lemma OAI.CriticalHoneycomb.Transfer.sine_product line 902
  158. lemma OAI.CriticalHoneycomb.Transfer.c_as_denominator line 908
  159. lemma OAI.CriticalHoneycomb.Transfer.c_unitary line 913
  160. lemma OAI.CriticalHoneycomb.Transfer.h_conjugate_c line 918
  161. lemma OAI.CriticalHoneycomb.Transfer.denominator_product line 926
  162. lemma OAI.CriticalHoneycomb.Transfer.one_diagonal line 936
  163. lemma OAI.CriticalHoneycomb.Transfer.one_offdiagonal line 943
  164. lemma OAI.CriticalHoneycomb.Transfer.sin_bigAngle line 950
  165. lemma OAI.CriticalHoneycomb.Transfer.cos_bigAngle line 954
  166. lemma OAI.CriticalHoneycomb.Transfer.cos_two_angle line 958
  167. lemma OAI.CriticalHoneycomb.Transfer.mixed_sine_identity line 963
  168. lemma OAI.CriticalHoneycomb.Transfer.zero_mixed line 985
  169. lemma OAI.CriticalHoneycomb.Transfer.blockOne_unitary line 995
  170. lemma OAI.CriticalHoneycomb.Transfer.phase_sq line 1007
  171. lemma OAI.CriticalHoneycomb.Transfer.phase_ne_zero line 1016
  172. lemma OAI.CriticalHoneycomb.Transfer.phase_inv line 1018
  173. lemma OAI.CriticalHoneycomb.Transfer.blockZero_unitary line 1025
  174. lemma OAI.CriticalHoneycomb.Transfer.Reflection.angle_double line 1056
  175. lemma OAI.CriticalHoneycomb.Transfer.Reflection.bigAngle_binding line 1057
  176. lemma OAI.CriticalHoneycomb.Transfer.Reflection.angle_binding line 1058
  177. lemma OAI.CriticalHoneycomb.Transfer.Reflection.denominator_binding line 1059
  178. lemma OAI.CriticalHoneycomb.Transfer.Reflection.phase_binding line 1061
  179. lemma OAI.CriticalHoneycomb.Transfer.Reflection.normA line 1065
  180. lemma OAI.CriticalHoneycomb.Transfer.Reflection.normH line 1069
  181. lemma OAI.CriticalHoneycomb.Transfer.Reflection.normV line 1073
  182. lemma OAI.CriticalHoneycomb.Transfer.Reflection.normC line 1077
  183. lemma OAI.CriticalHoneycomb.Transfer.Reflection.normD line 1081
  184. def OAI.CriticalHoneycomb.Transfer.Reflection.normalizedR line 1086
  185. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization00 line 1114
  186. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization01 line 1119
  187. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization02 line 1125
  188. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization10 line 1130
  189. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization11 line 1136
  190. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization12 line 1141
  191. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization20 line 1147
  192. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization21 line 1152
  193. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityNormalization22 line 1158
  194. lemma OAI.CriticalHoneycomb.Transfer.Reflection.spectralR_normalized line 1163
  195. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0000 line 1175
  196. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0001 line 1183
  197. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0002 line 1189
  198. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0010 line 1195
  199. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0011 line 1201
  200. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0012 line 1207
  201. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0020 line 1213
  202. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0021 line 1219
  203. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0022 line 1225
  204. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary00 line 1231
  205. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0100 line 1246
  206. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0101 line 1252
  207. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0102 line 1259
  208. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0110 line 1265
  209. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0111 line 1272
  210. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0112 line 1278
  211. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0120 line 1284
  212. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0121 line 1290
  213. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0122 line 1296
  214. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary01 line 1302
  215. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0200 line 1317
  216. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0201 line 1323
  217. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0202 line 1329
  218. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0210 line 1336
  219. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0211 line 1342
  220. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0212 line 1349
  221. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0220 line 1355
  222. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0221 line 1362
  223. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary0222 line 1368
  224. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary02 line 1374
  225. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1000 line 1389
  226. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1001 line 1395
  227. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1002 line 1402
  228. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1010 line 1408
  229. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1011 line 1415
  230. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1012 line 1421
  231. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1020 line 1427
  232. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1021 line 1433
  233. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1022 line 1439
  234. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary10 line 1445
  235. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1100 line 1460
  236. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1101 line 1466
  237. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1102 line 1472
  238. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1110 line 1479
  239. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1111 line 1485
  240. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1112 line 1492
  241. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1120 line 1498
  242. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1121 line 1505
  243. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1122 line 1511
  244. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary11 line 1517
  245. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1200 line 1532
  246. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1201 line 1538
  247. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1202 line 1544
  248. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1210 line 1550
  249. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1211 line 1556
  250. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1212 line 1562
  251. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1220 line 1569
  252. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1221 line 1575
  253. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary1222 line 1582
  254. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary12 line 1588
  255. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2000 line 1603
  256. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2001 line 1609
  257. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2002 line 1615
  258. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2010 line 1622
  259. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2011 line 1628
  260. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2012 line 1635
  261. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2020 line 1641
  262. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2021 line 1648
  263. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2022 line 1654
  264. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary20 line 1660
  265. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2100 line 1675
  266. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2101 line 1681
  267. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2102 line 1687
  268. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2110 line 1693
  269. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2111 line 1699
  270. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2112 line 1705
  271. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2120 line 1712
  272. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2121 line 1718
  273. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2122 line 1725
  274. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary21 line 1731
  275. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2200 line 1746
  276. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2201 line 1752
  277. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2202 line 1758
  278. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2210 line 1764
  279. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2211 line 1770
  280. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2212 line 1776
  281. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2220 line 1782
  282. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2221 line 1788
  283. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary2222 line 1794
  284. lemma OAI.CriticalHoneycomb.Transfer.Reflection.unitarityUnitary22 line 1802
  285. theorem OAI.CriticalHoneycomb.Transfer.Reflection.spectral_unitarity line 1816
  286. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.FourVector line 1841
  287. def OAI.CriticalHoneycomb.Transfer.Reflection.actAD line 1842
  288. def OAI.CriticalHoneycomb.Transfer.Reflection.actBD line 1844
  289. def OAI.CriticalHoneycomb.Transfer.Reflection.actBC line 1846
  290. def OAI.CriticalHoneycomb.Transfer.Reflection.pairVector line 1848
  291. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actBD_transpose line 1850
  292. lemma OAI.CriticalHoneycomb.Transfer.Reflection.BC_pairVector line 1854
  293. lemma OAI.CriticalHoneycomb.Transfer.Reflection.ADt_pairVector line 1858
  294. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actAD_comp line 1863
  295. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actBD_comp line 1867
  296. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actAD_one line 1871
  297. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actBD_one line 1874
  298. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actAD_add line 1877
  299. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actBD_add line 1881
  300. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actBC_add line 1885
  301. lemma OAI.CriticalHoneycomb.Transfer.Reflection.actAC_add line 1889
  302. def OAI.CriticalHoneycomb.Transfer.Reflection.fourExchanges line 1894
  303. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_boundary_invariant_constant line 1899
  304. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_boundary_invariant_linear line 1916
  305. def OAI.CriticalHoneycomb.Transfer.Reflection.pair4 line 1939
  306. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_AD line 1941
  307. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_BD line 1947
  308. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_AC line 1952
  309. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_BC line 1959
  310. lemma OAI.CriticalHoneycomb.Transfer.Reflection.dot_pair_cancel line 1965
  311. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_AD_cancel line 1968
  312. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_BD_cancel line 1974
  313. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_AC_cancel line 1980
  314. lemma OAI.CriticalHoneycomb.Transfer.Reflection.pair4_BC_cancel line 1987
  315. lemma OAI.CriticalHoneycomb.Transfer.Reflection.spectral_transpose_unitarity line 1993
  316. theorem OAI.CriticalHoneycomb.Transfer.Reflection.four_exchanges_pair line 1997
  317. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_left_covector_constant line 2010
  318. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_left_covector_linear line 2029
  319. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.flatten4 line 2056
  320. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.unflatten4 line 2058
  321. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.flatten_unflatten line 2060
  322. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.flatten_add line 2061
  323. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.flattenBC line 2062
  324. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.flattenAC line 2067
  325. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.flattenBD line 2072
  326. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.flattenAD line 2077
  327. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exactTrain line 2082
  328. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exactTrain_action line 2085
  329. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pair4_flatten line 2089
  330. theorem OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exactTrain_right_constant line 2093
  331. theorem OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exactTrain_right_linear line 2100
  332. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.vecMul_eq_of_pair4 line 2108
  333. theorem OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exactTrain_left_constant line 2117
  334. theorem OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exactTrain_left_linear line 2126