"""master/extension — a ledger file of the master's block C, the Subject: the rows the extension theme proves (the pushes on
C10 and C11, 8 October 2026).

Block C is bound by one file per theme whose key file proves its rows (subject.py, fourier.py, projective.py and this
file). This file binds C10, the two strata of probability (its witness 22:stratum.py), and C11, the uniqueness of the pair
tally on the Q₄ core (its witness 22:gleason.py): the table of keys (generated from
docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the rings, and the checks, which
call the extension theme (frc/extension.py). The Lean side is lean/FrcCore/Theme/Extension.lean for C10 (the strata section;
the extension itself is Theme/Quadratic.lean) and lean/FrcCore/Theme/Tally.lean for C11 (a file of its own), the key file
lean/FrcCore/Keys/Extension.lean and the certificate lean/FrcCore/Ledgers/Master/Extension.lean.

    python3 -m frc.ledgers.master.extension        every block, the census; exit 1 if a check fails

Blocks:  T  the two strata of probability: the tally line, the two reductions, the framed readout   EXACT  (00:C10)
         G  the pair tally on the Q₄ core: the character cone fixed by the pure windings, the Born ray EXACT  (00:C11)

The notebook frc/ledgers/master/extension.ipynb runs one row per cell, the cell's id its key (gate G13).
"""
import random
import itertools
import sys
from fractions import Fraction as Fr
from math import isqrt

from frc.registry import Registry
from frc.extension import Quad, pair_tally, trace_seq, dial_tally
from frc.shell import generators

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "C"
KEYS = {"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 key
LEAN = {"C10": "core", "C11": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them
# ---- end of the generated table ----

# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys
# 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.
PROOFS = {
    "C10": ["FRC.Extension.two_way_tally", "FRC.Extension.core_weights", "FRC.Extension.root_two_two_way",
            "FRC.Extension.conjugate_pair_tally", "FRC.Extension.trace_recurrence", "FRC.Extension.dial_shift",
            "FRC.Extension.dial_tally", "FRC.Extension.framed_readout"],
    "C11": ["FRC.Extension.Tally.winding_fixing", "FRC.Extension.Tally.tally_criterion", "FRC.Extension.Tally.two_way",
            "FRC.Extension.Tally.fourier_inversion", "FRC.Extension.Tally.channel_selectivity", "FRC.Extension.Tally.dft_det",
            "FRC.Extension.Tally.cone_boundary", "FRC.Extension.Tally.linear_exclusion"],
}

LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none

LEDGER = {"T1": "00:C10", "T2": "00:C10", "T3": "00:C10", "T4": "00:C10", "T5": "00:C10",
          "G1": "00:C11", "G2": "00:C11", "G3": "00:C11", "G4": "00:C11"}
BLOCKS = {"T": "the two strata of probability: the tally line, the two reductions, the framed readout",
          "G": "the pair tally on the Q₄ core: the character cone fixed by the pure windings, the Born ray"}
PREDICATES = {"00:C10": "T1", "00:C11": "G1"}

R = Registry("00", "extension", LEDGER, PREDICATES, sources=[__file__])


def readout(m, g, n):
    """The framed readout of √m at scale n on the chart of generator g: s = ⌊√(m g^{2n})⌋, s² ≤ m g^{2n} < (s + 1)²,
    the registered value s / gⁿ (22-quantum, Def. readout)."""
    return isqrt(m * g ** (2 * n))


def largest_remainder(ps, B):
    """B counts allocated to the probabilities ps (Fractions summing to 1): the floors, then one count each to the
    largest remainders, ties by index."""
    prov = [int(B * q) for q in ps]
    rem = [B * q - v for q, v in zip(ps, prov)]
    counts = prov[:]
    for i in sorted(range(len(ps)), key=lambda i: (-rem[i], i))[:B - sum(prov)]: counts[i] += 1
    return counts


# ------------------------------------------------------------------------------------------------------------
# block T: the two strata of probability (00:C10; 22-quantum prop:strata, the witness 22:stratum.py S1, S2, S4–S7, S9, S10)
# a structural weight is an element of a quadratic ring ℤ[w]/(w² − ν) or 𝔽_p[w]/(w² − ν) (Quad); a registered value
# 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 the
# cyclotomic ring fixed by ζ ↦ ζ⁻¹: the tally line of ℤ[i], and for ν = 2 it holds w = √2 = ζ₈ + ζ₈⁻¹ itself, so the
# engineered-core weights 2 ± w are two-way and w ↦ −w is the conjugate-pair involution W₊ ↔ W₋. The two reductions
# that join the strata on the stationary core-valued sector: the conjugate-pair trace tally
# 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 the
# dial-shift conjugation w₊(M − θ) = w₋(θ); and the dial-ensemble Parseval tally Σ_θ w± = Σ_θ w₊ w₋ = 2N over a dial of
# N settings. The engineered-core weights W± = 2 ± w, w² = 2: W₊ + W₋ = 4, W₊ W₋ = 2, on Ω = 641 as residues, r = 67 a
# grid point 3⁵⁵⁵ of the Subject chart. The framed readout: s_n = ⌊√(2 · 9ⁿ)⌋, R_4 = 23/54, the largest-remainder
# allocation at B = 81, a computation over the naturals of the laboratory host in which the paper's Carrier Ω = 641 is
# observed (decision Q20), not a count of the totality (Extension.lean: two_way_tally, core_weights, root_two_two_way,
# conjugate_pair_tally, trace_recurrence, dial_shift, dial_tally, framed_readout).
@R.block("T", BLOCKS["T"])
def block_T():
    """Block T — the two strata of probability (EXACT): T1–T5."""
    # 00:C10 (p00030)
    # T1 the tally line (S1): the conjugation-fixed part of ℤ[i], ℤ[√2], ℤ[√3] and of 𝔽_p[w]/(w² − ν) is the line b = 0;
    # z + z̄ = (tr z, 0); for ℤ[i] this is the paper's two-way subring
    bad = []
    for Q in (Quad(-1), Quad(2), Quad(3)):
        for a in range(-6, 7):
            for b in range(-6, 7):
                z = Q.el(a, b)
                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))
    for p, nu in ((13, 2), (641, 2), (101, 5), (17, 3)):
        Q = Quad(nu, p)
        for a in range(p):
            for b in range(p):
                z = (a, b)
                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)); break
    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), "
            "(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 "
            "tally line is the paper's two-way subring", not bad, f"exceptions {bad[:3]}")
    # T2 the engineered-core weights (S2, S4): W± = 2 ± w in 𝔽_p[w]/(w² − 2) and on Ω = 641 as residues, r = 67 = 3⁵⁵⁵,
    # a grid point of the Subject chart (S4); w = ζ₈ + ζ₈⁻¹ is two-way, (ζ₈ + ζ₈⁻¹)² = 2 for every ζ₈ of order 8
    Om = 641
    r = next(x for x in range(1, Om) if x * x % Om == 2)
    Wp, Wm = (2 + r) % Om, (2 - r) % Om
    ok = Om % 8 == 1 and r == 67 and (Wp + Wm) % Om == 4 and Wp * Wm % Om == 2 and pow(3, 555, Om) == r
    ok &= all(pow(3, k, Om) != r for k in range(555))                                                    # the least exponent
    for p in (None, 7, 13, 641, 1373):
        Q = Quad(2, p); W = Q.el(2, 1); Wb = Q.conj(W)
        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)
    n8 = 0
    for q in (17, 41, 97, 641, 1289):
        for z in range(2, q):
            if pow(z, 8, q) == 1 and pow(z, 4, q) != 1:
                n8 += 1; c = (z + pow(z, q - 2, q)) % q
                ok &= c * c % q == 2
    ok &= (318 + pow(318, 639, 641)) % 641 == 641 - 67
    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 "
            "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), "
            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 "
            "w = ζ₈ + ζ₈⁻¹ is two-way; on 641, ζ₈ = 318 gives ζ₈ + ζ₈⁻¹ = −67",
            ok, f"r = {r}, W± = {Wp}, {Wm}")
    # T3 the conjugate-pair trace tally (S9): in ℤ[√2] for B ≤ 12 verbatim, and for every weight z of ℤ[√ν]
    Q = Quad(2); W = Q.el(2, 1)
    t = trace_seq(Q, W, 14)
    ok = t[:4] == [2, 4, 12, 40] and all(t[m + 2] + 2 * t[m] == 4 * t[m + 1] for m in range(12))
    Wb = Q.conj(W)
    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)
              for B in range(1, 13) for k in range(B + 1))
    rng = random.Random(30); n_pairs = 0
    for nu in (-1, 2, 3, 5, -3):
        Qn = Quad(nu)
        for _ in range(40):
            z = Qn.el(rng.randrange(-5, 6), rng.randrange(-5, 6))
            tz = trace_seq(Qn, z, 8); N = Qn.norm(z)
            ok &= all(tz[m + 2] + N * tz[m] == tz[1] * tz[m + 1] for m in range(6))
            for k in range(4):
                for m in range(4):
                    lhs, rhs = pair_tally(Qn, z, k, m); n_pairs += 1
                    ok &= lhs == rhs and Qn.on_line(lhs)
    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, "
            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 "
            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)
    # 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 N
    def vec(e):
        e %= 80; v = [0] * 40
        if e < 40: v[e] += 1
        else: v[e - 40] -= 1
        return v
    vadd = lambda a, b: [x + y for x, y in zip(a, b)]
    def vmul(a, b):
        out = [0] * 40
        for i, ai in enumerate(a):
            if ai:
                for j, bj in enumerate(b):
                    if bj:
                        if i + j < 40: out[i + j] += ai * bj
                        else: out[i + j - 40] -= ai * bj
        return out
    one = vec(0); sp = sm = spm = [0] * 40
    for D in range(80):
        c = vadd(vec(D), vec(-D))
        wp, wm = vadd([2 * x for x in one], c), vadd([2 * x for x in one], [-x for x in c])
        sp, sm, spm = vadd(sp, wp), vadd(sm, wm), vadd(spm, vmul(wp, wm))
    ok = sp == sm == spm == [160 * x for x in one]
    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)
    for q, N in ((241, 80), (241, 240), (13, 12), (41, 5), (1373, 28), (641, 80)):
        ok &= dial_tally(q, N) == ((2 * N) % q,) * 3
        if N % 2 == 0:                                                                                           # the dial shift in the shell
            M = N // 2
            z = pow(generators(q)[0], (q - 1) // N, q); zi = pow(z, q - 2, q)                                   # ζ of order N
            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))
    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): "
            "Σ w₊ = Σ w₋ = Σ w₊ w₋ = 160 exactly; in 𝔽_q with ζ of order N, (q, N) = (241, 80), (241, 240), (13, 12), (41, 5), (1373, 28), "
            "(641, 80): the three sums are 2N, and for even N the shift by N/2 conjugates the weight", ok)
    # T5 the framed readout (S5–S7): the grid bound, the nesting, R_4 = 23/54, the √3 instance, the allocation at B = 81;
    # a computation over the naturals of the laboratory host (Q20)
    g = 3
    s = [readout(2, g, n) for n in range(9)]
    ok = s == [1, 4, 12, 38, 114, 343, 1030, 3092, 9278]
    ok &= all(s[n] ** 2 <= 2 * g ** (2 * n) < (s[n] + 1) ** 2 for n in range(9))
    ok &= all(0 <= s[n + 1] - g * s[n] <= g - 1 for n in range(8))
    ok &= Fr(2 * g ** 4 + s[4], 8 * g ** 4) == Fr(23, 54) and readout(3, g, 3) == 46
    probs = [Fr(23, 54), Fr(23, 54), Fr(2, 27), Fr(2, 27)]
    ok &= sum(probs) == 1 and largest_remainder(probs, 81) == [35, 34, 6, 6]
    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, "
            "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; "
            "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}")


# ------------------------------------------------------------------------------------------------------------
# block G: the pair tally on the Q₄ core (00:C11; 22-quantum Prop. gleason, 22:gleason.py)
# kernels K: Q₄ → ℤ[i], two-way (K(−d) = conj K(d)), tally-valued; the admissible kernels are the tally combinations
# 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 on
# the pure winding ψ_k reads the coefficient, F(K_c, ψ_k) = 16 c_k (the tallies fixed in-sector); Fourier inversion
# recovers c; channel-selectivity (one responding channel) is a scaled unit vector, the Born ray; the core DFT has
# determinant −16i; a linear functional and an unconjugated bilinear form leave the tally cone (Theme/Tally.lean:
# winding_fixing and tally_criterion on the box −1..3, two_way, fourier_inversion and channel_selectivity on the cube
# 0..3, cone_boundary, dft_det, linear_exclusion — exhausted by the kernel).
@R.block("G", BLOCKS["G"])
def block_G():
    """Block G — the pair tally on the Q₄ core (EXACT): G1–G4."""
    from frc.extension import GI, ipow, q4_kernel, q4_winding, q4_tally, q4_inversion, q4_bilinear, q4_dft_det
    cube = list(itertools.product(range(4), repeat=4))
    box = list(itertools.product(range(-1, 4), repeat=4))
    # 00:C11 (p22028)
    ok, n = True, 0
    for c in box:
        K = q4_kernel(c)
        for k in range(4):
            n += 1
            val = q4_tally(K, q4_winding(k))
            ok &= val == GI.el(16 * c[k]) and ((GI.on_line(val) and val[0] >= 0) == (c[k] >= 0))
    neg = q4_tally(q4_kernel((1, -1, 1, 0)), q4_winding(1))
    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 "
            "every kernel and every channel k, and the value is a tally (a nonnegative integer) iff c_k ≥ 0 — on the box, a "
            "tally-valued functional is a nonnegative combination of the characters, and a negative c₁ is excluded by its own "
            "winding, F = −16", ok and neg == GI.el(-16), f"{n} evaluations on {len(box)} kernels; F(K_(1,−1,1,0), ψ₁) = {neg}")
    # G2 two-way and tally-valued on the windings; Fourier inversion recovers c
    ok = True
    for c in cube:
        K = q4_kernel(c)
        ok &= all(K[(-d) % 4] == GI.conj(K[d]) for d in range(4))
        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))
        ok &= all(q4_inversion(K, r) == GI.el(4 * c[r]) for r in range(4))
    R.check("G2", "every kernel of the cube is two-way, K(−d) = conj K(d), tally-valued on the four windings, and Fourier "
            "inversion Σ_d K(d) i^{−rd} = 4 c_r recovers every coefficient exactly", ok, f"{len(cube)} kernels")
    # G3 channel-selectivity picks the ray: one responding channel iff a scaled unit coefficient vector; the fibre norm
    # K = [d = 0] responds on all four channels with c_r = 1/4 (no tally), the counterexample the clause excludes
    ok = True
    for c in cube:
        K = q4_kernel(c)
        single = sum(1 for k in range(4) if q4_tally(K, q4_winding(k)) != GI.el(0)) == 1
        ok &= single == (sum(1 for x in c if x) == 1)
    Kfn = [GI.el(1), GI.el(0), GI.el(0), GI.el(0)]
    resp = [q4_tally(Kfn, q4_winding(k)) for k in range(4)]
    inv = [q4_inversion(Kfn, r) for r in range(4)]
    ok &= resp == [GI.el(4)] * 4 and inv == [GI.el(1)] * 4
    R.check("G3", "channel-selectivity: a kernel of the cube responds on exactly one channel iff its coefficient vector is a scaled "
            "unit vector e_r (the Born ray); the fibre norm [d = 0] satisfies the first four clauses, responds (4, 4, 4, 4) with "
            "4 c_r = 1 each, and fails selectivity", ok, f"fibre norm: responses {[x[0] for x in resp]}")
    # G4 the core DFT is invertible (det −16i: the windings span the fibre, polarisation pins the kernel) and the
    # minimal degree is forced: a linear functional vanishes on the nontrivial windings and, on the trivial one,
    # F(i ψ₀) = i F(ψ₀) leaves the tally cone for every nonzero multiplier
    det = q4_dft_det()
    ok = det == GI.el(0, -16)
    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))
    ok &= all(not GI.on_line(GI.mul(GI.el(0, 1), GI.el(4 * c))) for c in range(1, 5))
    # the unconjugated bilinear form leaves the tally line on Gaussian-lattice states where the conjugated form stays
    psi_a = [GI.el(1, 1), GI.el(0), GI.el(0), GI.el(0)]                 # (1 + i) e₀
    psi_b = [GI.el(1), GI.el(0, 1), GI.el(0), GI.el(0)]                 # e₀ + i e₁
    shift = [GI.el(0), GI.el(1), GI.el(0), GI.el(0)]                    # [d = 1]
    bil = (q4_bilinear(Kfn, psi_a) == GI.el(0, 2) and q4_tally(Kfn, psi_a) == GI.el(2)
           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)
           and q4_tally(q4_kernel((1, 1, 0, 0)), psi_a) == GI.el(4))
    ok &= bil
    seen, pol = {}, True
    for c in itertools.product(range(3), repeat=4):
        K = q4_kernel(c)
        key = tuple(q4_tally(K, q4_winding(k)) for k in range(4))
        if key in seen and seen[key] != tuple(K): pol = False
        seen[key] = tuple(K)
    R.check("G4", "the core DFT (i^{ru}) has determinant −16i, so the windings span the fibre and equal responses force equal "
            "kernels (exhaustive on 0..2); the minimal degree is forced: the complete character sums vanish on k = 1, 2, 3, "
            "i · (4c, 0) = (0, 4c) is no tally for c = 1..4, and the unconjugated bilinear form leaves the tally line — "
            "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",
            ok and pol, f"det = {det}, {len(seen)} response patterns")


if __name__ == "__main__":
    blocks = [a for a in sys.argv[1:] if a in R.blocks]
    if blocks:
        for b in blocks: R.run_block(b)
        sys.exit(0 if R.summary(write=False) else 1)
    sys.exit(0 if R.verify_all() else 1)