OAI/Combinatorics/HoneycombChords/SpectralCommutation.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Spectral commutation for critical honeycomb strips

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

  1. def OAI.CriticalHoneycomb.Transfer.RowExchange.sourceMatrix line 17
  2. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.local_source_exchange line 18
  3. def OAI.CriticalHoneycomb.Transfer.RowExchange.spectralSites line 33
  4. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.source_row_exchange line 36
  5. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.yangBaxter_denominator line 53
  6. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.yangBaxter_normalized line 55
  7. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.yangBaxter_spectral line 59
  8. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.sourceMatrix_spectral line 62
  9. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.spectralSites_exact line 64
  10. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.exact_row_exchange line 69
  11. lemma OAI.CriticalHoneycomb.Transfer.Reflection.continuous_sine line 88
  12. lemma OAI.CriticalHoneycomb.Transfer.Reflection.continuous_Q line 91
  13. lemma OAI.CriticalHoneycomb.Transfer.Reflection.continuous_bulkNumerator line 95
  14. lemma OAI.CriticalHoneycomb.Transfer.Reflection.continuousAt_spectralR line 100
  15. lemma OAI.CriticalHoneycomb.Transfer.Reflection.continuousAt_boundary0 line 102
  16. lemma OAI.CriticalHoneycomb.Transfer.Reflection.continuousAt_boundary1 line 112
  17. lemma OAI.CriticalHoneycomb.Transfer.Reflection.sine_zero_countable line 124
  18. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Q_zero_countable line 131
  19. lemma OAI.CriticalHoneycomb.Transfer.Reflection.dense_exchange_regular line 140
  20. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.matrix_entry_continuousAt line 163
  21. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.continuousAt_row line 167
  22. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.continuousAt_exact_row line 180
  23. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.continuous_C line 191
  24. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.continuousAt_K line 193
  25. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.continuousAt_bulkRows line 201
  26. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.continuousAt_T line 213
  27. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.eventually_nonsingular line 224
  28. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K_tensor line 249
  29. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.marked_right_invariant line 257
  30. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.marked_left_invariant line 269
  31. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.JRow_exchange line 281
  32. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.exactTrain_jet line 291
  33. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.closed_commutation_generic line 297
  34. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.source_global_spectral_commutation line 339
  35. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_PT_entry line 370
  36. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_PT_jet line 374
  37. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K_swap line 379
  38. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_reflection_generic line 395
  39. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.nonsingular_reflect line 411
  40. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.dense_swap_regular line 417
  41. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.source_spectral_reflection line 421
  42. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.parity line 446
  43. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.parity_sq line 447
  44. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.sine_add_pi line 449
  45. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.sine_sub_pi line 451
  46. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Q_periodic line 453
  47. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.A_antiperiodic line 455
  48. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.H_antiperiodic line 457
  49. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.V_periodic line 459
  50. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.C_periodic line 461
  51. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.D_periodic line 464
  52. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.R_periodic_entry line 466
  53. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.boundary0_periodic line 472
  54. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.boundary1_antiperiodic line 475
  55. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K0_periodic_entry line 480
  56. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.K1_periodic_entry line 485
  57. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.row_parity line 490
  58. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_row_periodic line 509
  59. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.spectral_row_sub_period line 516
  60. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.pairParity line 527
  61. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.pairParity_sq line 528
  62. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.bulkRows_periodic line 533
  63. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Kpart_periodic line 544
  64. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Kpart_sub_period line 548
  65. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.coefficient_periodic line 554
  66. theorem OAI.CriticalHoneycomb.Transfer.SpectralFamily.source_spectral_periodicity line 569
  67. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.cap line 583
  68. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.sum_cap line 584
  69. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.localForward_cap_expand line 587
  70. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.phase_cancel line 594
  71. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.localForward_cap line 600
  72. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.localForward_period_cap line 631