OAI/Combinatorics/HoneycombChords/ClosedFusion.lean

GitHub source file

170 declarations, 0 contain sorry, 0 declared as axioms

Closed spectral fusion and its physical specialization.

This development follows the finite strip transfer calculation for critical honeycomb walks in the companion paper on uniform marked polygon estimates.

  1. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Q_at_L line 17
  2. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Q_at_L_ne_zero line 26
  3. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalR_binding line 29
  4. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.reverseSites line 39
  5. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.reverseSites_apply line 44
  6. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.row_eq_product line 46
  7. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.row_eq_matrixPath line 51
  8. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.cons_reverseSites line 54
  9. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_row_kernel line 57
  10. def OAI.CriticalHoneycomb.BoundaryJet.reflected line 81
  11. lemma OAI.CriticalHoneycomb.BoundaryJet.reflected_base line 83
  12. lemma OAI.CriticalHoneycomb.BoundaryJet.reflected_left line 84
  13. lemma OAI.CriticalHoneycomb.BoundaryJet.reflected_right line 85
  14. lemma OAI.CriticalHoneycomb.BoundaryJet.reflected_both line 86
  15. lemma OAI.CriticalHoneycomb.BoundaryJet.reflected_involutive line 87
  16. def OAI.CriticalHoneycomb.BoundaryJet.reflectJet line 90
  17. lemma OAI.CriticalHoneycomb.BoundaryJet.reflectJet_apply line 97
  18. lemma OAI.CriticalHoneycomb.BoundaryJet.reflectJet_C line 98
  19. lemma OAI.CriticalHoneycomb.BoundaryJet.reflectJet_eL line 102
  20. lemma OAI.CriticalHoneycomb.BoundaryJet.reflectJet_eR line 107
  21. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulk_spin_star_0 line 122
  22. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulk_spin_star_1 line 128
  23. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulk_spin_star_2 line 135
  24. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectralR_spin_star line 142
  25. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.flipSites line 153
  26. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.flipSites_apply line 155
  27. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.row_spin_star line 157
  28. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.reflectedSites line 174
  29. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_reflected_row line 176
  30. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.homogeneous line 192
  31. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.b_sub_gamma line 193
  32. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.gamma_homogeneous line 194
  33. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.sine_twice_gamma_ne_zero line 196
  34. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.homogeneous_nonsingular line 200
  35. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.positiveK line 207
  36. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.positiveK_binding line 209
  37. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.reflect_positiveK line 217
  38. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.markedDoubleMatrix_fin line 221
  39. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.markedDoubleMatrix_pair line 229
  40. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_bulkRows line 235
  41. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalFamily line 248
  42. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalFamily_at_gamma line 250
  43. def OAI.CriticalHoneycomb.Transfer.FusionContraction.contract line 280
  44. lemma OAI.CriticalHoneycomb.Transfer.FusionContraction.output_transpose line 283
  45. lemma OAI.CriticalHoneycomb.Transfer.FusionContraction.quotient_transpose line 288
  46. theorem OAI.CriticalHoneycomb.Transfer.FusionContraction.range_compression line 293
  47. theorem OAI.CriticalHoneycomb.Transfer.FusionContraction.quotient_compression line 317
  48. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rotateAux line 359
  49. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rotateSite line 364
  50. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rotate_rowA line 367
  51. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rotate_rowB line 373
  52. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rotate_rowC line 379
  53. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rotate_rowD line 384
  54. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.close4_rotate line 390
  55. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAB_backward line 399
  56. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxBC_mul line 405
  57. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxBC_one line 409
  58. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.middle_close line 413
  59. lemma OAI.CriticalHoneycomb.Transfer.FusionContraction.contract_eq_sum line 460
  60. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.matrixBoundary line 478
  61. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.close4_fusion_contract line 480
  62. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.closePair_fusion_contract line 499
  63. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_swap_transpose line 528
  64. def OAI.CriticalHoneycomb.Transfer.Reflection.fusionVector line 532
  65. def OAI.CriticalHoneycomb.Transfer.Reflection.fusionUnbend line 534
  66. lemma OAI.CriticalHoneycomb.Transfer.Reflection.fusion_unbend line 536
  67. def OAI.CriticalHoneycomb.Transfer.Reflection.bendPair line 547
  68. def OAI.CriticalHoneycomb.Transfer.Reflection.bendSpin line 549
  69. lemma OAI.CriticalHoneycomb.Transfer.Reflection.mul_bendPair line 551
  70. lemma OAI.CriticalHoneycomb.Transfer.Reflection.mul_bendSpin line 554
  71. lemma OAI.CriticalHoneycomb.Transfer.Reflection.fusion_bend line 557
  72. lemma OAI.CriticalHoneycomb.Transfer.Reflection.bendPair_Wbar line 566
  73. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Wbar_transpose_bendPair line 571
  74. lemma OAI.CriticalHoneycomb.Transfer.Reflection.boundary_bend line 576
  75. lemma OAI.CriticalHoneycomb.Transfer.Reflection.fusion_right_close line 581
  76. lemma OAI.CriticalHoneycomb.Transfer.Reflection.fusion_left_close line 586
  77. lemma OAI.CriticalHoneycomb.Transfer.Reflection.fusion_right_close_add line 595
  78. lemma OAI.CriticalHoneycomb.Transfer.Reflection.fusion_left_close_add line 602
  79. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_fusion_right_constant line 608
  80. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_fusion_right_linear line 613
  81. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_fusion_left_constant line 619
  82. lemma OAI.CriticalHoneycomb.Transfer.Reflection.source_fusion_left_linear line 624
  83. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.wallMatrix line 641
  84. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.markedFusionVector line 643
  85. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.wallMatrix_affine line 646
  86. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.markedFusionVector_affine line 651
  87. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.affine_right line 680
  88. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.affine_left line 689
  89. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.marked_fusion_right line 698
  90. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.marked_fusion_left line 705
  91. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.right_middle_boundary line 724
  92. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.left_middle_boundary line 733
  93. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.marked_middle_right line 745
  94. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.marked_middle_left line 750
  95. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceJ line 769
  96. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceJ_W line 771
  97. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceJ_Wbar line 775
  98. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceWbar_J line 779
  99. lemma OAI.CriticalHoneycomb.Transfer.cos_angle_pos line 788
  100. lemma OAI.CriticalHoneycomb.Transfer.sine2_sq line 791
  101. lemma OAI.CriticalHoneycomb.Transfer.denominator_two_angle line 796
  102. lemma OAI.CriticalHoneycomb.Transfer.special_two_angle line 801
  103. lemma OAI.CriticalHoneycomb.Transfer.denominator_zero line 825
  104. lemma OAI.CriticalHoneycomb.Transfer.sine2_pos line 827
  105. lemma OAI.CriticalHoneycomb.Transfer.special_zero line 831
  106. lemma OAI.CriticalHoneycomb.Transfer.denominator_bigAngle line 836
  107. lemma OAI.CriticalHoneycomb.Transfer.special_bigAngle line 842
  108. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.swapR line 856
  109. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceOmega line 858
  110. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceOmegaBar line 864
  111. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceKappa_real line 870
  112. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.Q_ne_of_denominator_ne line 872
  113. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.Q_zero_ne line 875
  114. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.Q_two_L_ne line 879
  115. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.Q_b_ne line 884
  116. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero00 line 888
  117. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero01 line 892
  118. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero02 line 896
  119. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero10 line 900
  120. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero11 line 904
  121. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero12 line 908
  122. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero20 line 912
  123. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero21 line 916
  124. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialZero22 line 920
  125. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.source_R_zero line 925
  126. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo00 line 938
  127. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo01 line 946
  128. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo02 line 955
  129. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo10 line 964
  130. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo11 line 973
  131. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo12 line 982
  132. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo20 line 991
  133. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo21 line 1000
  134. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialTwo22 line 1009
  135. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.source_R_two line 1018
  136. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB00 line 1031
  137. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB01 line 1038
  138. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB02 line 1045
  139. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB10 line 1052
  140. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB11 line 1059
  141. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB12 line 1066
  142. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB20 line 1073
  143. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB21 line 1080
  144. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralValueSpecialB22 line 1087
  145. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.source_R_b line 1095
  146. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.localBackward_with_swap line 1116
  147. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.row_range_factor line 1131
  148. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.row_quotient_factor line 1150
  149. def OAI.CriticalHoneycomb.Transfer.RowExchange.specialFinish line 1177
  150. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.local_first_node line 1180
  151. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.source_first_node_range line 1191
  152. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.source_R_L line 1217
  153. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.omegaBar_sum line 1223
  154. def OAI.CriticalHoneycomb.Transfer.RowExchange.secondFinish line 1226
  155. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.local_second_node_entry line 1228
  156. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.local_second_node line 1239
  157. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.source_second_node_quotient line 1263
  158. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.first_node_projection line 1292
  159. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.second_node_projection line 1302
  160. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.JRow_fusion line 1312
  161. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.JRow_quotient_fusion line 1320
  162. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.closed_fusion_compression line 1329
  163. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.closed_fusion_generic line 1387
  164. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.continuousAt_row_curve line 1425
  165. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.continuousAt_bulkRows_curve line 1432
  166. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.continuousAt_T_curve line 1445
  167. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.eventually_nonsingular_curve line 1459
  168. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.dense_fusion_regular line 1472
  169. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.fusion_along_nodes line 1489
  170. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.source_global_spectral_fusion line 1521