extension.py — frc/ledgers/master

1"""master/extension — a ledger file of the master's block C, the Subject: the rows the extension theme proves (the pushes on2C10 and C11, 8 October 2026).34Block C is bound by one file per theme whose key file proves its rows (subject.py, fourier.py, projective.py and this5file). This file binds C10, the two strata of probability (its witness 22:stratum.py), and C11, the uniqueness of the pair6tally on the Q₄ core (its witness 22:gleason.py): the table of keys (generated from7docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the rings, and the checks, which8call the extension theme (frc/extension.py). The Lean side is lean/FrcCore/Theme/Extension.lean for C10 (the strata section;9the extension itself is Theme/Quadratic.lean) and lean/FrcCore/Theme/Tally.lean for C11 (a file of its own), the key file10lean/FrcCore/Keys/Extension.lean and the certificate lean/FrcCore/Ledgers/Master/Extension.lean.1112    python3 -m frc.ledgers.master.extension        every block, the census; exit 1 if a check fails1314Blocks:  T  the two strata of probability: the tally line, the two reductions, the framed readout   EXACT  (00:C10)15         G  the pair tally on the Q₄ core: the character cone fixed by the pure windings, the Born ray EXACT  (00:C11)1617The notebook frc/ledgers/master/extension.ipynb runs one row per cell, the cell's id its key (gate G13).18"""19import random20import itertools21import sys22from fractions import Fraction as Fr23from math import isqrt2425from frc.registry import Registry26from frc.extension import Quad, pair_tally, trace_seq, dial_tally27from frc.shell import generators2829# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----30BLOCK = "C"31KEYS = {"C1": "p00021", "C2": "p00022", "C3": "p00150", "C4": "p00024", "C5": "p00025", "C6": "p00171", "C7": "p00189", "C8": "p00028", "C9": "p00029", "C10": "p00030", "C11": "p22028", "C12": "p00032", "C14": "p00034", "C16": "p00151", "C19": "p00190", "C20": "p00040", "C21": "p00041", "C22": "p00152", "C23": "p00182", "C24": "p13064", "C25": "p00139", "C26": "p00174", "C27": "p00183"}       # every row of the block: its label and its accession key32LEAN = {"C10": "core", "C11": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them33# ---- end of the generated table ----3435# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys36# 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.37PROOFS = {38    "C10": ["FRC.Extension.two_way_tally", "FRC.Extension.core_weights", "FRC.Extension.root_two_two_way",39            "FRC.Extension.conjugate_pair_tally", "FRC.Extension.trace_recurrence", "FRC.Extension.dial_shift",40            "FRC.Extension.dial_tally", "FRC.Extension.framed_readout"],41    "C11": ["FRC.Extension.Tally.winding_fixing", "FRC.Extension.Tally.tally_criterion", "FRC.Extension.Tally.two_way",42            "FRC.Extension.Tally.fourier_inversion", "FRC.Extension.Tally.channel_selectivity", "FRC.Extension.Tally.dft_det",43            "FRC.Extension.Tally.cone_boundary", "FRC.Extension.Tally.linear_exclusion"],44}4546LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none4748LEDGER = {"T1": "00:C10", "T2": "00:C10", "T3": "00:C10", "T4": "00:C10", "T5": "00:C10",49          "G1": "00:C11", "G2": "00:C11", "G3": "00:C11", "G4": "00:C11"}50BLOCKS = {"T": "the two strata of probability: the tally line, the two reductions, the framed readout",51          "G": "the pair tally on the Q₄ core: the character cone fixed by the pure windings, the Born ray"}52PREDICATES = {"00:C10": "T1", "00:C11": "G1"}5354R = Registry("00", "extension", LEDGER, PREDICATES, sources=[__file__])555657def readout(m, g, n):58    """The framed readout of √m at scale n on the chart of generator g: s = ⌊√(m g^{2n})⌋, s² ≤ m g^{2n} < (s + 1)²,59    the registered value s / gⁿ (22-quantum, Def. readout)."""60    return isqrt(m * g ** (2 * n))616263def largest_remainder(ps, B):64    """B counts allocated to the probabilities ps (Fractions summing to 1): the floors, then one count each to the65    largest remainders, ties by index."""66    prov = [int(B * q) for q in ps]67    rem = [B * q - v for q, v in zip(ps, prov)]68    counts = prov[:]69    for i in sorted(range(len(ps)), key=lambda i: (-rem[i], i))[:B - sum(prov)]: counts[i] += 170    return counts717273# ------------------------------------------------------------------------------------------------------------74# block T: the two strata of probability (00:C10; 22-quantum prop:strata, the witness 22:stratum.py S1, S2, S4–S7, S9, S10)75# a structural weight is an element of a quadratic ring ℤ[w]/(w² − ν) or 𝔽_p[w]/(w² − ν) (Quad); a registered value76# lies on the tally line (a, 0), the part fixed by the ring's conjugation. The paper's two-way subring is the part of the77# cyclotomic ring fixed by ζ ↦ ζ⁻¹: the tally line of ℤ[i], and for ν = 2 it holds w = √2 = ζ₈ + ζ₈⁻¹ itself, so the78# engineered-core weights 2 ± w are two-way and w ↦ −w is the conjugate-pair involution W₊ ↔ W₋. The two reductions79# that join the strata on the stationary core-valued sector: the conjugate-pair trace tally80# z^k z̄^(k+m) + z̄^k z^(k+m) = (N(z)^k · tr(z^m), 0), with the trace recurrence t_{m+2} + N t_m = tr · t_{m+1} and the81# dial-shift conjugation w₊(M − θ) = w₋(θ); and the dial-ensemble Parseval tally Σ_θ w± = Σ_θ w₊ w₋ = 2N over a dial of82# N settings. The engineered-core weights W± = 2 ± w, w² = 2: W₊ + W₋ = 4, W₊ W₋ = 2, on Ω = 641 as residues, r = 67 a83# grid point 3⁵⁵⁵ of the Subject chart. The framed readout: s_n = ⌊√(2 · 9ⁿ)⌋, R_4 = 23/54, the largest-remainder84# allocation at B = 81, a computation over the naturals of the laboratory host in which the paper's Carrier Ω = 641 is85# observed (decision Q20), not a count of the totality (Extension.lean: two_way_tally, core_weights, root_two_two_way,86# conjugate_pair_tally, trace_recurrence, dial_shift, dial_tally, framed_readout).87@R.block("T", BLOCKS["T"])88def block_T():89    """Block T — the two strata of probability (EXACT): T1–T5."""90    # 00:C10 (p00030)91    # T1 the tally line (S1): the conjugation-fixed part of ℤ[i], ℤ[√2], ℤ[√3] and of 𝔽_p[w]/(w² − ν) is the line b = 0;92    # z + z̄ = (tr z, 0); for ℤ[i] this is the paper's two-way subring93    bad = []94    for Q in (Quad(-1), Quad(2), Quad(3)):95        for a in range(-6, 7):96            for b in range(-6, 7):97                z = Q.el(a, b)98                if (Q.conj(z) == z) != (b == 0) or Q.add(z, Q.conj(z)) != Q.el(Q.trace(z)): bad.append((Q.nu, a, b))99    for p, nu in ((13, 2), (641, 2), (101, 5), (17, 3)):100        Q = Quad(nu, p)101        for a in range(p):102            for b in range(p):103                z = (a, b)104                if (Q.conj(z) == z) != (b == 0) or Q.add(z, Q.conj(z)) != Q.el(Q.trace(z)): bad.append((p, nu, a, b)); break105    R.check("T1", "the part of ℤ[i], ℤ[√2], ℤ[√3] (exhaustive |a|, |b| ≤ 6) and of 𝔽_p[w]/(w² − ν), (p, ν) = (13, 2), (641, 2), (101, 5), "106            "(17, 3) (every element), fixed by the ring's conjugation is the tally line b = 0, and z + z̄ = (tr z, 0); for ℤ[i] the "107            "tally line is the paper's two-way subring", not bad, f"exceptions {bad[:3]}")108    # T2 the engineered-core weights (S2, S4): W± = 2 ± w in 𝔽_p[w]/(w² − 2) and on Ω = 641 as residues, r = 67 = 3⁵⁵⁵,109    # a grid point of the Subject chart (S4); w = ζ₈ + ζ₈⁻¹ is two-way, (ζ₈ + ζ₈⁻¹)² = 2 for every ζ₈ of order 8110    Om = 641111    r = next(x for x in range(1, Om) if x * x % Om == 2)112    Wp, Wm = (2 + r) % Om, (2 - r) % Om113    ok = Om % 8 == 1 and r == 67 and (Wp + Wm) % Om == 4 and Wp * Wm % Om == 2 and pow(3, 555, Om) == r114    ok &= all(pow(3, k, Om) != r for k in range(555))                                                    # the least exponent115    for p in (None, 7, 13, 641, 1373):116        Q = Quad(2, p); W = Q.el(2, 1); Wb = Q.conj(W)117        ok &= Q.add(W, Wb) == Q.el(4) and Q.mul(W, Wb) == Q.el(2) and Q.trace(W) == Q.red(4) and Q.norm(W) == Q.red(2)118    n8 = 0119    for q in (17, 41, 97, 641, 1289):120        for z in range(2, q):121            if pow(z, 8, q) == 1 and pow(z, 4, q) != 1:122                n8 += 1; c = (z + pow(z, q - 2, q)) % q123                ok &= c * c % q == 2124    ok &= (318 + pow(318, 639, 641)) % 641 == 641 - 67125    R.check("T2", "641 ≡ 1 (mod 8), r = 67 = 3⁵⁵⁵ (the least exponent), r² = 2: the engineered-core weights W± = 2 ± r are residues with "126            "W₊ + W₋ = 4 and W₊ W₋ = 2; in ℤ[√2] and in 𝔽_p[w]/(w² − 2), p = 7, 13, 641, 1373: W₊ + W̄₊ = (4, 0), W₊ W̄₊ = (2, 0), "127            f"tr W₊ = 4, N(W₊) = 2; for every ζ₈ of order 8 in 𝔽_q, q = 17, 41, 97, 641, 1289 ({n8} of them): (ζ₈ + ζ₈⁻¹)² = 2, so "128            "w = ζ₈ + ζ₈⁻¹ is two-way; on 641, ζ₈ = 318 gives ζ₈ + ζ₈⁻¹ = −67",129            ok, f"r = {r}, W± = {Wp}, {Wm}")130    # T3 the conjugate-pair trace tally (S9): in ℤ[√2] for B ≤ 12 verbatim, and for every weight z of ℤ[√ν]131    Q = Quad(2); W = Q.el(2, 1)132    t = trace_seq(Q, W, 14)133    ok = t[:4] == [2, 4, 12, 40] and all(t[m + 2] + 2 * t[m] == 4 * t[m + 1] for m in range(12))134    Wb = Q.conj(W)135    ok &= all(Q.add(Q.mul(Q.pow(W, k), Q.pow(Wb, B - k)), Q.mul(Q.pow(Wb, k), Q.pow(W, B - k))) == (2 ** min(k, B - k) * t[abs(B - 2 * k)], 0)136              for B in range(1, 13) for k in range(B + 1))137    rng = random.Random(30); n_pairs = 0138    for nu in (-1, 2, 3, 5, -3):139        Qn = Quad(nu)140        for _ in range(40):141            z = Qn.el(rng.randrange(-5, 6), rng.randrange(-5, 6))142            tz = trace_seq(Qn, z, 8); N = Qn.norm(z)143            ok &= all(tz[m + 2] + N * tz[m] == tz[1] * tz[m + 1] for m in range(6))144            for k in range(4):145                for m in range(4):146                    lhs, rhs = pair_tally(Qn, z, k, m); n_pairs += 1147                    ok &= lhs == rhs and Qn.on_line(lhs)148    R.check("T3", "the conjugate-pair trace tally in ℤ[√2]: W₊^k W₋^(B−k) + W₋^k W₊^(B−k) = 2^min(k, B−k) t_|B−2k| for B ≤ 12 and every k ≤ B, "149            f"t = 2, 4, 12, 40, …, t_(m+2) = 4 t_(m+1) − 2 t_m; for 200 draws of a weight z of ℤ[√ν], ν = −1, 2, 3, 5, −3, and k, m < 4 "150            f"({n_pairs} evaluations): z^k z̄^(k+m) + z̄^k z^(k+m) = (N(z)^k tr(z^m), 0) on the tally line, and t_(m+2) + N t_m = tr(z) t_(m+1)", ok)151    # T4 the dial-shift conjugation (S9) and the dial-ensemble Parseval tally (S10): in ℤ[x]/(x^40 + 1) verbatim, and in 𝔽_q with ζ of order N152    def vec(e):153        e %= 80; v = [0] * 40154        if e < 40: v[e] += 1155        else: v[e - 40] -= 1156        return v157    vadd = lambda a, b: [x + y for x, y in zip(a, b)]158    def vmul(a, b):159        out = [0] * 40160        for i, ai in enumerate(a):161            if ai:162                for j, bj in enumerate(b):163                    if bj:164                        if i + j < 40: out[i + j] += ai * bj165                        else: out[i + j - 40] -= ai * bj166        return out167    one = vec(0); sp = sm = spm = [0] * 40168    for D in range(80):169        c = vadd(vec(D), vec(-D))170        wp, wm = vadd([2 * x for x in one], c), vadd([2 * x for x in one], [-x for x in c])171        sp, sm, spm = vadd(sp, wp), vadd(sm, wm), vadd(spm, vmul(wp, wm))172    ok = sp == sm == spm == [160 * x for x in one]173    ok &= all(vadd(vec(40 - D), vec(D - 40)) == [-x for x in vadd(vec(D), vec(-D))] for D in range(80))          # w₊(40 − D) = w₋(D)174    for q, N in ((241, 80), (241, 240), (13, 12), (41, 5), (1373, 28), (641, 80)):175        ok &= dial_tally(q, N) == ((2 * N) % q,) * 3176        if N % 2 == 0:                                                                                           # the dial shift in the shell177            M = N // 2178            z = pow(generators(q)[0], (q - 1) // N, q); zi = pow(z, q - 2, q)                                   # ζ of order N179            ok &= all((2 + pow(z, M - t, q) + pow(zi, M - t, q)) % q == (2 - pow(z, t, q) - pow(zi, t, q)) % q for t in range(M + 1))180    R.check("T4", "the dial-shift conjugation w₊(40 − D) = w₋(D) and the dial-ensemble Parseval tally over ℤ_80 in ℤ[x]/(x^40 + 1): "181            "Σ w₊ = Σ w₋ = Σ w₊ w₋ = 160 exactly; in 𝔽_q with ζ of order N, (q, N) = (241, 80), (241, 240), (13, 12), (41, 5), (1373, 28), "182            "(641, 80): the three sums are 2N, and for even N the shift by N/2 conjugates the weight", ok)183    # T5 the framed readout (S5–S7): the grid bound, the nesting, R_4 = 23/54, the √3 instance, the allocation at B = 81;184    # a computation over the naturals of the laboratory host (Q20)185    g = 3186    s = [readout(2, g, n) for n in range(9)]187    ok = s == [1, 4, 12, 38, 114, 343, 1030, 3092, 9278]188    ok &= all(s[n] ** 2 <= 2 * g ** (2 * n) < (s[n] + 1) ** 2 for n in range(9))189    ok &= all(0 <= s[n + 1] - g * s[n] <= g - 1 for n in range(8))190    ok &= Fr(2 * g ** 4 + s[4], 8 * g ** 4) == Fr(23, 54) and readout(3, g, 3) == 46191    probs = [Fr(23, 54), Fr(23, 54), Fr(2, 27), Fr(2, 27)]192    ok &= sum(probs) == 1 and largest_remainder(probs, 81) == [35, 34, 6, 6]193    R.check("T5", "the framed readout on the chart g = 3, over the naturals of the laboratory host: s_n = ⌊√(2 · 9ⁿ)⌋ = 1, 4, 12, 38, 114, 343, "194            "1030, 3092, 9278 with s_n² ≤ 2 · 9ⁿ < (s_n + 1)² and 0 ≤ s_(n+1) − 3 s_n ≤ 2; R_4((2 + √2)/8) = (2 · 81 + 114)/(8 · 81) = 23/54; "195            "s_3(√3) = 46; the largest-remainder allocation of (23/54, 23/54, 2/27, 2/27) at B = 81 is 35 + 34 + 6 + 6", ok, f"s = {s}")196197198# ------------------------------------------------------------------------------------------------------------199# block G: the pair tally on the Q₄ core (00:C11; 22-quantum Prop. gleason, 22:gleason.py)200# kernels K: Q₄ → ℤ[i], two-way (K(−d) = conj K(d)), tally-valued; the admissible kernels are the tally combinations201# K_c = Σ_r c_r η_r of the four characters η_r(d) = i^{rd}; the pair tally F(K, ψ) = Σ_{u,v} K(v − u) ψ_u conj ψ_v on202# the pure winding ψ_k reads the coefficient, F(K_c, ψ_k) = 16 c_k (the tallies fixed in-sector); Fourier inversion203# recovers c; channel-selectivity (one responding channel) is a scaled unit vector, the Born ray; the core DFT has204# determinant −16i; a linear functional and an unconjugated bilinear form leave the tally cone (Theme/Tally.lean:205# winding_fixing and tally_criterion on the box −1..3, two_way, fourier_inversion and channel_selectivity on the cube206# 0..3, cone_boundary, dft_det, linear_exclusion — exhausted by the kernel).207@R.block("G", BLOCKS["G"])208def block_G():209    """Block G — the pair tally on the Q₄ core (EXACT): G1–G4."""210    from frc.extension import GI, ipow, q4_kernel, q4_winding, q4_tally, q4_inversion, q4_bilinear, q4_dft_det211    cube = list(itertools.product(range(4), repeat=4))212    box = list(itertools.product(range(-1, 4), repeat=4))213    # 00:C11 (p22028)214    ok, n = True, 0215    for c in box:216        K = q4_kernel(c)217        for k in range(4):218            n += 1219            val = q4_tally(K, q4_winding(k))220            ok &= val == GI.el(16 * c[k]) and ((GI.on_line(val) and val[0] >= 0) == (c[k] >= 0))221    neg = q4_tally(q4_kernel((1, -1, 1, 0)), q4_winding(1))222    R.check("G1", "the pure windings fix the tallies on the box −1..3 (negative coefficients included): F(K_c, ψ_k) = 16 c_k for "223            "every kernel and every channel k, and the value is a tally (a nonnegative integer) iff c_k ≥ 0 — on the box, a "224            "tally-valued functional is a nonnegative combination of the characters, and a negative c₁ is excluded by its own "225            "winding, F = −16", ok and neg == GI.el(-16), f"{n} evaluations on {len(box)} kernels; F(K_(1,−1,1,0), ψ₁) = {neg}")226    # G2 two-way and tally-valued on the windings; Fourier inversion recovers c227    ok = True228    for c in cube:229        K = q4_kernel(c)230        ok &= all(K[(-d) % 4] == GI.conj(K[d]) for d in range(4))231        ok &= all(GI.on_line(q4_tally(K, q4_winding(k))) and q4_tally(K, q4_winding(k))[0] >= 0 for k in range(4))232        ok &= all(q4_inversion(K, r) == GI.el(4 * c[r]) for r in range(4))233    R.check("G2", "every kernel of the cube is two-way, K(−d) = conj K(d), tally-valued on the four windings, and Fourier "234            "inversion Σ_d K(d) i^{−rd} = 4 c_r recovers every coefficient exactly", ok, f"{len(cube)} kernels")235    # G3 channel-selectivity picks the ray: one responding channel iff a scaled unit coefficient vector; the fibre norm236    # K = [d = 0] responds on all four channels with c_r = 1/4 (no tally), the counterexample the clause excludes237    ok = True238    for c in cube:239        K = q4_kernel(c)240        single = sum(1 for k in range(4) if q4_tally(K, q4_winding(k)) != GI.el(0)) == 1241        ok &= single == (sum(1 for x in c if x) == 1)242    Kfn = [GI.el(1), GI.el(0), GI.el(0), GI.el(0)]243    resp = [q4_tally(Kfn, q4_winding(k)) for k in range(4)]244    inv = [q4_inversion(Kfn, r) for r in range(4)]245    ok &= resp == [GI.el(4)] * 4 and inv == [GI.el(1)] * 4246    R.check("G3", "channel-selectivity: a kernel of the cube responds on exactly one channel iff its coefficient vector is a scaled "247            "unit vector e_r (the Born ray); the fibre norm [d = 0] satisfies the first four clauses, responds (4, 4, 4, 4) with "248            "4 c_r = 1 each, and fails selectivity", ok, f"fibre norm: responses {[x[0] for x in resp]}")249    # G4 the core DFT is invertible (det −16i: the windings span the fibre, polarisation pins the kernel) and the250    # minimal degree is forced: a linear functional vanishes on the nontrivial windings and, on the trivial one,251    # F(i ψ₀) = i F(ψ₀) leaves the tally cone for every nonzero multiplier252    det = q4_dft_det()253    ok = det == GI.el(0, -16)254    ok &= all(sum(ipow(k * u)[0] for u in range(4)) == 0 and sum(ipow(k * u)[1] for u in range(4)) == 0 for k in range(1, 4))255    ok &= all(not GI.on_line(GI.mul(GI.el(0, 1), GI.el(4 * c))) for c in range(1, 5))256    # the unconjugated bilinear form leaves the tally line on Gaussian-lattice states where the conjugated form stays257    psi_a = [GI.el(1, 1), GI.el(0), GI.el(0), GI.el(0)]                 # (1 + i) e₀258    psi_b = [GI.el(1), GI.el(0, 1), GI.el(0), GI.el(0)]                 # e₀ + i e₁259    shift = [GI.el(0), GI.el(1), GI.el(0), GI.el(0)]                    # [d = 1]260    bil = (q4_bilinear(Kfn, psi_a) == GI.el(0, 2) and q4_tally(Kfn, psi_a) == GI.el(2)261           and q4_bilinear(shift, psi_b) == GI.el(0, 1) and q4_bilinear(q4_kernel((1, 1, 0, 0)), psi_a) == GI.el(0, 4)262           and q4_tally(q4_kernel((1, 1, 0, 0)), psi_a) == GI.el(4))263    ok &= bil264    seen, pol = {}, True265    for c in itertools.product(range(3), repeat=4):266        K = q4_kernel(c)267        key = tuple(q4_tally(K, q4_winding(k)) for k in range(4))268        if key in seen and seen[key] != tuple(K): pol = False269        seen[key] = tuple(K)270    R.check("G4", "the core DFT (i^{ru}) has determinant −16i, so the windings span the fibre and equal responses force equal "271            "kernels (exhaustive on 0..2); the minimal degree is forced: the complete character sums vanish on k = 1, 2, 3, "272            "i · (4c, 0) = (0, 4c) is no tally for c = 1..4, and the unconjugated bilinear form leaves the tally line — "273            "B([d=0], (1+i)e₀) = 2i against F = 2, B([d=1], e₀+ie₁) = i, B(K_(1,1,0,0), (1+i)e₀) = 4i against F = 4",274            ok and pol, f"det = {det}, {len(seen)} response patterns")275276277if __name__ == "__main__":278    blocks = [a for a in sys.argv[1:] if a in R.blocks]279    if blocks:280        for b in blocks: R.run_block(b)281        sys.exit(0 if R.summary(write=False) else 1)282    sys.exit(0 if R.verify_all() else 1)283