OAI/Combinatorics/HoneycombChords/CommonEigenline.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

The physical common eigenline and its crossing observable.

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.RasterGrid.marked_double_mixed_ports line 15
  2. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.source_marked_coefficient_limit line 26
  3. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedProjection_vacuum_base line 58
  4. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_vacuum_coefficient line 62
  5. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_eigenvalue_limit line 73
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangular_ports_im_zero line 93
  7. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_coefficient_real line 107
  8. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.source_eigenvalue_eq_twice_bridge_mass line 115
  9. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.reorient line 135
  10. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.reorient_mul line 138
  11. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalFamily_commute line 142
  12. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar line 149
  13. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_common_line line 151
  14. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_at_gamma line 158
  15. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_mass line 169
  16. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_reflection line 173
  17. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_periodicity line 178
  18. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.seedAux_eq line 190
  19. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rowGates line 201
  20. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fold_rowGates line 205
  21. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rowGates_valid line 211
  22. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.twoRowGates line 224
  23. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.twoRowGates_valid line 228
  24. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fold_twoRowGates line 239
  25. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.span_zero_of_length line 246
  26. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceDoubleRow line 260
  27. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceDoubleRow_eq_network line 266
  28. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceDoubleRow_span line 284
  29. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceDoubleRow_vacuum line 291
  30. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuum line 299
  31. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuum_span line 302
  32. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuum_value line 305
  33. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceRows line 308
  34. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceRows_span line 313
  35. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceRows_empty_entry line 320
  36. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.normalizedR_sourceR line 341
  37. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectralR_charge line 344
  38. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.row_charge line 352
  39. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_row_charge line 371
  40. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulkRows_charge line 375
  41. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_charge line 384
  42. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K1_charge line 387
  43. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.coefficient_shift line 390
  44. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spinCharge_rev line 413
  45. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.columnCharge_reflected line 415
  46. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_base line 420
  47. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_left line 425
  48. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_right line 430
  49. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_left_shift line 435
  50. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_right_shift line 443
  51. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectralWeights line 461
  52. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectralR_weights line 463
  53. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.row_planar_kernel line 467
  54. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_row_planar_kernel line 491
  55. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.boundaryWeight line 498
  56. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_planar line 499
  57. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_spin_star line 505
  58. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulkRows_spin_star line 519
  59. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.coefficient_base_spin_star line 532
  60. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_base_reversed line 547
  61. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_sum line 560
  62. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.seedAux_sum line 573
  63. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fixed_double_columns_distinct line 581
  64. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceDoubleRow_fixed line 602
  65. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.modelKernel line 631
  66. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.modelKernel_mulVec line 635
  67. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_row_modelKernel line 648
  68. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulkRows_modelKernel line 656
  69. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_base_matrix line 675
  70. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_base_source line 699
  71. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.commute_archProjection line 722
  72. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.base_commute line 728
  73. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.base_common_line line 735
  74. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.base_common_dual line 743
  75. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumIterate_span line 758
  76. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.columnVector_at_vacuum line 769
  77. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.columnVector_physical_iterate line 772
  78. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_iterate_limit line 779
  79. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_base_on_vacuumIterate line 792
  80. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physical_base_archColumn line 800
  81. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_base line 810
  82. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.common_scalar_left_zero line 831
  83. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.common_scalar_right_zero line 848
  84. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_singles line 868
  85. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_form line 888
  86. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.sine_ne_zero_interval line 896
  87. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.homogeneous_nonsingular_interval line 898
  88. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalFamily_node_fusion line 908
  89. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.commonScalar_mul_line line 918
  90. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.both_mul_normalized line 925
  91. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalScalar_node_fusion line 930
  92. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalP line 946
  93. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalP_reflection line 947
  94. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalP_mass line 953
  95. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_at_zero line 964
  96. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K1_at_zero line 970
  97. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K1_at_halfpi line 973
  98. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.boundary_ratio_halfpi line 978
  99. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_at_halfpi line 985
  100. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.phase_cap_cancel line 989
  101. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_close_cap line 993
  102. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K1_close_cap line 998
  103. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_close_twisted_cap line 1001
  104. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K1_close_twisted_cap line 1010
  105. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.forward_cap_all line 1023
  106. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.closed_at_cap line 1040
  107. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Q_endpoint_ne_zero line 1075
  108. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.homogeneous_T_zero line 1085
  109. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.homogeneous_T_halfpi line 1094
  110. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalFamily_of_T_one line 1108
  111. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.commonScalar_one line 1112
  112. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.physicalP_endpoint_zeros line 1115