Theme/Super.lean — FrcCore

1import FrcCore.Theme.Hadrons2import FrcCore.Ring34/-!5# FrcCore.Theme.Super — the super theme (superconductivity on the split torus, 19 October 2026)67The exact content of the master's rows G19 (superconductivity, structure) and G20 (superconductivity, duality), developed8in the master without a paper ledger (34-super is unpublished; its theorems C1, C3–C5, C9, C10 and its prediction D1 are9the content), as `frc/super.py` and `frc/ledgers/master/super.py` compute it: the phase-neutral pairs of a cycle are the10inverse pairs `(k, −k)` (`winding_pairs`, G19), the charge-`2` condensate leaves the residual `ℤ₂` on every cycle of length11`4m` (`residual_two`, G19), the self-dual point `β* = ½ ln(1 + √2)` as a ring identity in `√2` (`self_dual_point`, G19),12the symplectic quarter-turn on the charge–flux lattice (`symplectic_quarter_turn`, G20), the metrology closure13`K_J R_K Q = 4` (`metrology_closure`, G20) and the even and odd Airy ladders of the vortex core by Sturm's count14(`airy_ladder_sturm`, G20). Kernel-decided or ring-normalised throughout; no axioms (`check_core_axioms.py`).15-/1617namespace FRC.Super1819open FRC.Shell FRC.Shell.Frame2021/-! ## The phase-neutral pairs and the residual `ℤ₂` (00:G19; 34-super C3, C4) -/2223/-- The two-body neutral composites of a cycle of length `q`: the pairs `(a, b)` with `a + b ≡ 0 (mod q)`, as a list. -/24def neutralPairs (q : Nat) : List (Nat × Nat) :=25  (List.range q).flatMap fun a => ((List.range q).filter fun b => (a + b) % q == 0).map fun b => (a, b)2627/-- The three-body neutral composites of a cycle of length `q`. -/28def neutralTriples (q : Nat) : List (Nat × Nat × Nat) :=29  (List.range q).flatMap fun a => (List.range q).flatMap fun b =>30    ((List.range q).filter fun c => (a + b + c) % q == 0).map fun c => (a, b, c)3132/-- 00:G19 — the phase-neutral pair is the inverse pair: on every shell, `a + b = 0` forces `b = −a` (the zero-total-winding33Cooper pair `(k, −k)`); on the substrates `q = 16, 28, 40, 52, 88, 100` the two-body neutral set has exactly `q` members, each34`(a, (q − a) mod q)`, and on `q = 16, 28` the three-body neutral set has `q²` members. -/35theorem winding_pairs :36    (∀ {q : Nat} [Pos q] (a b : Shell q), a + b = 0 → b = -a) ∧37    ([16, 28, 40, 52, 88, 100].all fun q =>38      (neutralPairs q).length == q && (neutralPairs q).all fun ab => ab.2 == (q - ab.1) % q) = true ∧39    ([16, 28].all fun q => (neutralTriples q).length == q * q) = true :=40  ⟨fun a b h => (neg_eq_of_add_eq_zero h).symm, by decide +kernel, by decide +kernel⟩4142/-- The vorticities `b < q` with `2b ≡ 0 (mod q)`: the subgroup the charge-`2` condensate leaves deconfined. -/43def residual (q : Nat) : List Nat := (List.range q).filter fun b => (2 * b) % q == 04445/-- 00:G19 — the charge-`2` condensate leaves the residual `ℤ₂`: on every cycle of length `4m`, the solutions `b < 4m` of46`2b ≡ 0 (mod 4m)` are exactly `0` and `2m` — two of them, the flux quantum `h/2e` the half of the cycle; on the substrates47`q = 16, 28, 40, 52, 88, 100` the residual list is `[0, q/2]`. -/48theorem residual_two :49    (∀ m b : Nat, 0 < m → b < 4 * m → (2 * b) % (4 * m) = 0 → b = 0 ∨ b = 2 * m) ∧50    (∀ m : Nat, 0 < m → (2 * 0) % (4 * m) = 0 ∧ (2 * (2 * m)) % (4 * m) = 0) ∧51    ([16, 28, 40, 52, 88, 100].all fun q => residual q == [0, q / 2]) = true := by52  refine ⟨?_, ?_, by decide +kernel⟩53  · intro m b hm hb h54    have h4 : 0 < 4 * m := Nat.mul_pos (by decide) hm55    obtain ⟨t, ht⟩ := FRC.Nat.mod_spec (4 * m) h4 (2 * b)56    rw [h, Nat.add_zero] at ht57    have hb' : b = 2 * m * t := by58      apply Nat.eq_of_mul_eq_mul_left (show 0 < 2 by decide)59      rw [ht, ← FRC.Nat.mul_assoc, ← FRC.Nat.mul_assoc]60    have hb4 : b < 2 * m * 2 := by61      rw [FRC.Nat.mul_assoc, Nat.mul_comm m 2, ← FRC.Nat.mul_assoc]62      exact hb63    have ht2 : t < 2 := by                                   -- without the classical `Nat.lt_of_mul_lt_mul_left`64      match Nat.lt_or_ge t 2 with65      | Or.inl h => exact h66      | Or.inr h =>67        have : 2 * m * 2 ≤ b := by rw [hb']; exact Nat.mul_le_mul_left (2 * m) h68        exact absurd (Nat.lt_of_lt_of_le hb4 this) (Nat.lt_irrefl _)69    cases t with                                             -- `cases`, not `match`: the latter's impossible case uses propext70    | zero => exact Or.inl (by rw [hb', Nat.mul_zero])71    | succ t => cases t with72      | zero => exact Or.inr (by rw [hb', Nat.mul_one])73      | succ t => exact absurd ht2 (Nat.not_lt_of_le (Nat.le_add_left 2 t))74  · intro m hm75    exact ⟨rfl, by rw [← FRC.Nat.mul_assoc]; exact FRC.Nat.mod_self (4 * m) (Nat.mul_pos (by decide) hm)⟩7677/-! ## The self-dual point as a ring identity in `√2` (00:G19; 34-super C5) -/7879/-- 00:G19 — with `w² = 2` (every shell carrying `√2`, and `ℤ[√2]`) and `x = e^{2β*} = 1 + w`: `(1 + w)(w − 1) = 1`, so80`x − x⁻¹ = (1 + w) − (w − 1) = 2` and `sinh 2β* = 1`; `(2 + w)(w − 1) = w`, so `tanh β* = (x − 1)/(x + 1) = w/(2 + w) = w − 1 =81√2 − 1`; the vortex line tension `τ(β*) = 2β* + ln tanh β* = ln[(1 + w)(w − 1)] = ln 1 = 0`; and `x² − 2x − 1 = 0`, the82fixed point of the duality `sinh 2β sinh 2β̃ = 1`: `β* = ½ ln(1 + √2)` is the self-dual point, where the vortex deconfines. -/83theorem self_dual_point {p : Nat} [Pos p] (w : Shell p) (hw : w * w = 1 + 1) :84    (1 + w) * (w + -1) = 1 ∧ 1 + w + -(w + -1) = 1 + 1 ∧ (1 + 1 + w) * (w + -1) = w ∧85    (1 + w) * (1 + w) + -((1 + 1) * (1 + w)) + -1 = 0 := by86  refine ⟨?_, ?_, ?_, ?_⟩87  · have e : (1 + w) * (w + -1) = w * w + -1 := RE.sound (look [w]) (.mul (.add .one (.var 0)) (.add (.var 0) (.neg .one))) (.add (.mul (.var 0) (.var 0)) (.neg .one)) (by decide +kernel)88    rw [e, hw]89    exact RE.sound (look []) (.add (.add .one .one) (.neg .one)) .one (by decide +kernel)90  · exact RE.sound (look [w]) (.add (.add .one (.var 0)) (.neg (.add (.var 0) (.neg .one)))) (.add .one .one) (by decide +kernel)91  · have e : (1 + 1 + w) * (w + -1) = w * w + -(1 + 1) + w := RE.sound (look [w]) (.mul (.add (.add .one .one) (.var 0)) (.add (.var 0) (.neg .one))) (.add (.add (.mul (.var 0) (.var 0)) (.neg (.add .one .one))) (.var 0)) (by decide +kernel)92    rw [e, hw]93    exact RE.sound (look [w]) (.add (.add (.add .one .one) (.neg (.add .one .one))) (.var 0)) (.var 0) (by decide +kernel)94  · have e : (1 + w) * (1 + w) + -((1 + 1) * (1 + w)) + -1 = w * w + -(1 + 1) := RE.sound (look [w]) (.add (.add (.mul (.add .one (.var 0)) (.add .one (.var 0))) (.neg (.mul (.add .one .one) (.add .one (.var 0))))) (.neg .one)) (.add (.mul (.var 0) (.var 0)) (.neg (.add .one .one))) (by decide +kernel)95    rw [e, hw]96    exact RE.sound (look []) (.add (.add .one .one) (.neg (.add .one .one))) .zero (by decide +kernel)9798/-! ## The symplectic quarter-turn on the charge–flux lattice (00:G20; 34-super C9) -/99100/-- The electric–magnetic dual `S(a, b) = (b, −a)` on the charge–flux lattice. -/101def S {p : Nat} [Pos p] (v : Shell p × Shell p) : Shell p × Shell p := (v.2, -v.1)102103/-- The Dirac pairing `ω((a, b), (a', b')) = ab' − a'b`. -/104def pairing {p : Nat} [Pos p] (u v : Shell p × Shell p) : Shell p := u.1 * v.2 + -(v.1 * u.2)105106/-- 00:G20 — the duality is a symplectic quarter-turn: `S² = −I` (charge conjugation), `S⁴ = I`, the pairing `ab' − a'b` is107`S`-invariant, the condensate `(2, 0)` goes to the double vortex `(0, −2)` and the unit vortex `(0, 1)` to the unit charge108`(1, 0)` — charge and flux exchanged, Wilson and 't Hooft loops exchanged, on every shell. -/109theorem symplectic_quarter_turn {p : Nat} [Pos p] (a b a' b' : Shell p) :110    S (S (a, b)) = (-a, -b) ∧ S (S (S (S (a, b)))) = (a, b) ∧111    pairing (S (a, b)) (S (a', b')) = pairing (a, b) (a', b') ∧112    S ((1 : Shell p) + 1, 0) = (0, -(1 + 1)) ∧ S ((0 : Shell p), 1) = (1, 0) := by113  refine ⟨rfl, ?_, ?_, rfl, ?_⟩114  · show (- -a, - -b) = (a, b)115    rw [neg_neg a, neg_neg b]116  · show b * -a' + -(b' * -a) = a * b' + -(a' * b)117    exact RE.sound (look [a, b, a', b']) (.add (.mul (.var 1) (.neg (.var 2))) (.neg (.mul (.var 3) (.neg (.var 0))))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 2) (.var 1)))) (by decide +kernel)118  · show ((1 : Shell p), -(0 : Shell p)) = (1, 0)119    rw [neg_zero]120121/-! ## The metrology closure (00:G20; 34-super C10) -/122123/-- 00:G20 — the charge–flux duality of the quantised relations, with the inverses `E = e⁻¹`, `Hi = h⁻¹` and the half `t`124(`2t = 1`) as shell elements: the Josephson constant `K_J = 2e/h`, the von Klitzing resistance `R_K = h/e²` and the current125quantum `Q` close the metrology triangle on an integer, `K_J R_K Q = 4 = q_c²` for the pair quantum `Q = 2e` and `2` for the126single-electron quantum `Q = e`; the condensate charge `2e` and the flux quantum `h/2e` multiply to the action quantum `h`.127Each is a ring identity in `e, h, E, Hi, t` with the hypotheses `eE = 1`, `hHi = 1`, `2t = 1` applied. -/128theorem metrology_closure {p : Nat} [Pos p] (e h E Hi t : Shell p) (he : e * E = 1) (hh : h * Hi = 1) (ht : (1 + 1) * t = 1) :129    (1 + 1) * e * Hi * (h * E * E) * ((1 + 1) * e) = 1 + 1 + 1 + 1 ∧130    (1 + 1) * e * Hi * (h * E * E) * e = 1 + 1 ∧131    (1 + 1) * e * (h * E * t) = h := by132  refine ⟨?_, ?_, ?_⟩133  · have i : (1 + 1) * e * Hi * (h * E * E) * ((1 + 1) * e) = (1 + 1 + 1 + 1) * (e * E) * (e * E) * (h * Hi) := RE.sound (look [e, h, E, Hi, t]) (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 3)) (.mul (.mul (.var 1) (.var 2)) (.var 2))) (.mul (.add .one .one) (.var 0))) (.mul (.mul (.mul (.add (.add (.add .one .one) .one) .one) (.mul (.var 0) (.var 2))) (.mul (.var 0) (.var 2))) (.mul (.var 1) (.var 3))) (by decide +kernel)134    rw [i, he, hh]135    exact RE.sound (look []) (.mul (.mul (.mul (.add (.add (.add .one .one) .one) .one) .one) .one) .one) (.add (.add (.add .one .one) .one) .one) (by decide +kernel)136  · have i : (1 + 1) * e * Hi * (h * E * E) * e = (1 + 1) * (e * E) * (e * E) * (h * Hi) := RE.sound (look [e, h, E, Hi, t]) (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 3)) (.mul (.mul (.var 1) (.var 2)) (.var 2))) (.var 0)) (.mul (.mul (.mul (.add .one .one) (.mul (.var 0) (.var 2))) (.mul (.var 0) (.var 2))) (.mul (.var 1) (.var 3))) (by decide +kernel)137    rw [i, he, hh]138    exact RE.sound (look []) (.mul (.mul (.mul (.add .one .one) .one) .one) .one) (.add .one .one) (by decide +kernel)139  · have i : (1 + 1) * e * (h * E * t) = h * (e * E) * ((1 + 1) * t) := RE.sound (look [e, h, E, Hi, t]) (.mul (.mul (.add .one .one) (.var 0)) (.mul (.mul (.var 1) (.var 2)) (.var 4))) (.mul (.mul (.var 1) (.mul (.var 0) (.var 2))) (.mul (.add .one .one) (.var 4))) (by decide +kernel)140    rw [i, he, ht]141    exact RE.sound (look [h]) (.mul (.mul (.var 0) .one) .one) (.var 0) (by decide +kernel)142143/-! ## The even and odd Airy ladders of the vortex core by Sturm's count (00:G20; 34-super D1) -/144145/-- The leading principal minors of the even (Neumann) operator's integer tridiagonal on the sites `k = 0 … N`: the diagonal146`2c + L³ k` with `c = (N + 1)³`, the squared off-diagonal `2c²` on the first link (the origin's symmetrising rescaling,147`u(−h) = u(h)`) and `c²` on the others; `(p_k, p_{k−1}, sign changes)`, as `FRC.Hadrons.sturmAux` for the odd (Dirichlet)148operator. -/149def sturmEvenAux (N L : Nat) (μ : Int) : Nat → Int × Int × Nat150  | 0 => (1, 1, 0)151  | k + 1 =>152    let (pm, pmm, acc) := sturmEvenAux N L μ k153    let c : Int := ((N + 1) ^ 3 : Nat)154    let d : Int := 2 * c + (L ^ 3 : Nat) * (k : Nat)155    let cc : Int := if k = 1 then 2 * c * c else c * c156    let cur := (d - μ) * pm - (if k = 0 then 0 else cc * pmm)157    (cur, pm, if (decide (cur < 0)) != (decide (pm < 0)) then acc + 1 else acc)158159/-- Sturm's count of the even operator's eigenvalues below `μ = (N + 1) L² ε`, over its `N + 1` sites. -/160def sturmEven (N L : Nat) (μ : Int) : Nat := (sturmEvenAux N L μ (N + 1)).2.2161162/-- 00:G20 — the vortex-core ladder is the Airy ladder, by Sturm's count on `N = 200` sites of `[0, 16]`: the even operator163has exactly one eigenvalue in `(1.018, 1.019)` (`E₁`, the first zero of `Ai'`) and one in `(3.246, 3.247)` (`E₃`, the164second), the odd operator (`FRC.Hadrons.sturm`) exactly one in `(2.337, 2.338)` (`E₂`, the first zero of `Ai`); so the165successive-spacing ratio `ρ = (E₃ − E₂)/(E₂ − E₁)` lies in `(0.687, 0.691)` — the Airy value `0.690`, below the166equally-spaced ladder's `1`. The bracket ends enter as the integer `μ = ⌊201 · 256 · ε⌋`, within `2 × 10⁻⁵` below the167decimal `ε` (the convention of `FRC.Hadrons.airy_sturm`); the python witness `frc.super.airy_ladder` counts at the exact168decimals in `Fraction`s. -/169theorem airy_ladder_sturm :170    sturmEven 200 16 (201 * 256 * 1018 / 1000) = 0 ∧ sturmEven 200 16 (201 * 256 * 1019 / 1000) = 1 ∧171    sturmEven 200 16 (201 * 256 * 3246 / 1000) = 1 ∧ sturmEven 200 16 (201 * 256 * 3247 / 1000) = 2 ∧172    FRC.Hadrons.sturm 200 16 (201 * 256 * 2337 / 1000) = 0 ∧ FRC.Hadrons.sturm 200 16 (201 * 256 * 2338 / 1000) = 1 ∧173    687 * (2338 - 1018) < (3246 - 2338) * 1000 ∧ (3247 - 2337) * 1000 < 691 * (2337 - 1019) ∧174    (3247 - 2337) * 1000 < 1000 * (2337 - 1019) := by175  decide +kernel176177end FRC.Super178