The core module lean/FrcCore/Keys/Super.lean — the substrate from first principles, no Mathlib, no axioms (the modules in order: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Projective, Theme/Fourier, Theme/Fractional, Theme/Lifts, Theme/Dichotomy, Theme/Rotations, Theme/Heisenberg, Theme/Spectra, Theme/Exclusivity, Theme/Quadratic, Theme/Extension, Theme/Tally, Theme/Numbers, Theme/Logic, Theme/SecondOrder, Theme/Formation, Theme/Field, Theme/Foundation, Theme/Drive, Theme/Carrier, Theme/Subject, Theme/Pair, Theme/Hopf, Theme/Symbol, Theme/Gravity, Theme/Quantum, Theme/Unitary, Theme/Interactions, Theme/Fields, Theme/Horizon, Theme/Zeros, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Observation, Theme/Interference, Theme/Composite, Theme/Ladder, Theme/Flavour, Theme/Dark, Meridian, Fourier, Algebra, Epi, Dimensions, Poly, Quaternion, Causality, Representation, Reductio, Godel, Finitism, Geometry, Complex, Instances, Rh, Entropy, Dirac, Gravity, S13, Fields, Qm, Pnp, Flavour, Dark, Keys/Frame, Keys/Extension, Keys/Projective, Keys/Fourier, Keys/Numbers, Keys/Logic, Keys/Foundation, Keys/Carrier, Keys/Subject, Keys/Gravity, Keys/Quantum, Keys/Interactions, Keys/Horizon, Keys/Flavour, Keys/Dark, Theme/Hadrons, Hadrons, Keys/Hadrons, Theme/Super, Keys/Super, Theme/Spin): 2 theorems (0 definitions): 2 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Transform2import FrcCore.Theme.Super34/-!5# FrcCore.Keys.Super — the keyed theorems of the super theme (ledger migration, task LM19)67One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem8that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration9`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).10-/1112namespace FRC.Ledger1314-- Keys of the super theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)15/-- p00088 — 00:G19. \textbf{Superconductivity} (structure): superconductivity is split-torus confinement, the electric/phase dual of colour (G4), the charge-$2$ condensate a phase-singlet reducing $\mathrm{U}(1)$ to a residual $\Z_2$ (flux $h/2e$) and the Abrikosov vortex the dual colour string whose line tension vanishes at the Kramers--Wannier self-dual point $\beta_*=\tfrac12\ln(1+\sqrt2)$ that is $T_c$. -/16
theorem p00088 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k j : Nat), FRC.Shell.sumRange (fun l => FRC.Shell.Frame.Fmat g κ k l * FRC.Shell.Frame.Fmat g κ l j) (p - (1 : Nat)) = FRC.Shell.Frame.J (p - (1 : Nat)) k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.J (p - (1 : Nat)) k l * FRC.Shell.Frame.J (p - (1 : Nat)) l j) (p - (1 : Nat)) = if k = j then (1 : FRC.Shell p) else (0 : FRC.Shell p)) ∧ ((∀ {q : Nat} [FRC.Pos q] (a b : FRC.Shell q), a + b = (0 : FRC.Shell q) → b = -a) ∧ ([(16 : Nat), (28 : Nat), (40 : Nat), (52 : Nat), (88 : Nat), (100 : Nat)].all fun q => (FRC.Super.neutralPairs q).length == q && (FRC.Super.neutralPairs q).all fun ab => ab.snd == (q - ab.fst) % q) = true ∧ ([(16 : Nat), (28 : Nat)].all fun q => (FRC.Super.neutralTriples q).length == q * q) = true) ∧ ((∀ (m b : Nat), (0 : Nat) < m → b < (4 : Nat) * m → (2 : Nat) * b % ((4 : Nat) * m) = (0 : Nat) → b = (0 : Nat) ∨ b = (2 : Nat) * m) ∧ (∀ (m : Nat), (0 : Nat) < m → (2 : Nat) * (0 : Nat) % ((4 : Nat) * m) = (0 : Nat) ∧ (2 : Nat) * ((2 : Nat) * m) % ((4 : Nat) * m) = (0 : Nat)) ∧ ([(16 : Nat), (28 : Nat), (40 : Nat), (52 : Nat), (88 : Nat), (100 : Nat)].all fun q => FRC.Super.residual q == [(0 : Nat), q / (2 : Nat)]) = true) ∧ ∀ {p : Nat} [FRC.Pos p] (w : FRC.Shell p), w * w = (1 : FRC.Shell p) + (1 : FRC.Shell p) → ((1 : FRC.Shell p) + w) * (w + (-1 : FRC.Shell p)) = (1 : FRC.Shell p) ∧ (1 : FRC.Shell p) + w + -(w + (-1 : FRC.Shell p)) = (1 : FRC.Shell p) + (1 : FRC.Shell p) ∧ ((1 : FRC.Shell p) + (1 : FRC.Shell p) + w) * (w + (-1 : FRC.Shell p)) = w ∧ ((1 : FRC.Shell p) + w) * ((1 : FRC.Shell p) + w) + -(((1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((1 : FRC.Shell p) + w)) + (-1 : FRC.Shell p) = (0 : FRC.Shell p) :=17 And.intro @FRC.Shell.Frame.F_sq (And.intro @FRC.Shell.Frame.J_sq (And.intro @FRC.Super.winding_pairs (And.intro @FRC.Super.residual_two (@FRC.Super.self_dual_point))))18/-- p00089 — 00:G20. \textbf{Superconductivity} (duality): the electric--magnetic duality is the $Q_4$ quarter-turn on the charge-flux lattice (charge$\leftrightarrow$flux, Josephson$\leftrightarrow$phase-slip), predicting an Airy vortex-core spectrum and a quantum current standard whose metrology triangle closes on $q_c^2=4$. -/19theorem p00089 : (∀ {p : Nat} [FRC.Pos p] (a b a' b' : FRC.Shell p), FRC.Super.S (FRC.Super.S (a, b)) = (-a, -b) ∧ FRC.Super.S (FRC.Super.S (FRC.Super.S (FRC.Super.S (a, b)))) = (a, b) ∧ FRC.Super.pairing (FRC.Super.S (a, b)) (FRC.Super.S (a', b')) = FRC.Super.pairing (a, b) (a', b') ∧ FRC.Super.S ((1 : FRC.Shell p) + (1 : FRC.Shell p), (0 : FRC.Shell p)) = ((0 : FRC.Shell p), -((1 : FRC.Shell p) + (1 : FRC.Shell p))) ∧ FRC.Super.S ((0 : FRC.Shell p), (1 : FRC.Shell p)) = ((1 : FRC.Shell p), (0 : FRC.Shell p))) ∧ (∀ {p : Nat} [FRC.Pos p] (e h E Hi t : FRC.Shell p), e * E = (1 : FRC.Shell p) → h * Hi = (1 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * t = (1 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * e * Hi * (h * E * E) * (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * e) = (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) ∧ ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * e * Hi * (h * E * E) * e = (1 : FRC.Shell p) + (1 : FRC.Shell p) ∧ ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * e * (h * E * t) = h) ∧ FRC.Super.sturmEven (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (1018 : Int) / (1000 : Int)) = (0 : Nat) ∧ FRC.Super.sturmEven (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (1019 : Int) / (1000 : Int)) = (1 : Nat) ∧ FRC.Super.sturmEven (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (3246 : Int) / (1000 : Int)) = (1 : Nat) ∧ FRC.Super.sturmEven (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (3247 : Int) / (1000 : Int)) = (2 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (2337 : Int) / (1000 : Int)) = (0 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (2338 : Int) / (1000 : Int)) = (1 : Nat) ∧ (687 : Nat) * ((2338 : Nat) - (1018 : Nat)) < ((3246 : Nat) - (2338 : Nat)) * (1000 : Nat) ∧ ((3247 : Nat) - (2337 : Nat)) * (1000 : Nat) < (691 : Nat) * ((2337 : Nat) - (1019 : Nat)) ∧ ((3247 : Nat) - (2337 : Nat)) * (1000 : Nat) < (1000 : Nat) * ((2337 : Nat) - (1019 : Nat)) :=20 And.intro @FRC.Super.symplectic_quarter_turn (And.intro @FRC.Super.metrology_closure (@FRC.Super.airy_ladder_sturm))21-- end keys2223end FRC.Ledger24