Flux.lean`

GitHub source file

131 declarations, 0 contain sorry, 0 declared as axioms

Finite honeycomb current conservation

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

def OAI.CriticalHoneycomb.Transfer.FluxWard.r line 16
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_ne_zero line 17
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_sq line 18
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_eight line 24
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_inverse line 27
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.phase_q line 33
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.phase_inv_q line 34
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.kappa_phase line 39
def OAI.CriticalHoneycomb.Transfer.FluxWard.raising line 52
Source documentation
Off-diagonal raising generator, in the source order +, vacant, -.
```
def raising (i j : Fin 3) : ℂ :=
…
```
def OAI.CriticalHoneycomb.Transfer.FluxWard.twist line 55
Source documentation
Diagonal quantum-group weight, with q=exp(5πi/8).
```
noncomputable def twist (i : Fin 3) : ℂ :=
…
```
def OAI.CriticalHoneycomb.Transfer.FluxWard.untwist line 57
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.twist_inverse line 60
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.weight_equation line 66
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.kappa_polynomial line 70
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_power_reduce line 73
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_8 line 78
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_9 line 82
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_10 line 86
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_11 line 90
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_12 line 94
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_13 line 98
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_14 line 102
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_15 line 106
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_16 line 110
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_17 line 114
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_18 line 118
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_19 line 122
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_20 line 126
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_21 line 130
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_22 line 134
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_23 line 138
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_24 line 142
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_25 line 146
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_26 line 150
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_27 line 154
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_28 line 158
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_29 line 162
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_30 line 166
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_31 line 170
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.r_pow_32 line 174
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.inverse_r_sq line 179
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.up_current line 182
Source documentation
Local current conservation at a single actual up-triangle center.
```
theorem up_current (w a b : Fin 3) :
    (∑ v : Fin 3, raising w v * upTensor v a b) =
      r * (∑ v : Fin 3, upTensor w v b * raising v a * twist b) +
      r⁻¹ * (∑ v : Fin 3, upTensor w a v * untwist a * raising v b) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Transfer.FluxWard.raising, OAI.CriticalHoneycomb.Transfer.FluxWard.r, OAI.CriticalHoneycomb.Transfer.FluxWard.twist, OAI.CriticalHoneycomb.Transfer.FluxWard.untwist
def OAI.CriticalHoneycomb.Transfer.FluxWard.physicalTile line 192
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_twist line 195
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_untwist line 200
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_00 line 205
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_01 line 215
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_02 line 225
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_10 line 235
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_11 line 245
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_12 line 255
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_20 line 265
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_21 line 275
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current_22 line 285
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.tile_current line 295
Source documentation
The exact R tile transports the weighted current (r,1) to (1,r). Its phases and κ are those of the original honeycomb model.
```
theorem tile_current (w n s e : Fin 3) :
    (∑ v : Fin 3, raising w v * twist n * physicalTile v n s e) +
      r * (∑ v : Fin 3, untwist w * raising n v * physicalTile w v s e) =
      r * (∑ v : Fin 3, physicalTile w n v e * raising v s * twist e) +
      (∑ v : Fin 3, physicalTile w n s v * untwist s * raising v e) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Transfer.FluxWard.raising, OAI.CriticalHoneycomb.Transfer.FluxWard.twist, OAI.CriticalHoneycomb.Transfer.FluxWard.physicalTile, OAI.CriticalHoneycomb.Transfer.FluxWard.r, OAI.CriticalHoneycomb.Transfer.FluxWard.untwist
abbrev OAI.CriticalHoneycomb.Transfer.FluxWard.FState line 316
def OAI.CriticalHoneycomb.Transfer.FluxWard.twistProduct line 317
def OAI.CriticalHoneycomb.Transfer.FluxWard.untwistProduct line 318
def OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct line 320
def OAI.CriticalHoneycomb.Transfer.FluxWard.current line 328
Source documentation
The coproduct of the actual spin-raising current, with direction weights attached to the boundary wires in their planar contour order.
```
noncomputable def current : List ℂ → FState → FState
  | [], _, _ => 0
  | q::qs, f, x::xs =>
      q * (∑ y : Fin 3, raising x y * f (y::xs)) * twistProduct xs +
      untwist x * current qs (fun ys=>f (x::ys)) xs
  | _::_, _, [] => 0
```
Mentions: OAI.CriticalHoneycomb.Transfer.FluxWard.FState, OAI.CriticalHoneycomb.Transfer.FluxWard.raising, OAI.CriticalHoneycomb.Transfer.FluxWard.twistProduct, OAI.CriticalHoneycomb.Transfer.FluxWard.untwist
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_add line 335
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_smul line 349
def OAI.CriticalHoneycomb.Transfer.FluxWard.siteLinear line 363
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_add line 368
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_smul line 383
def OAI.CriticalHoneycomb.Transfer.FluxWard.currentLinear line 400
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_sum line 405
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_sum line 412
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_scalar line 419
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_scalar line 422
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_twist line 426
abbrev OAI.CriticalHoneycomb.Transfer.FluxWard.TwoSpin line 456
def OAI.CriticalHoneycomb.Transfer.FluxWard.pairCurrent line 457
def OAI.CriticalHoneycomb.Transfer.FluxWard.tileMatrix line 460
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.pairCurrent_left line 462
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.pairCurrent_right line 471
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.pairCurrent_tile line 480
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.pairCurrent_act line 486
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_two line 493
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_zero_pair line 513
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_site_tail line 518
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.current_site_zero line 533
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct_pointwise_add line 548
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.current_site_prefix line 553
Source documentation
The local physical Ward identity at any adjacent pair of contour wires.
```
theorem current_site_prefix (pre qs : List ℂ) (f : FState) :
    current (pre++1::r::qs) (siteAct pre.length f) =
      siteAct pre.length (current (pre++r::1::qs) f) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.FluxWard.FState, OAI.CriticalHoneycomb.Transfer.FluxWard.current, OAI.CriticalHoneycomb.Transfer.FluxWard.r, OAI.CriticalHoneycomb.Transfer.FluxWard.siteAct
def OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct line 573
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct_current line 577
def OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct line 593
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_current line 600
Source documentation
Finite rectangle current conservation, including all boundary indices. It is an equality for the literal physical tensor network, not an assumed bound or an infinite-volume assertion.
```
theorem rectangle_current (w h : ℕ) (qs : List ℂ) (f : FState) :
    current (List.replicate h 1 ++ List.replicate w r ++ qs) (rectangleAct w h f) =
      rectangleAct w h (current (List.replicate w r ++ List.replicate h 1 ++ qs) f) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.FluxWard.FState, OAI.CriticalHoneycomb.Transfer.FluxWard.current, OAI.CriticalHoneycomb.Transfer.FluxWard.r, OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct
def OAI.CriticalHoneycomb.Transfer.FluxWard.consState line 623
def OAI.CriticalHoneycomb.Transfer.FluxWard.emptyState line 626
def OAI.CriticalHoneycomb.Transfer.FluxWard.vacuum line 629
def OAI.CriticalHoneycomb.Transfer.FluxWard.twistState line 632
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.consState_add line 634
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.consState_smul line 638
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.consState_zero line 642
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_zero line 645
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_emptyHead line 648
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_minusHead line 657
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.twist_consState line 666
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.twist_vacuum line 676
def OAI.CriticalHoneycomb.Transfer.FluxWard.plusSum line 681
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_vacuum line 685
def OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac line 691
def OAI.CriticalHoneycomb.Transfer.FluxWard.sourceState line 694
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac_add line 697
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.prefixVac_smul line 701
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.twist_source line 706
def OAI.CriticalHoneycomb.Transfer.FluxWard.beforeArches line 715
def OAI.CriticalHoneycomb.Transfer.FluxWard.afterArches line 718
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.current_source line 723
Source documentation
The input side of the boundary Ward identity: the current creates just one vacuum term and the two ordered classes of source-to-input arcs.
```
theorem current_source (pre post : List ℂ) (q : ℂ) :
    current (pre++q::post) (sourceState pre.length post.length) =
      (-q) • vacuum (pre.length+1+post.length) +
      (-r^3) • beforeArches pre post.length + r^5 • afterArches pre.length post := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.FluxWard.current, OAI.CriticalHoneycomb.Transfer.FluxWard.sourceState, OAI.CriticalHoneycomb.Transfer.FluxWard.vacuum, OAI.CriticalHoneycomb.Transfer.FluxWard.r, OAI.CriticalHoneycomb.Transfer.FluxWard.beforeArches, OAI.CriticalHoneycomb.Transfer.FluxWard.afterArches
def OAI.CriticalHoneycomb.Transfer.FluxWard.exitSum line 740
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.twistProduct_vacuum line 744
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.current_vacuum_eval line 747
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct_add line 756
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rowAct_smul line 760
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct_add line 764
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct_smul line 769
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_boundary_flux line 778
Source documentation
Exact boundary flux equality for a prescribed input port of the finite physical lozenge rectangle. The three non-vacuum terms enumerate output exits and the two contour-ordered classes of input-side arches.
```
theorem rectangle_boundary_flux (w h : ℕ) (pre post : List ℂ) (q : ℂ)
    (directions : List.replicate w r++List.replicate h 1=pre++q::post) :
    exitSum (List.replicate h 1++List.replicate w r)
        (rectangleAct w h (sourceState pre.length post.length)) +
      (-r^3)*(rectangleAct w h (beforeArches pre post.length)) (List.replicate (h+w) 1) +
      r^5*(rectangleAct w h (afterArches pre.length post)) (List.replicate (h+w) 1) =
      q*(rectangleAct w h (vacuum (w+h))) (List.replicate (h+w) 1) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.FluxWard.r, OAI.CriticalHoneycomb.Transfer.FluxWard.exitSum, OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct, OAI.CriticalHoneycomb.Transfer.FluxWard.sourceState, OAI.CriticalHoneycomb.Transfer.FluxWard.beforeArches, OAI.CriticalHoneycomb.Transfer.FluxWard.afterArches, OAI.CriticalHoneycomb.Transfer.FluxWard.vacuum
abbrev OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.Spin line 811
def OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.spinEquiv line 813
def OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.physicalWeights line 818
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.tile_physical line 821
def OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.decode line 827
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.decode_siteAct line 830
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.decode_vacuum line 855
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.decode_vacuum_eval line 869
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.row_span line 873
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.row_vacuum line 883
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rectangle_span line 898
lemma OAI.CriticalHoneycomb.Transfer.FluxWard.Diagram.rectangle_vacuum line 907
theorem OAI.CriticalHoneycomb.Transfer.FluxWard.rectangle_vacuum_one line 921
Source documentation
The boundary Ward identity's normalization is the literal empty partition: all detached closed honeycomb loops cancel.
```
theorem rectangle_vacuum_one (w h : ℕ) :
    rectangleAct w h (vacuum (w+h)) (List.replicate (h+w) 1)=1 := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.FluxWard.rectangleAct, OAI.CriticalHoneycomb.Transfer.FluxWard.vacuum