OAI/Combinatorics/HoneycombChords/Reflection.lean

GitHub source file

156 declarations, 0 contain sorry, 0 declared as axioms

Reflection equations, boundary fusion and bulk fusion.

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

  1. def OAI.CriticalHoneycomb.Transfer.Reflection.root line 14
  2. def OAI.CriticalHoneycomb.Transfer.Reflection.point line 15
  3. lemma OAI.CriticalHoneycomb.Transfer.Reflection.root_ne_zero line 16
  4. lemma OAI.CriticalHoneycomb.Transfer.Reflection.point_ne_zero line 17
  5. lemma OAI.CriticalHoneycomb.Transfer.Reflection.point_add line 18
  6. lemma OAI.CriticalHoneycomb.Transfer.Reflection.point_sub line 20
  7. lemma OAI.CriticalHoneycomb.Transfer.Reflection.root_pow line 22
  8. lemma OAI.CriticalHoneycomb.Transfer.Reflection.root_sixteen line 28
  9. lemma OAI.CriticalHoneycomb.Transfer.Reflection.root_constraint line 31
  10. lemma OAI.CriticalHoneycomb.Transfer.Reflection.point_nat_angle line 32
  11. lemma OAI.CriticalHoneycomb.Transfer.Reflection.root_eight line 33
  12. lemma OAI.CriticalHoneycomb.Transfer.Reflection.root_complement line 36
  13. lemma OAI.CriticalHoneycomb.Transfer.Reflection.point_neg_angle line 39
  14. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sine_exp line 44
  15. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sine_positive_shift line 50
  16. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sine_negative_shift line 60
  17. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sine_zero_shift line 70
  18. def OAI.CriticalHoneycomb.Transfer.Reflection.sine line 80
  19. def OAI.CriticalHoneycomb.Transfer.Reflection.tau line 81
  20. def OAI.CriticalHoneycomb.Transfer.Reflection.S line 82
  21. def OAI.CriticalHoneycomb.Transfer.Reflection.gamma line 83
  22. def OAI.CriticalHoneycomb.Transfer.Reflection.b line 84
  23. def OAI.CriticalHoneycomb.Transfer.Reflection.L line 85
  24. def OAI.CriticalHoneycomb.Transfer.Reflection.phase line 86
  25. def OAI.CriticalHoneycomb.Transfer.Reflection.Q line 87
  26. def OAI.CriticalHoneycomb.Transfer.Reflection.coeffA line 88
  27. def OAI.CriticalHoneycomb.Transfer.Reflection.coeffH line 89
  28. def OAI.CriticalHoneycomb.Transfer.Reflection.coeffV line 90
  29. def OAI.CriticalHoneycomb.Transfer.Reflection.coeffC line 91
  30. def OAI.CriticalHoneycomb.Transfer.Reflection.coeffD line 92
  31. def OAI.CriticalHoneycomb.Transfer.Reflection.bulkNumerator line 93
  32. def OAI.CriticalHoneycomb.Transfer.Reflection.spectralR line 116
  33. def OAI.CriticalHoneycomb.Transfer.Reflection.boundary0 line 117
  34. def OAI.CriticalHoneycomb.Transfer.Reflection.boundary1 line 119
  35. lemma OAI.CriticalHoneycomb.Transfer.Reflection.tau_ne_zero line 122
  36. lemma OAI.CriticalHoneycomb.Transfer.Reflection.phase_eq line 124
  37. lemma OAI.CriticalHoneycomb.Transfer.Reflection.phase_inv line 126
  38. lemma OAI.CriticalHoneycomb.Transfer.Reflection.phase_inv_sq line 132
  39. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_b_minus line 136
  40. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_quarter_minus line 138
  41. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_b_plus line 140
  42. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_quarter_plus line 142
  43. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_minus_L line 144
  44. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_zero line 152
  45. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_S line 153
  46. lemma OAI.CriticalHoneycomb.Transfer.Reflection.coeffA_scaled line 163
  47. lemma OAI.CriticalHoneycomb.Transfer.Reflection.coeffH_scaled line 165
  48. lemma OAI.CriticalHoneycomb.Transfer.Reflection.coeffV_scaled line 167
  49. lemma OAI.CriticalHoneycomb.Transfer.Reflection.coeffC_scaled line 169
  50. lemma OAI.CriticalHoneycomb.Transfer.Reflection.coeffD_scaled line 171
  51. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Q_scaled line 173
  52. lemma OAI.CriticalHoneycomb.Transfer.Reflection.bulk_scaled line 175
  53. lemma OAI.CriticalHoneycomb.Transfer.Reflection.r_homogeneous line 183
  54. lemma OAI.CriticalHoneycomb.Transfer.Reflection.spectralR_scaled line 187
  55. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_gamma_minus line 191
  56. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sin_gamma_plus line 193
  57. def OAI.CriticalHoneycomb.Transfer.Reflection.beta line 195
  58. lemma OAI.CriticalHoneycomb.Transfer.Reflection.beta_ne_zero line 196
  59. lemma OAI.CriticalHoneycomb.Transfer.Reflection.beta_polynomial line 198
  60. lemma OAI.CriticalHoneycomb.Transfer.Reflection.beta_k line 200
  61. lemma OAI.CriticalHoneycomb.Transfer.Reflection.point_twice line 205
  62. lemma OAI.CriticalHoneycomb.Transfer.Reflection.beta_l line 207
  63. lemma OAI.CriticalHoneycomb.Transfer.Reflection.boundary0_scaled line 212
  64. lemma OAI.CriticalHoneycomb.Transfer.Reflection.boundary1_scaled line 218
  65. def OAI.CriticalHoneycomb.Transfer.Reflection.alphaMinus line 232
  66. def OAI.CriticalHoneycomb.Transfer.Reflection.alphaPlus line 233
  67. lemma OAI.CriticalHoneycomb.Transfer.Reflection.alphaMinus_ne_zero line 234
  68. lemma OAI.CriticalHoneycomb.Transfer.Reflection.alphaPlus_ne_zero line 236
  69. lemma OAI.CriticalHoneycomb.Transfer.Reflection.rminus_scaled line 238
  70. lemma OAI.CriticalHoneycomb.Transfer.Reflection.rplus_scaled line 244
  71. lemma OAI.CriticalHoneycomb.Transfer.Reflection.slot1_smul line 247
  72. lemma OAI.CriticalHoneycomb.Transfer.Reflection.slot2_smul line 250
  73. lemma OAI.CriticalHoneycomb.Transfer.Reflection.scale_four line 253
  74. lemma OAI.CriticalHoneycomb.Transfer.Reflection.scalar_cancel line 258
  75. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_reflection_constant line 263
  76. theorem OAI.CriticalHoneycomb.Transfer.Reflection.source_reflection_linear line 280
  77. lemma OAI.CriticalHoneycomb.Transfer.Reflection.swap_constant_algebra line 305
  78. lemma OAI.CriticalHoneycomb.Transfer.Reflection.swap_linear_algebra line 308
  79. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.twoCos line 318
  80. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceKappa line 319
  81. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceW line 320
  82. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceWbar line 330
  83. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.point_L line 340
  84. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.point_neg_L line 342
  85. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.point_add_L line 344
  86. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.point_sub_L line 345
  87. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.twoCos_polynomial line 347
  88. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.twoCos_ne_zero line 354
  89. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.kappa_normalization line 357
  90. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceW_scaled line 358
  91. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceWbar_scaled line 364
  92. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.star_point line 370
  93. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.phase_star line 375
  94. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceKappa_star line 380
  95. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceWbar_eq_conj line 382
  96. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bNum_binding line 386
  97. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.aNum_binding line 387
  98. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bNum_plus_binding line 391
  99. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bNum_minus_binding line 392
  100. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.constant_plus_binding line 393
  101. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.constant_minus_binding line 396
  102. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.linear_plus_binding line 399
  103. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.linear_minus_binding line 402
  104. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulk_twice_binding line 405
  105. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceKappa_eq_critical line 416
  106. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionProduct line 425
  107. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionLift line 428
  108. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionProduct_smul line 431
  109. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionLift_smul line 440
  110. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkScale line 446
  111. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bulkScale_ne_zero line 447
  112. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.qNumerator_binding line 456
  113. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.plusNumerator_binding line 458
  114. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.minusNumerator_binding line 462
  115. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.source_bulk_fusion line 467
  116. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionScalar line 493
  117. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionScalar_ne_zero line 495
  118. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.scalar_cancel_rect line 502
  119. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundary_fusion_constant line 507
  120. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundary_fusion_linear line 524
  121. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror line 551
  122. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_mul line 553
  123. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_add line 559
  124. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spinFlip line 563
  125. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spinFlip_apply line 568
  126. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.pairFlip line 569
  127. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sine_star line 571
  128. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_boundary0 line 573
  129. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_boundary1 line 577
  130. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_slot1 line 582
  131. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_slot2 line 586
  132. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_W line 590
  133. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_Wbar line 595
  134. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_00 line 600
  135. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_01 line 604
  136. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_02 line 608
  137. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_10 line 612
  138. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_11 line 616
  139. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_12 line 620
  140. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_20 line 624
  141. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_21 line 628
  142. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk_22 line 632
  143. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.mirror_bulk line 636
  144. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundary_fusion_dual_constant line 649
  145. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundary_fusion_dual_linear line 657
  146. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk00 line 677
  147. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk01 line 681
  148. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk02 line 685
  149. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk10 line 689
  150. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk11 line 693
  151. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk12 line 697
  152. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk20 line 701
  153. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk21 line 705
  154. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.hermitianHermitianBulk22 line 709
  155. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.spectralR_hermitian line 714
  156. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.sourceW_conjTranspose line 726