OAI/Combinatorics/HoneycombChords/FluxBounds.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

Boundary flux estimates

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

  1. inductive OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PositiveSpan line 16

    Source documentation

    Positive combinations of genuine planar tensor diagrams.

    inductive PositiveSpan (n b : ℕ) (seed : State) : DiluteState → Prop
  | zero : PositiveSpan n b seed (fun _=>0)
  | basis (o : List Bool) (k : ℕ) (w : PlanarWord b k)
      (hl : o.length=n) (hc : o.count true=b+2*k) :
      PositiveSpan n b seed (embed o (w.eval seed))
  | add {F G : DiluteState} (hF : PositiveSpan n b seed F)
      (hG : PositiveSpan n b seed G) : PositiveSpan n b seed (fun xs=>F xs+G xs)
  | smul (a : ℝ) (ha : 0≤a) {F : DiluteState} (hF : PositiveSpan n b seed F) :
      PositiveSpan n b seed (fun xs=>(a:ℂ)*F xs)

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PlanarWord, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed, OAI.CriticalHoneycomb.Transfer.a

  2. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.realWeights line 26
  3. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_positive line 29
  4. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PhasePositive line 69

    Source documentation

    Nonnegative multiples of an exact endpoint phase.

    def PhasePositive (z q : ℂ) : Prop := ∃ a : ℝ, 0≤a ∧ z=(a:ℂ)*q

    Mentions: OAI.CriticalHoneycomb.Transfer.a

  5. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PhasePositive.zero line 70
  6. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PhasePositive.add line 71
  7. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PhasePositive.smul line 75
  8. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.one_orientation_positive line 80
  9. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.two_orientation_positive line 99
  10. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pointState line 133
  11. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair line 136
  12. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_comm line 140
  13. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_zero line 145
  14. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_scalar line 149
  15. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_sum line 154
  16. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_scalar_right line 161
  17. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_sum_right line 164
  18. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pointState_cons line 169
  19. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_point line 174
  20. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_point_right line 188
  21. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.tile_transpose line 192
  22. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_act_zero line 196
  23. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_act line 232
  24. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates line 247
  25. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates_append line 250
  26. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.finitePair_gates line 254
  27. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates_kernel_transpose line 265

    Source documentation

    Ordinary transpose, not the Hermitian adjoint: precisely the cup gauge.

    theorem gates_kernel_transpose (t : TileWeights) {n : ℕ} (gs : List ℕ)
    (hg : ∀ i∈gs,i+1<n) (xs ys : List Spin) (hx : xs.length=n) (hy : ys.length=n) :
    gates t gs (pointState xs) ys=gates t gs.reverse (pointState ys) xs := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pointState

  28. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates_positive line 273
  29. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.point_one_positive line 283
  30. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.point_vacuum_positive line 293
  31. def OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rowSites line 320
  32. def OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rectangleSites line 323
  33. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rowSites_valid line 326
  34. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rectangleSites_valid line 336
  35. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.decode_row line 346
  36. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.decode_rectangle line 354
  37. def OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.stateOn line 363

    Source documentation

    A literal prescribed spin word; the vacant positions are not summed.

    noncomputable def stateOn : List Spin → FState
  | [] => emptyState
  | a::xs => consState (spinEquiv a) (stateOn xs)

    Mentions: OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.Spin, OAI.CriticalHoneycomb.Transfer.FluxWard.FState, OAI.CriticalHoneycomb.Transfer.FluxWard.emptyState, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.FluxWard.consState, OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.spinEquiv

  38. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.decode_stateOn line 366
  39. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.stateOn_vacuum line 378
  40. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.stateOn_prefix line 382
  41. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.stateOn_source line 387
  42. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.physical_nonneg line 393
  43. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.physical_eq_realWeights line 395
  44. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rectangle_one_phase line 398
  45. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rectangle_input_pair_phase line 411
  46. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_re line 433
  47. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_re_pos line 439
  48. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_re_le_one line 442
  49. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.diagram_phase line 444
  50. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.before_coefficient_nonneg line 450
  51. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.after_coefficient_nonneg line 466
  52. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.phasePositive_mul_real_nonneg line 479
  53. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac_zero line 485
  54. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct_zero line 488
  55. def OAI.CriticalHoneycomb.Transfer.FluxWard.emptyEval line 492
  56. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.emptyEval_add line 494
  57. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.emptyEval_smul line 497
  58. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.emptyEval_zero line 500
  59. def OAI.CriticalHoneycomb.Transfer.FluxWard.twoState line 502
  60. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.twoState_phase line 505
  61. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac_cons_one line 516
  62. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.before_real_nonneg line 522
  63. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.after_real_nonneg line 542
  64. def OAI.CriticalHoneycomb.Transfer.FluxWard.minusWord line 568
  65. def OAI.CriticalHoneycomb.Transfer.FluxWard.OneNonneg line 571
  66. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_source_positive line 574
  67. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.exitSum_real_nonneg line 588
  68. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.exitSum_append line 603
  69. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_output_bound line 615
  70. theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_west_exit_bound line 644

    Source documentation

    Finite physical parafermionic flux bounds the total opposite-side one-strand coefficient, uniformly in both rectangle dimensions.

    theorem rectangle_west_exit_bound (w k post : ℕ) :
    (exitSum (List.replicate (k+1+post) 1)
      (fun xs=>rectangleAct w (k+1+post) (sourceState (w+k) post)
        (xs++List.replicate w 1))).re≤1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.FluxWard.exitSum, OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct, OAI.CriticalHoneycomb.Transfer.FluxWard.sourceState

  71. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_zero_state line 677
  72. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_congr_length line 681
  73. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct_congr_length line 708
  74. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct_congr_length line 715
  75. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_suffix line 722
  76. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct_suffix line 739
  77. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct_suffix line 751
  78. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_prefixVac line 763
  79. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct_prefixVac line 782
  80. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac_eval_append line 790
  81. def OAI.CriticalHoneycomb.Transfer.FluxWard.vacuumColumn line 804
  82. theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_eq_columns line 809

    Source documentation

    Sweeping the lozenge rectangle and then fixing the north boundary is exactly iteration of its literal empty-auxiliary column.

    theorem rectangle_eq_columns (w h : ℕ) (f : FState) (xs : List (Fin 3))
    (hx : xs.length=h) :
    rectangleAct w h (prefixVac w f) (xs++List.replicate w 1)=
      (vacuumColumn h)^[w] f xs := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.FluxWard.FState, OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct, OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac, OAI.CriticalHoneycomb.Transfer.FluxWard.vacuumColumn

  83. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.decode_rowAct line 838
  84. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.spinEquiv_eq line 846
  85. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.physicalWeights_eq line 847
  86. def OAI.CriticalHoneycomb.Transfer.FluxWard.columnBasis line 849
  87. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.cons_columnBasis line 852
  88. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.vacuumColumn_basis_eq_kernel line 861
  89. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.consState_sum line 896
  90. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct_sum line 901
  91. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.vacuumColumn_sum line 910
  92. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.vacuumColumn_scalar line 914
  93. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.columnBasis_expansion line 920
  94. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.vacuumColumn_congr line 931
  95. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.vacuumColumn_as_matrix line 944
  96. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.iterateColumn_basis_eq_power line 956
  97. theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_columnBasis_eq_prescribed line 969

    Source documentation

    Literal finite rectangle: the flux raster and the actual center/path matrix use exactly the same vacuum north/south boundary and ordering.

    theorem rectangle_columnBasis_eq_prescribed (w h : ℕ) (west east : RasterGrid.Column h) :
    rectangleAct w h (prefixVac w (columnBasis east))
      (List.ofFn west++List.replicate w 1)=
      RasterGrid.prescribedPartition w h west east (fun _=>1) (fun _=>1) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct, OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac, OAI.CriticalHoneycomb.Transfer.FluxWard.columnBasis, OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition

  98. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.vacuum_indicator line 981
  99. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac_indicator line 991
  100. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.sourceState_indicator line 1003
  101. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.singleColumn_list line 1018
  102. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.sourceState_eq_basis line 1042
  103. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac_source line 1048
  104. lemma OAI.CriticalHoneycomb.Transfer.FluxWard.exitSum_eq_sum line 1054
  105. theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_actual_sum_bound line 1074

    Source documentation

    The actual literal honeycomb chord sum to the opposite wall, not an abstract positivity assumption on a transfer matrix.

    theorem rectangle_actual_sum_bound (W H : ℕ) (k : Fin (H+1)) :
    (∑ j : Fin (H+1),∑ γ : RasterGrid.RectChord W H j k,
      kappa^γ.val.length)≤1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.RectChord, OAI.CriticalHoneycomb.kappa

  106. theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_actual_mass_bound line 1090