super.py — frc/ledgers/master

1"""master/super — a ledger file of the master's block G, the superconductivity rows: the rows the super theme proves, developed2in the master (19 October 2026; 34-super is unpublished and has no paper ledger).34The master's superconductivity rows of block G are bound by this file. It binds G19 (structure: superconductivity as5split-torus confinement — the dual map the quarter-turn transform, the charge-2 condensate a phase-singlet leaving the6residual ℤ₂ with flux h/2e, the vortex line tension vanishing at the self-dual point β* = ½ ln(1 + √2)) and G20 (duality:7the Q₄ quarter-turn on the charge–flux lattice, the Josephson–phase-slip dictionary and the metrology closure on q_c² = 4,8the Airy vortex-core ladder): the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean9proofs each key conjoins (PROOFS), and the checks, which call the super theme (frc/super.py), the frame theme's transform10(frc/fourier.py) and, for the readings, the chart theme (frc/chart_super.py). The Lean side is11lean/FrcCore/Theme/Super.lean with the frame theme's Transform.lean, the key file lean/FrcCore/Keys/Super.lean and the12certificate lean/FrcCore/Ledgers/Master/Super.lean. Both rows are T rows of block G, so their keys are the core's; the13continuum readings (τ(β) in floating point, the universal numbers, the ladder's decimal ratio) are the rows' charts,14decided here in python alone (gate G08). The checks reproduce 34-super's scripts m1–m7 record for record.1516    python3 -m frc.ledgers.master.super        every block, the census; exit 1 if a check fails (≈ 2 s)1718Blocks:  S  structure: the dual map, the winding kernel, the residual ℤ₂, the self-dual point   EXACT, CHART  (00:G19)19         D  duality: the quarter-turn, the metrology closure, the Airy ladder                     EXACT, CHART  (00:G20)2021The notebook frc/ledgers/master/super.ipynb runs one row per cell, the cell's id its key (gate G13).22"""23import sys24from fractions import Fraction as Q2526from frc.registry import Registry27from frc import super as S28from frc import chart_super as CS2930# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----31BLOCK = "G"32KEYS = {"G1": "p00178", "G2": "p00067", "G3": "p00068", "G4": "p00069", "G5": "p00070", "G6": "p00071", "G7": "p27043", "G8": "p00073", "G9": "p00074", "G10": "p00075", "G11": "p27020", "G12": "p00155", "G13": "p00078", "G14": "p00079", "G15": "p00080", "G16": "p00081", "G17": "p00179", "G18": "p00083", "G19": "p00088", "G20": "p00089", "G21": "p00090"}       # every row of the block: its label and its accession key33LEAN = {"G19": "core", "G20": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them34# ---- end of the generated table ----3536# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys37# FRC.Ledger.p<key> from them). The master's block file is the binding's source, as a paper's \lean{} cells are its own.38PROOFS = {39    "G19": ["FRC.Shell.Frame.F_sq", "FRC.Shell.Frame.J_sq",                                       # 34-super C1: the dual map is the quarter-turn transform, F² = J, F⁴ = I40            "FRC.Super.winding_pairs", "FRC.Super.residual_two", "FRC.Super.self_dual_point"],     # C3, C4, C5: the inverse pairs, the residual ℤ₂, the self-dual point41    "G20": ["FRC.Super.symplectic_quarter_turn", "FRC.Super.metrology_closure", "FRC.Super.airy_ladder_sturm"],   # C9, C10, D142}4344LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none4546LEDGER = {"S1": "00:G19", "S2": "00:G19", "D1": "00:G20", "D2": "00:G20"}47BLOCKS = {"S": "structure: the dual map, the winding kernel, the residual ℤ₂, the self-dual point",48          "D": "duality: the quarter-turn, the metrology closure, the Airy ladder"}49PREDICATES = {"00:G19": "S1", "00:G20": "D1"}5051R = Registry("00", "super", LEDGER, PREDICATES, sources=[__file__])5253SUBSTRATES = [16, 28, 40, 52, 88, 100]       # q = p − 1 for the primes p ≡ 5 (mod 12) of 34-super's m1: 17, 29, 41, 53, 89, 10154FRAMES = [(17, 3), (29, 2)]                  # the shells of the first two substrates with a drive (frc.shell.generators)555657def _near(x, centre, tol):58    return abs(x - centre) < tol596061# ------------------------------------------------------------------------------------------------------------62# block S: structure (00:G19)63@R.block("S", BLOCKS["S"])64def block_S():65    """Block S — structure: S1 the exact content (EXACT), S2 the tension and the universal numbers (CHART)."""66    # 00:G19 (p00088)67    maps = [S.dual_map(p, g) for p, g in FRAMES]68    kernels = {q: S.winding_kernel(q, 2) for q in SUBSTRATES}69    triples = {q: S.winding_kernel(q, 3)[0] for q in SUBSTRATES[:3]}70    residuals = {q: S.residual(q) for q in SUBSTRATES}71    sd = S.self_dual_point()72    dual = all(m == (True, True, True) for m in maps)73    pairs = all(kernels[q] == (q, True) for q in SUBSTRATES) and all(triples[q] == q ** 2 for q in triples)74    z2 = all(residuals[q] == [0, q // 2] for q in SUBSTRATES) and all((2 * 1) % q != 0 for q in SUBSTRATES)75    point = sd["prod"] == sd["one"] and sd["diff"] == (2, 0) and sd["tanh"] == sd["w"] and sd["quad"] == (0, 0)76    R.check("S1", "the structure's exact content: on the shells 𝔽₁₇ and 𝔽₂₉ (q = 16, 28) the dual map is the quarter-turn transform, "77            "F² = J and F⁴ = I in ℤ_p (34-super C1, Transform.lean); on every substrate q = 16, 28, 40, 52, 88, 100 the two-body "78            "composites of total winding 0 are the q inverse pairs (k, −k), the three-body ones number q² (C3); the charge-2 "79            "condensate leaves the residual {b : 2b ≡ 0 (mod q)} = {0, q/2} ≅ ℤ₂ with the unit vortex confined — the flux "80            "quantum h/2e (C4); in ℤ[√2], (1 + √2)(√2 − 1) = 1, (1 + √2) − (√2 − 1) = 2, (2 + √2)(√2 − 1) = √2 and "81            "x² − 2x − 1 = 0 at x = 1 + √2: sinh 2β* = 1, tanh β* = √2 − 1 and τ(β*) = ln 1 = 0 at β* = ½ ln(1 + √2), the "82            "Kramers–Wannier self-dual point (C5)",83            dual and pairs and z2 and point,84            f"F² = J, F⁴ = I on {[p for p, _ in FRAMES]}; kernels {dict((q, kernels[q][0]) for q in SUBSTRATES)}; residuals {residuals[16]}, {residuals[100]}; "85            f"(1+√2)(√2−1) = {sd['prod']}, tanh β* = {sd['tanh']} = √2 − 1")86    # S2 chart: the tension τ(β) = 2β + ln tanh β in floating point (m2, m3), and the universal numbers (m3, m4, m8)87    b = CS.beta_star(); r = CS.self_dual_readings(); prof, below = CS.tension_profile(); u = CS.universal_numbers()88    tiny, milli = Q(1, 10 ** 12), Q(1, 1000)89    tension = (_near(Q(r["sinh"]), 0, tiny) and _near(Q(r["tanh"]), 0, tiny) and _near(Q(r["tau0"]), 0, tiny)90               and all(v > 0 for v in prof) and all(prof[i + 1] > prof[i] for i in range(len(prof) - 1)) and below < 091               and _near(Q(r["tau8"]), 0, Q(1, 10 ** 6)))92    involution = all(_near(Q(x), 0, tiny) for x in r["involution"]) and _near(Q(r["fixed"]), 0, tiny) and r["swap"] < 093    numbers = _near(Q(u["jump"]), Q("0.6366197723675813"), tiny) and _near(Q(u["gap_ratio"]), Q(CS.GAP_RATIO_BCS), milli) and _near(Q(u["heat_jump"]), Q(CS.HEAT_JUMP_BCS), milli)94    R.check("S2", "[chart] β* = ½ ln(1 + √2) = 0.4407 in floating point: sinh 2β* = 1, tanh β* = √2 − 1 and τ(β*) = 0 to 10⁻¹²; the vortex "95            "line tension τ(β) = 2β + ln tanh β is positive and increasing at β* + 0.001 … β* + 2 and tends to 2β (16 at β = 8), "96            "negative at β* − 0.05: the vortex confined in the superconducting phase, deconfined at β*, which is T_c; the "97            "Kramers–Wannier map sinh 2β sinh 2β̃ = 1 is an involution with β* its fixed point, swapping the two phases; the "98            "universal numbers: the stiffness jump 2/π = 0.6366, the BCS gap ratio 2π/e^γ = 3.528, the heat jump 12/(7ζ(3)) = 1.426",99            tension and involution and numbers,100            f"β* = {CS.fmt(b, '.6f')}, τ(β*) = {CS.fmt(r['tau0'], '.1e')}, τ at β* + 0.2 = {CS.fmt(prof[2], '.4f')}; 2/π = {CS.fmt(u['jump'], '.4f')}, 2π/e^γ = {CS.fmt(u['gap_ratio'], '.4f')}, 12/(7ζ(3)) = {CS.fmt(u['heat_jump'], '.4f')}",101            kind="CHART")102103104# ------------------------------------------------------------------------------------------------------------105# block D: duality (00:G20)106@R.block("D", BLOCKS["D"])107def block_D():108    """Block D — duality: D1 the exact content (EXACT), D2 the ladder's decimal reading (CHART)."""109    # 00:G20 (p00089)110    turns = {q: S.symplectic(q) for q in SUBSTRATES[:2]}111    m = S.metrology()112    brackets = S.airy_ladder(200, 16, [("1.018", "1.019"), ("3.246", "3.247")], [("2.337", "2.338")])113    ev, od, (lo, hi) = brackets114    quarter = all(turns[q] == (True, True, True, True) for q in turns)115    closure = all(v.is_zero() for v in m.values())116    ladder = ev == [(0, 1), (1, 2)] and od == [(0, 1)] and Q("0.687") < lo < hi < Q("0.691") and hi < 1117    R.check("D1", "the duality's exact content: on ℤ_q ⊕ ℤ_q for q = 16 and 28, over every point, S(a, b) = (b, −a) has S² = −I and "118            "S⁴ = I, preserves the Dirac pairing ab′ − a′b (mod q) over every pair of points, and maps the condensate (2, 0) to the "119            "double flux (0, −2) and the unit vortex (0, 1) to the unit charge (1, 0): the Q₄ quarter-turn, charge ↔ flux, "120            "Wilson ↔ 't Hooft (34-super C9); as polynomial identities with e⁻¹ and h⁻¹ as variables, (2e)(h/2e) = h, the "121            "Josephson step V_n = n f/K_J = n(h/2e)f and its S-image, the phase-slip step I_n = n(2e)f, multiply to n²f²h, and "122            "the metrology triangle K_J R_K Q = (2e/h)(h/e²)Q closes on 4 = q_c² for Q = 2e and on 2 for Q = e (C10); Sturm's "123            "count of the even (Neumann) and odd (Dirichlet) finite operators −u″ + x u on N = 200 sites of [0, 16], in exact "124            "rational arithmetic, places one eigenvalue in each of (1.018, 1.019), (2.337, 2.338), (3.246, 3.247), so the vortex-core "125            "ladder has ρ = (E₃ − E₂)/(E₂ − E₁) in (0.687, 0.691) — below the equal spacing 1 of the harmonic minigap (D1)",126            quarter and closure and ladder,127            f"S on q = {list(turns)}: {turns[16]}; closures {[k for k, v in m.items() if v.is_zero()]}; counts {ev}, {od}; ρ in ({CS.fmt(lo, '.4f')}, {CS.fmt(hi, '.4f')})")128    # D2 chart: the ladder by bisection on the float Sturm counts at N = 200 and N = 400, the Airy zeros, the BCS reference129    (e1, e2, e3, rho), zeros = CS.airy_ladder(200, 16); (_, _, _, rho4), _ = CS.airy_ladder(400, 20)130    rz = CS.airy_ratio(); airy = Q("0.690")131    levels = all(_near(Q(e), Q(z), Q(2, 1000)) for e, z in zip((e1, e2, e3), zeros)) and lo < Q(rho) < hi132    reading = _near(Q(rz), airy, Q(1, 1000)) and _near(Q(rho), airy, Q(2, 1000)) and _near(Q(rho4), airy, Q(1, 1000)) and Q(rz) < Q("0.95") and abs(1 - Q(rz)) > Q(1, 4)133    spacing = (e2 - e1) > (e3 - e2) > 0134    R.check("D2", "[chart] the ladder read in floating point: at N = 200 the three levels agree with the Airy zeros |a′₁| = 1.0188, "135            "|a₁| = 2.3381, |a′₂| = 3.2482 to 2 × 10⁻³ and ρ falls inside the exact bracket; from the zeros ρ = 0.690 (34-super's "136            "m6), at N = 400 on [0, 20] ρ = 0.690 to 10⁻³; the spacings shrink (E₂ − E₁ > E₃ − E₂): the confinement reading, "137            "against ρ = 1 of the equally spaced Caroli–de Gennes–Matricon minigap, separated by more than 0.25 — the "138            "vortex-core spectroscopy that decides between them",139            levels and reading and spacing,140            f"E = ({CS.fmt(e1, '.4f')}, {CS.fmt(e2, '.4f')}, {CS.fmt(e3, '.4f')}), ρ = {CS.fmt(rho, '.4f')} (N = 200), {CS.fmt(rho4, '.4f')} (N = 400), {CS.fmt(rz, '.4f')} from the zeros; BCS 1",141            kind="CHART")142143144if __name__ == "__main__":145    blocks = [a for a in sys.argv[1:] if a in R.blocks]146    if blocks:147        for b in blocks: R.run_block(b)148        sys.exit(0 if R.summary(write=False) else 1)149    sys.exit(0 if R.verify_all() else 1)150