"""p22_quantum — the ledger file of 22-quantum (ledger migration, task LM35, 7 October 2026).

"Quantum Observation over Finite Holographic Substrate" (Akhtman & Voether, 2026, doi 10.20944/preprints202606.1160.v2).
The paper's predicate ledger is docs/22-quantum/22-quantum-ledger.json. This file binds its predicates to the framework:
the table of keys (generated from the ledger by ci/make_ledgers.py) and the checks of seventeen blocks. A block is one
suite of the paper's validation package (src/22-quantum, whose results.json holds one record per suite; served until the
release pin of the paper's milestone, 15 October 2026), and the composite suite is two blocks. Each check names the
predicate(s) it witnesses (LEDGER), under a `# 22:XN (<key>)` marker on the check that decides it (PREDICATES). The
checks compute what the suites compute, record for record, and since 15 October 2026 decide every theorem row of the
paper (the rows C6, C13, C25, X1–X3, X5, X6 had no suite), the Ω rows on the master's anchor (block O, G4), and the
sweep by certified brackets (C7). The Lean side is the quantum theme's Theme/Observation.lean, Theme/Interference.lean
and Theme/Composite.lean, the key files Keys/Quantum.lean, Keys/Extension.lean, Keys/Subject.lean and the
certificates lean/FrcCore/Ledgers/P22Qm.lean and lean/FrcLedger/Ledgers/P22Qm.lean.

The checks call the quantum theme (frc/quantum.py: the cyclotomic ring ℤ[ζ_n], the partial transpose, the
characteristic polynomial), the extension theme (frc/extension.py: 𝔽_{p²}), the chart theme's certified brackets
(frc/chart.py: the Ω bracket of the scale import, π, √8) and, for the two continuum readings, the chart file
frc/chart_quantum.py. This file itself is exact (gate G09): it compares the chart's numbers with Fractions.

    python3 -m frc.ledgers.p22_quantum           every block, the census; exit 1 if a check fails (≈ 5 s)
    python3 -m frc.ledgers.p22_quantum C         one block
    from frc.ledgers.p22_quantum import R; R.predicate("22:C17")    one predicate: its blocks run once per session

Blocks, with the package's suite and its kind:
    V  validate         the single-system formalism on F_157 and F_421          EXACT   (22:C1–C7, C9, C13, C24, X2, X3, X5)
    S  sorkin           Sorkin nullity, shadows and wrap quantisation           EXACT   (22:C8, P2, X8)
    D  dispersion       exact boost transport on F_13 and F_169                 EXACT   (22:A2, P4)
    C  composite        the composite gate on F_641, CHSH and Tsirelson         EXACT, the sweep CHART by brackets (22:C15–C17, C25, P3, X7)
    U  composite        the unequal-cycle gate on F_421                          EXACT   (22:C26)
    M  synchronisation  the m-body conserved offset                             EXACT   (22:C15)
    R  renou            the real-versus-complex network over Q(ζ_8)             EXACT   (22:C18, P3)
    B  bmv              the gravitational channel over Q(ζ_80)                  EXACT   (22:C19, P1)
    Q  decoherence      no collapse, dilation dephasing, the registered count   EXACT, the envelope CHART (22:C7, C20)
    E  equivalence      the two scaling laws and the equivalence-principle null EXACT   (22:C22)
    G  granularity      the depth ceiling, at the anchor by bit length          EXACT   (22:C14, P5)
    T  stratum          the two probability strata and the framed readout      EXACT   (22:C10, C11, X1, X6)
    F  gravfraction     the coherent-fraction channel over ℤ[ζ_16]              EXACT   (22:C21)
    L  gleason          uniqueness of the pair tally on the Q4 core             EXACT   (22:C12)
    O  omega            the Ω ledger in scale arithmetic                        EXACT   (22:A5, Z2)
    I  intersubject     inter-Subject consistency on F_421                      EXACT   (22:C23, X4)
    K  transport        the quarter-turn transport trichotomy                   EXACT   (22:C27)

A check is CHART when its verdict is a continuum reading: the sweep decided by certified rational brackets on the
cosines (C7) and the Gaussian envelope at a stated tolerance (Q3). The notebook frc/ledgers/p22_quantum.ipynb runs one
predicate per cell, the cell's id its key (gate G13).
"""
import random
import sys
from fractions import Fraction as Fr
from itertools import combinations, permutations, product
from math import comb, gcd, isqrt, lcm

from frc import arith
from frc import chart as CH
from frc import chart_quantum as CQ
from frc.extension import Ext
from frc.quantum import Cyclotomic, charpoly, nonneg_spectrum, partial_transpose
from frc.registry import Registry

# ---- generated by ci/make_ledgers.py from docs/22-quantum/22-quantum-ledger.json; edit the ledger, not this table ----
PAPER = "22-quantum"
KEYS = {"A1": "p22001", "A2": "p22002", "A3": "p22003", "A4": "p22004", "A5": "p22005", "A6": "p22006", "A7": "p22007", "A8": "p22008", "B1": "p22009", "B2": "p22010", "B3": "p22011", "B4": "p22012", "B5": "p22013", "B6": "p22014", "B7": "p22015", "B8": "p22016", "C1": "p22017", "C2": "p22018", "C3": "p22019", "C4": "p22020", "C5": "p22021", "C6": "p22022", "C7": "p22023", "C8": "p22024", "C9": "p22025", "C10": "p22026", "C11": "p22027", "C12": "p22028", "C13": "p22029", "C14": "p22030", "C15": "p22031", "C16": "p22032", "C17": "p22033", "C18": "p22034", "C19": "p22035", "C20": "p22036", "C21": "p22037", "C22": "p22038", "C23": "p22039", "C24": "p22040", "C25": "p22041", "C26": "p22042", "C27": "p22043", "X1": "p22044", "X2": "p22045", "X3": "p22046", "X4": "p22047", "X5": "p22048", "X6": "p22049", "X7": "p22050", "X8": "p22051", "P1": "p22052", "P2": "p22053", "P3": "p22054", "P4": "p22055", "P5": "p22056", "Z1": "p22060", "Z2": "p22061"}       # every row of the ledger: its label and its accession key
LEAN = {"A2": "core", "A5": "ml", "C1": "core", "C2": "core", "C3": "core", "C4": "core", "C5": "core", "C6": "core", "C7": "core, ml", "C8": "core, ml", "C9": "core", "C10": "core", "C11": "core", "C12": "core", "C13": "core", "C14": "core, ml", "C15": "core", "C16": "core", "C17": "core, ml", "C18": "core", "C19": "core, ml", "C20": "core", "C21": "core", "C22": "core", "C23": "core", "C24": "core", "C25": "core, ml", "C26": "core", "C27": "core", "X1": "core, ml", "X2": "core", "X3": "core", "X4": "core", "X5": "core", "X6": "core", "X7": "core, ml", "X8": "core, ml", "P1": "core, ml", "P2": "core, ml", "P3": "core, ml", "P4": "core", "P5": "core, ml", "Z2": "ml"}       # the rows with a Lean declaration: the libraries whose key files prove them
# ---- end of the generated table ----

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

# The paper's predicate ledger (predicates cited as 22:XN): the predicate(s) each check witnesses.
LEDGER = {
    "V1": "22:C24", "V2": "22:C3", "V3": "22:C4", "V4": "22:C1, 22:C2", "V5": "22:C3, 22:X3", "V6": "22:C3, 22:C7",
    "V7": "22:C9", "V8": "22:C5", "V9": "22:C4, 22:C7", "V10": "22:C9", "V11": "22:C24", "V12": "22:C4", "V13": "22:C24, 22:X5",
    "V14": "22:C6", "V15": "22:C13, 22:X2", "V16": "22:C7, 22:X1",
    "S1": "22:C8, 22:X8", "S2": "22:P2, 22:C8", "S3": "22:P2, 22:X8",
    "D1": "22:A2", "D2": "22:A2", "D3": "22:A2", "D4": "22:P4", "D5": "22:P4", "D6": "22:P4", "D7": "22:P4", "D8": "22:P4",
    "C1": "22:C15", "C2": "22:C15", "C3": "22:C16", "C4": "22:C17", "C5": "22:C17", "C6": "22:C17",
    "C7": "22:C17, 22:P3", "C8": "22:X7, 22:C17, 22:P3, 22:C25",
    "U1": "22:C26", "U2": "22:C26", "U3": "22:C26", "U4": "22:C26", "U5": "22:C26", "U6": "22:C26",
    "M1": "22:C15", "M2": "22:C15", "M3": "22:C15", "M4": "22:C15", "M5": "22:C15",
    "R1": "22:C18", "R2": "22:C18", "R3": "22:C18", "R4": "22:P3, 22:C18", "R5": "22:C18",
    "B1": "22:C19", "B2": "22:C19", "B3": "22:C19, 22:P1", "B4": "22:C19", "B5": "22:P1, 22:C19",
    "Q1": "22:C20", "Q2": "22:C20", "Q3": "22:C20", "Q4": "22:C20", "Q5": "22:C7", "Q6": "22:C7", "Q7": "22:C7",
    "E1": "22:C22", "E2": "22:C22", "E3": "22:C22", "E4": "22:C22",
    "G1": "22:C14", "G2": "22:C14", "G3": "22:C14", "G4": "22:P5", "G5": "22:C14, 22:P5", "G6": "22:P5", "G7": "22:C14",
    "T1": "22:C10, 22:X1", "T2": "22:C10", "T3": "22:C10", "T4": "22:C11", "T5": "22:C11, 22:X6", "T6": "22:C11", "T7": "22:C11",
    "T8": "22:C11", "T9": "22:C11", "T10": "22:C11", "T11": "22:C11", "T12": "22:C10",
    "F1": "22:C21", "F2": "22:C21", "F3": "22:C21", "F4": "22:C21", "F5": "22:C21", "F6": "22:C21", "F7": "22:C21",
    "F8": "22:C21", "F9": "22:C21", "F10": "22:C21", "F11": "22:C21", "F12": "22:C21",
    "L1": "22:C12", "L2": "22:C12", "L3": "22:C12", "L4": "22:C12", "L5": "22:C12", "L6": "22:C12", "L7": "22:C12",
    "L8": "22:C12", "L9": "22:C12",
    "O1": "22:A5", "O2": "22:A5", "O3": "22:A5", "O4": "22:Z2",
    "I1": "22:C23", "I2": "22:C23", "I3": "22:C23", "I4": "22:C23", "I5": "22:X4, 22:C23", "I6": "22:X4", "I7": "22:X4",
    "K1": "22:C27",
}

BLOCK = {"V": "validate: the single-system formalism on F_157 and F_421",         # check-id prefix -> the block
         "S": "sorkin: Sorkin nullity, sub-horizon shadows, wrap quantisation",
         "D": "dispersion: exact boost transport on F_13 and F_169",
         "C": "composite: the composite gate on F_641, CHSH and Tsirelson",
         "U": "composite: the unequal-cycle gate on F_421",
         "M": "synchronisation: the m-body conserved offset",
         "R": "renou: the real-versus-complex network over Q(zeta_8)",
         "B": "bmv: the gravitational channel over Q(zeta_80)",
         "Q": "decoherence: no collapse, dilation dephasing, the registered count",
         "E": "equivalence: the two scaling laws and the equivalence-principle null",
         "G": "granularity: the depth ceiling",
         "T": "stratum: the two probability strata and the framed readout",
         "F": "gravfraction: the coherent-fraction channel",
         "L": "gleason: uniqueness of the pair tally",
         "O": "omega: the Omega ledger in scale arithmetic",
         "I": "intersubject: inter-Subject consistency",
         "K": "transport: the quarter-turn transport trichotomy"}

# the package's suite of each block (the script its results.json record names)
SUITE = {"V": "validate", "S": "sorkin", "D": "dispersion", "C": "composite", "U": "composite", "M": "synchronisation",
         "R": "renou", "B": "bmv", "Q": "decoherence", "E": "equivalence", "G": "granularity", "T": "stratum",
         "F": "gravfraction", "L": "gleason", "O": "omega", "I": "intersubject", "K": "transport"}

# the deciding check of each witnessed predicate (the other checks that touch it are corroboration)
PREDICATES = {
    "22:A2": "D3", "22:A5": "O1", "22:C1": "V4", "22:C2": "V4", "22:C3": "V5", "22:C4": "V3", "22:C5": "V8",
    "22:C6": "V14", "22:C7": "V16", "22:C8": "S1", "22:C9": "V7", "22:C10": "T1", "22:C11": "T5", "22:C12": "L1",
    "22:C13": "V15", "22:C14": "G3", "22:C15": "M3", "22:C16": "C3", "22:C17": "C4", "22:C18": "R3", "22:C19": "B2",
    "22:C20": "Q1", "22:C21": "F11", "22:C22": "E2", "22:C23": "I4", "22:C24": "V13", "22:C25": "C8", "22:C26": "U2",
    "22:C27": "K1", "22:P1": "B5", "22:P2": "S3", "22:P3": "R4", "22:P4": "D8", "22:P5": "G4", "22:X1": "V16",
    "22:X2": "V15", "22:X3": "V5", "22:X4": "I5", "22:X5": "V13", "22:X6": "T5", "22:X7": "C8", "22:X8": "S1",
    "22:Z2": "O4",
}

R = Registry("22", "quantum", LEDGER, PREDICATES, sources=[__file__])

TOL = Fr(1, 10 ** 12)           # the package's tolerance for its floating-point laws


# ---- Gaussian integers as pairs, the ledger ℤ[i] of the suites -----------------------------------------------------
def gm(z, w): return (z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0])
def ga(z, w): return (z[0] + w[0], z[1] + w[1])
def gc(z): return (z[0], -z[1])
def gnorm(z): return z[0] * z[0] + z[1] * z[1]
I4 = [(1, 0), (0, 1), (-1, 0), (0, -1)]                       # i^l


def shell(p, e, nS, nO):
    """The Subject and Object cycles of orders nS, nO in F_p^x (generator e), their gcd and the core."""
    N = p - 1
    gS, gO = pow(e, N // nS, p), pow(e, N // nO, p)
    HS, HO = {pow(gS, j, p) for j in range(nS)}, [pow(gO, j, p) for j in range(nO)]
    return N, gS, gO, gcd(nS, nO), HS, HO, sorted(HS.intersection(HO))


# ------------------------------------------------------------------------------------------------------------
# block V: the single-system formalism (validate.py, 22:C1–C5, C7, C9, C24)
# The first Carrier is F_157 (g = 5), with the Subject S_53 (C_52) and the Object O_13 (C_12). Their core is Q4, and the
# Object has three outcomes. The checks cover the fibres, the selection rule over every channel pair and the drive
# eigenstates. The forced basis is checked on a fixed Gaussian-integer state: orthogonality, Parseval and Lüders. The
# ledger selection rule is checked in ℤ[ζ_12], with both reductions to the Carrier. The second Carrier is F_421 (g = 2).
# There the quantum pair S_61, O_29 has core Q4 and quotient C_7, and the classical pair S_61, O_13 is total absorption.
@R.block("V", BLOCK["V"])
def block_V():
    """Block V — validate.py (EXACT): V1–V13, the package's 19 checks."""
    p, e, nS, nO = 157, 5, 52, 12
    N, gS, gO, d, HS, HO, core = shell(p, e, nS, nO)
    ip = pow(e, N // 4, p)
    ok = arith.order(e, p) == N and core == [1, 28, 129, 156] and d == 4
    ok &= pow(e, N - 39, p) == 28 and pow(28, 2, p) == p - 1 and lcm(nS, nO) == N
    R.check("V1", "F_157: g = 5 primitive; core = {1, 28, 129, 156}, |core| = 4 = gcd(52, 12); I = g^-39 = 28, I^2 = -1; lcm(52, 12) = 156", ok)

    fib = {a: [pow(gO, a + 3 * l, p) for l in range(4)] for a in range(3)}
    R.check("V2", "F_157: the three fibres (Q4-cosets) partition Phi_O", sorted(sum(fib.values(), [])) == sorted(HO))

    ok = all(sum(pow(e, ((N // 4) * (s - r) * l) % N, p) for l in range(4)) % p == (4 if (r - s) % 4 == 0 else 0)
             for r in range(nS) for s in range(nO))
    # 22:C4 (p22020)
    R.check("V3", "F_157: the selection rule A(r, s) = 4 [r = s mod 4] over all 52 x 12 channel pairs", ok)

    ok = all(pow(gO * u % p, s, p) == pow(gO, s, p) * pow(u, s, p) % p for u in HO for s in range(nO))
    distinct = len({tuple(pow(u, s, p) for u in HO) for s in range(nO)}) == nO == len({pow(gO, s, p) for s in range(nO)})
    roots = sorted(x for x in range(1, p) if pow(x, nO, p) == 1)              # every 12th root of unity in F_157 ...
    complete = roots == sorted(HO) and len(roots) == nO                       # ... is a power of g_O: the characters are the power maps, no other
    # 22:C1 (p22017), 22:C2 (p22018)
    R.check("V4", "F_157: the windings psi_s(u) = u^s are drive eigenstates, U psi_s = g_O^s psi_s, all s; the 12 power maps and their eigenvalues pairwise distinct; every 12th root of unity in F_157 is a power of g_O (the characters are the power maps and no others)",
            ok and distinct and complete)

    psi = {u: ((i % 13) - 6, (i % 11) - 5) for i, u in enumerate(HO)}          # the fixed state, no RNG
    red = lambda z: (z[0] + ip * z[1]) % p                                     # Z[i] -> F_p, i -> 5^39
    psip = {u: red(z) for u, z in psi.items()}
    def v(r, a):
        w = {u: (0, 0) for u in HO}
        for l in range(4): w[pow(gO, a + 3 * l, p)] = I4[(r * l) % 4]
        return w
    def pair(x, y):
        s = (0, 0)
        for u in HO: s = ga(s, gm(gc(x[u]), y[u]))
        return s
    def amp(r, a):
        s = (0, 0)
        for l in range(4): s = ga(s, gm(gc(I4[(r * l) % 4]), psi[pow(gO, a + 3 * l, p)]))
        return s
    def amp_fp(r, a):
        return sum(pow(pow(ip, l, p), (4 - r) % 4, p) * psip[pow(gO, a + 3 * l, p)] for l in range(4)) % p
    RA = [(r, a) for r in range(4) for a in range(3)]
    ok = all(pair(v(*x), v(*y)) == ((4, 0) if x == y else (0, 0)) for x in RA for y in RA)
    # 22:C3 (p22019), 22:X3 (p22046)
    R.check("V5", "F_157: the forced basis is orthogonal, <v_{r,a}, v_{r',a'}> = 4 delta delta (Z[i])", ok)

    lhs = sum(gnorm(amp(r, a)) for r, a in RA); rhs = 4 * sum(gnorm(z) for z in psi.values())
    R.check("V6", "F_157: Parseval, sum |Psi|^2 = 4 ||psi||^2 on the fixed Gaussian-integer state (resolution of the identity, 22:C3)", lhs == rhs, f"{lhs} = {rhs}")

    # The pair count (eq. paircount): the weight of a channel is the double sum over ordered pairs of fibre points of
    # the phase agreements conj(v(u)) psi(u) conj(psi(u')) v(u'), computed as that double sum in Z[i], equal to the
    # norm N(Psi) of the amplitude, a nonnegative integer (a realised tally), on every channel of the fixed state.
    def pair_count(r, a):
        vv, fibre, tot = v(r, a), [pow(gO, a + 3 * l, p) for l in range(4)], (0, 0)
        for u in fibre:
            for u2 in fibre: tot = ga(tot, gm(gm(gc(vv[u]), psi[u]), gm(gc(psi[u2]), vv[u2])))
        return tot
    counts = {x: pair_count(*x) for x in RA}
    ok = all(counts[x] == (gnorm(amp(*x)), 0) and gnorm(amp(*x)) >= 0 for x in RA) and any(gnorm(amp(*x)) > 0 for x in RA)
    # 22:C7 (p22023), 22:X1 (p22044)
    R.check("V16", "F_157: the pair count, the double sum of phase agreements over ordered fibre pairs, is the weight N(Psi_{r,a}) in Z, a nonnegative integer (a realised tally), on all 12 channels of the fixed state",
            ok, f"weights {[gnorm(amp(*x)) for x in RA]}")

    # 22:C9 (p22025)
    R.check("V7", "F_157: the ledger reduction Z[i] -> F_157 commutes with the amplitudes on every channel", all(red(amp(r, a)) == amp_fp(r, a) for r, a in RA))

    def proj(r, a, phi):
        A, vv = (0, 0), v(r, a)
        for l in range(4):
            u = pow(gO, a + 3 * l, p); A = ga(A, gm(gc(vv[u]), phi[u]))
        return {u: gm(vv[u], A) for u in HO}
    ok = True
    for r, a in RA:
        phi1 = proj(r, a, psi); phi2 = proj(r, a, phi1)
        ok &= all(phi2[u] == gm((4, 0), phi1[u]) for u in HO)
    # 22:C5 (p22021)
    R.check("V8", "F_157: Lueders idempotence Pi^2 = 4 Pi on all 12 channels (r, a) of the fixed state (the projector with its conjugate; r = 1, 3 are the complex channels)", ok)

    Z = Cyclotomic(12)
    okL = okR = True
    for s in range(12):
        for r in range(4):
            for a in range(3):
                S = Z.sum(Z.mul(Z.zeta(s * (a + 3 * l)), Z.zeta(-3 * r * l)) for l in range(4))
                tgt = Z.zeta(s * a, 4) if (s - r) % 4 == 0 else Z.zero
                okL &= S == tgt
                okR &= Z.shadow(S, p, gO) == ((4 * pow(gO, s * a, p)) % p if (s - r) % 4 == 0 else 0)
    R.check("V9", "F_157: the ledger selection rule Psi = 4 zeta_12^{s a} iff r = s mod 4, else 0, in Z[zeta_12]", okL)
    R.check("V10", "F_157: the ledger reduction zeta_12 -> g_O = 22 matches the Carrier amplitudes", okR and gO == 22)

    p2, e2 = 421, 2
    N2 = p2 - 1
    _, _, gO2, d2, HS2, HO2, core2 = shell(p2, e2, 60, 28)
    ok = arith.order(e2, p2) == N2 and core2 == [1, 29, 392, 420] and d2 == 4 and lcm(60, 28) == 420
    ok &= pow(e2, N2 - 105, p2) == 392 and pow(392, 2, p2) == p2 - 1
    R.check("V11", "F_421: g = 2 primitive; quantum pair S_61, O_29: core {1, 29, 392, 420}, gcd 4, lcm 420; I = 2^-105 = 392, I^2 = -1", ok)
    ok = all(sum(pow(e2, (105 * (s - r) * l) % N2, p2) for l in range(4)) % p2 == (4 if (r - s) % 4 == 0 else 0)
             for r in range(60) for s in range(28))
    R.check("V12", "F_421: the selection rule over all 60 x 28 channel pairs", ok)
    _, _, _, d3, HS3, HO3, core3 = shell(p2, e2, 60, 12)
    live = {s: [r for r in range(12) if sum(pow(e2, ((N2 // d3) * (s - r) * l) % N2, p2) for l in range(d3)) % p2 != 0] for s in range(12)}
    live_q = {s: [r for r in range(28) if sum(pow(e2, (105 * (s - r) * l) % N2, p2) for l in range(4)) % p2 != 0] for s in range(28)}
    # 22:C24 (p22040), 22:X5 (p22048)
    R.check("V13", "F_421: seven outcomes, C_28/Q4 = C_7 (quantum, index 7 > 1: every winding couples to 7 of the 28 channels); the classical pair S_61, O_13: gcd(60, 12) = 12, total absorption, one outcome per winding (the selection sums vanish on the other 11 channels)",
            28 // d2 == 7 and d3 == 12 and set(HO3) <= HS3 and 12 // d3 == 1 and all(len(live[s]) == 1 for s in range(12)) and all(len(live_q[s]) == 7 for s in range(28)))

    # Conjugation is cycle inversion, forced in each setting (22:C6): on every prime p = 4k + 1 below 200, the Frobenius
    # x -> x^p of F_{p^2} is the conjugation (a, b) -> (a, -b), it inverts the norm-one torus (z z^p = 1), and it is the
    # only non-trivial automorphism over F_p (an automorphism sends sqrt(nu) to a root of X^2 - nu, so to +-sqrt(nu));
    # on the phase cycle exponent negation is inversion, zeta^k zeta^(n-k) = 1; and the ledger's conjugation reduces to
    # it: the shadow of zeta_12^(-e) is the inverse of the shadow of zeta_12^e on F_157 (zeta_12 -> 22).
    ok = True; det = []
    for q in [x for x in range(5, 200) if arith.is_prime(x) and x % 4 == 1]:
        nu = next(v for v in range(2, q) if pow(v, (q - 1) // 2, q) == q - 1)
        K = Ext(q, nu)
        torus = K.norm_one()
        ok &= len(torus) == q + 1 and all(K.pow(z, q) == K.conj(z) and K.mul(z, K.conj(z)) == (1, 0) for z in torus)
        ok &= all(K.pow(z, q) == K.conj(z) for z in K.elements())
        roots = [x for x in K.elements() if K.mul(x, x) == (nu % q, 0)]
        ok &= sorted(roots) == sorted([(0, 1), (0, q - 1)])                  # sqrt(nu) has two images: the two automorphisms
        det.append(str(q))
    z12 = 22
    ok &= all(pow(z12, (12 - k) % 12, 157) * pow(z12, k, 157) % 157 == 1 for k in range(12))
    ok &= all(pow(pow(z12, k, 157), -1, 157) == pow(z12, (-k) % 12, 157) for k in range(12))
    # 22:C6 (p22022)
    R.check("V14", "conjugation is inversion in each setting: the Frobenius of F_{p^2} is (a, b) -> (a, -b), inverts the norm-one torus and is the only non-trivial automorphism over F_p (sqrt nu -> +-sqrt nu), every p = 4k+1 < 200; exponent negation inverts C_12 and the ledger's conjugation reduces to it on F_157",
            ok, f"{len(det)} shells")

    # The forced complex sector (22:C13, X2): the shared core of two framed shells of capacities kappa, kappa' is the
    # cycle of order gcd(4 kappa, 4 kappa'), a multiple of 4, and exactly Q4 when the capacities are coprime (exhaustive
    # below 30); a shell p = 3 (mod 4) has no square root of -1 and every p = 1 (mod 4) has one (every prime below 200).
    ok = all(gcd(4 * a, 4 * b) % 4 == 0 for a in range(1, 30) for b in range(1, 30))
    ok &= all(gcd(4 * a, 4 * b) == 4 for a in range(1, 30) for b in range(1, 30) if gcd(a, b) == 1)
    ok &= any(gcd(4 * a, 4 * b) > 4 for a in range(1, 30) for b in range(1, 30))
    for q in [x for x in range(3, 200) if arith.is_prime(x)]:
        has = any(x * x % q == q - 1 for x in range(q))
        ok &= has == (q % 4 == 1)
    # 22:C13 (p22029), 22:X2 (p22045)
    R.check("V15", "the shared core of two framed shells has order a multiple of 4 and is Q4 for coprime capacities (kappa, kappa' < 30); a square root of -1 exists on p = 1 (mod 4) and on no p = 3 (mod 4), every prime below 200: the universal ledger is Z[i], the real theory arises from no capacity",
            ok)


# ------------------------------------------------------------------------------------------------------------
# block S: the Sorkin hierarchy (sorkin.py, 22:C8, P2, X8)
# Four slits carry deterministic Gaussian-integer components on the Object cycle. The k-th order Sorkin combination is
# taken over every channel and outcome, on F_157 and F_421. I2 is nonzero, and I3 = I4 = 0 exactly. The observed
# combination comes from the lifted shadows. It is zero below the horizon, where every tally is below p. Above the
# horizon it is a multiple of p, with nonzero instances.
@R.block("S", BLOCK["S"])
def block_S():
    """Block S — sorkin.py (EXACT): S1–S3, the package's 8 checks."""
    cnt = [0]
    def nxt():
        cnt[0] += 1; return cnt[0]
    wide = lambda: (((nxt() * 5) % 19) - 9, ((nxt() * 13) % 19) - 9)
    binary = lambda: (nxt() % 2, 0)
    deep = lambda: (7 * (((nxt() * 5) % 19) - 9), 7 * (((nxt() * 13) % 19) - 9))
    def run(p, e, nO, nslits, coeff):
        gO = pow(e, (p - 1) // nO, p); HO = [pow(gO, j, p) for j in range(nO)]; q = nO // 4
        slits = [{u: coeff() for u in HO} for _ in range(nslits)]
        W = {}
        for mask in range(1, 1 << nslits):
            S = tuple(i for i in range(nslits) if mask >> i & 1)
            for r in range(4):
                for a in range(q):
                    s = (0, 0)
                    for l in range(4):
                        u = pow(gO, a + q * l, p); comp = (0, 0)
                        for i in S: comp = ga(comp, slits[i][u])
                        s = ga(s, gm(gc(I4[(r * l) % 4]), comp))
                    W[(S, r, a)] = gnorm(s)
        return W, q
    def hier(W, q, k, lift=None):
        out = []
        for r in range(4):
            for a in range(q):
                out.append(sum((-1) ** (k - m) * (W[(c, r, a)] if lift is None else W[(c, r, a)] % lift)
                               for m in range(1, k + 1) for c in combinations(range(k), m)))
        return out
    ok = True; det = []
    for p, e, nO, tag in [(157, 5, 12, "157/53/13"), (421, 2, 28, "421/61/29")]:
        W, q = run(p, e, nO, 4, wide)
        I2, I3, I4v = hier(W, q, 2), hier(W, q, 3), hier(W, q, 4)
        ok &= any(I2) and not any(I3) and not any(I4v)
        det.append(f"{tag}: max |I2| = {max(map(abs, I2))}")
    # 22:C8 (p22024), 22:X8 (p22051)
    R.check("S1", "Sorkin nullity on F_157 and F_421: I2 generically nonzero, I3 = I4 = 0 exactly on every channel and outcome", ok, "; ".join(det))

    p = 157
    W, q = run(p, 5, 12, 3, binary)
    I3h = hier(W, q, 3, p)
    R.check("S2", "F_157, sub-horizon tallies (every w < p): the observed I3 from the lifted shadows is 0 exactly", all(w < p for w in W.values()) and not any(I3h))
    W, q = run(p, 5, 12, 3, deep)
    I3h = hier(W, q, 3, p); nz = sum(1 for v in I3h if v)
    # 22:P2 (p22053)
    R.check("S3", "F_157, super-window tallies present: the observed I3 is a multiple of p (wrap quantisation), with nonzero instances",
            any(w >= p for w in W.values()) and all(v % p == 0 for v in I3h) and nz > 0, f"{nz} nonzero cases, all multiples of {p}")


# ------------------------------------------------------------------------------------------------------------
# block D: exact boost transport (dispersion.py, 22:A2, P4)
# The Dirac layer lives over K = F_169 = F_13(c), with c² = ν = 2. The gammas obey G^μG^ν + G^νG^μ = 2η^{μν}, with
# η = diag(−ν, 1, 1, 1). The spin lift is S(x, y) = xI + yM, where M = G0 G1 and M² = ν. Spin conjugation is checked for
# every boost (x, y) with δ = x² − νy² ≠ 0, together with the transported Clifford relations. The boost group law is
# checked on the norm-one cycle of order p + 1 = 14. The spinor fields live over Y = F_13⁴, and the package's fixed field
# is used. The transported Dirac operator is covariant under every norm-one boost. The Dirac → Klein–Gordon factorisation
# holds in the standard and in a boosted frame, and the boost cycle closes. A field is four lists over the 13⁴ points.
# Its values are packed as a + 13b and are added and scaled by tables.
@R.block("D", BLOCK["D"])
def block_D():
    """Block D — dispersion.py (EXACT): D1–D6, the package's 9 checks, and D7 on a field the package does not use."""
    p, nu = 13, 2
    K = Ext(p, nu); Z0 = (0, 0)
    ip = min(x for x in range(2, p) if x * x % p == p - 1)                    # the internal i, 5² = −1
    def mm(X, Y):                                                             # 4 x 4 over K, rows as {col: value}
        out = []
        for row in X:
            acc = {}
            for k, a in row.items():
                for j, b in Y[k].items(): acc[j] = K.add(acc.get(j, Z0), K.mul(a, b))
            out.append({j: w for j, w in acc.items() if w != Z0})
        return out
    def madd(X, Y):
        out = []
        for rx, ry in zip(X, Y):
            acc = dict(rx)
            for j, b in ry.items(): acc[j] = K.add(acc.get(j, Z0), b)
            out.append({j: w for j, w in acc.items() if w != Z0})
        return out
    def msc(c, X): return [{j: K.mul(c, w) for j, w in row.items() if K.mul(c, w) != Z0} for row in X]
    def emb(M, part=0): return [{j: ((M[i][j] % p, 0) if part == 0 else (0, M[i][j] % p)) for j in range(4) if M[i][j] % p} for i in range(4)]
    def blk(off, sign, M):
        Zm = [[0] * 4 for _ in range(4)]
        for i in range(2):
            for j in range(2):
                if off: Zm[i][j + 2] = Zm[i + 2][j] = M[i][j]
                else: Zm[i][j], Zm[i + 2][j + 2] = M[i][j], sign * M[i][j]
        return Zm
    s1, s2, s3, I2 = [[0, 1], [1, 0]], [[0, -ip], [ip, 0]], [[1, 0], [0, -1]], [[1, 0], [0, 1]]
    E = [emb(blk(1, 0, s1)), emb(blk(1, 0, s2)), emb(blk(1, 0, s3))]
    G = [emb([[ip * x for x in row] for row in blk(0, -1, I2)], 1)] + E           # G0 = c·i·e4, (G0)² = −ν
    eta = [(-nu) % p, 1, 1, 1]
    Id = emb([[int(i == j) for j in range(4)] for i in range(4)])
    def clifford(gs):
        return all(madd(mm(gs[m], gs[n]), mm(gs[n], gs[m])) == (msc((2 * eta[m] % p, 0), Id) if m == n else [{}] * 4)
                   for m in range(4) for n in range(4))
    M = mm(G[0], G[1])
    R.check("D1", "Clifford relations G^mu G^nu + G^nu G^mu = 2 eta^{mu nu} I over F_169 (all 16 pairs, eta = diag(-nu, 1, 1, 1)); M = G0 G1 has M^2 = nu I",
            clifford(G) and mm(M, M) == msc((nu, 0), Id))

    def AB(x, y):
        di = pow((x * x - nu * y * y) % p, -1, p)
        return (x * x + nu * y * y) * di % p, (-2 * x * y * di) % p
    def spin(x, y): return madd(msc((x % p, 0), Id), msc((y % p, 0), M))
    def hat(A, B): return [madd(msc((A, 0), G[0]), msc((-nu * B % p, 0), G[1])), madd(msc((-B % p, 0), G[0]), msc((A, 0), G[1])), G[2], G[3]]
    ok2 = ok4 = True; count = 0
    for x in range(p):
        for y in range(p):
            dl = (x * x - nu * y * y) % p
            if dl == 0: continue
            count += 1
            S = spin(x, y); Si = msc((pow(dl, -1, p), 0), spin(x, -y))                # S^{-1} = (xI − yM)/δ, checked
            A, B = AB(x, y)
            ok2 &= mm(S, Si) == Id
            ok2 &= mm(Si, mm(G[0], S)) == madd(msc((A, 0), G[0]), msc((nu * B % p, 0), G[1]))
            ok2 &= mm(Si, mm(G[1], S)) == madd(msc((B, 0), G[0]), msc((A, 0), G[1]))
            ok2 &= mm(Si, mm(G[2], S)) == G[2] and mm(Si, mm(G[3], S)) == G[3]
            ok4 &= clifford(hat(A, B))
    R.check("D2", "spin conjugation S^-1 G^mu S = Lambda G for all 168 boosts (x, y), delta != 0; the transported gammas obey the Clifford relations",
            ok2 and ok4 and count == p * p - 1, f"{count} boosts")

    def lam(x, y):
        A, B = AB(x, y)
        return [[A, B, 0, 0], [nu * B % p, A, 0, 0], [0, 0, 1, 0], [0, 0, 0, 1]]
    def imul(X, Y): return [[sum(X[i][k] * Y[k][j] for k in range(4)) % p for j in range(4)] for i in range(4)]
    U1 = [(x, y) for x in range(p) for y in range(p) if (x * x - nu * y * y) % p == 1]
    ok = all(imul(lam(x, y), lam(u, v)) == lam((x * u + nu * y * v) % p, (x * v + y * u) % p) for x, y in U1 for u, v in U1)
    # 22:A2 (p22002)
    R.check("D3", "the boost group law Lambda(x, y) Lambda(u, v) = Lambda(xu + nu yv, xv + yu), exhaustive on the norm-one cycle of order p + 1 = 14",
            ok and len(U1) == p + 1, f"{len(U1)}^2 products")

    # the spinor fields over Y = F_13^4: values packed a + 13 b
    P2, P4 = p * p, p ** 4
    unpack = lambda w: (w % p, w // p)
    ADD = [K.add(unpack(u), unpack(w)) for u in range(P2) for w in range(P2)]
    ADD = [a + p * b for a, b in ADD]
    SUB = [(lambda z: z[0] + p * z[1])(K.sub(unpack(u), unpack(w))) for u in range(P2) for w in range(P2)]
    tabs = {}
    def tab(c):
        if c not in tabs: tabs[c] = [(lambda z: z[0] + p * z[1])(K.mul(c, unpack(w))) for w in range(P2)]
        return tabs[c]
    def lincomb(terms):
        if not terms: return [0] * P4
        if len(terms) == 1: return [terms[0][0][w] for w in terms[0][1]]
        (T1, L1), (T2, L2) = terms[:2]
        out = [ADD[T1[u] * P2 + T2[w]] for u, w in zip(L1, L2)]
        for T, L in terms[2:]: out = [ADD[u * P2 + T[w]] for u, w in zip(out, L)]
        return out
    def mvec(X, f): return [lincomb([(tab(c), f[k]) for k, c in X[i].items()]) for i in range(4)]
    def fadd(f, g): return [[ADD[u * P2 + w] for u, w in zip(a, b)] for a, b in zip(f, g)]
    def fsub(f, g): return [[SUB[u * P2 + w] for u, w in zip(a, b)] for a, b in zip(f, g)]
    def fsc(c, f):
        T = tab((c % p, 0))
        return [[T[w] for w in a] for a in f]
    COORD = list(product(range(p), repeat=4))
    perms = {}
    def shift_perm(vec):                                                      # f(z + vec)
        if vec not in perms:
            a, b, c, d = vec
            perms[vec] = [(((t + a) % p * p + (x + b) % p) * p + (y + c) % p) * p + (z + d) % p for t, x, y, z in COORD]
        return perms[vec]
    def nabla(f, perm): return [[SUB[fc[q] * P2 + w] for q, w in zip(perm, fc)] for fc in f]
    def dirac(f, gams, perms):
        nab = [nabla(f, perms[mu]) for mu in range(4)]
        return [lincomb([(tab(c), nab[mu][k]) for mu in range(4) for k, c in gams[mu][i].items()]) for i in range(4)]
    def kg(f, perms):
        out = None
        for mu in range(4):
            t = fsc(eta[mu], nabla(nabla(f, perms[mu]), perms[mu]))
            out = t if out is None else fadd(out, t)
        return out
    sources = {}
    def transport(f, x, y):                                                   # (T f)(z) = S f(Λ^{-1} z)
        if (x, y) not in sources:
            Li = lam(x, -y % p)
            sources[(x, y)] = [((Li[0][0] * t + Li[0][1] * xx) % p * p + (Li[1][0] * t + Li[1][1] * xx) % p) * P2 + yy * p + z
                               for t, xx, yy, z in COORD]
        src = sources[(x, y)]
        return mvec(spin(x, y), [[fc[q] for q in src] for fc in f])
    def frame_perms(x, y):
        L = lam(x, y)
        return [shift_perm(tuple(L[i][mu] for i in range(4))) for mu in range(4)]
    psi = [[((((pos * 4 + c) * 2) * 7 + 3) % p) + p * ((((pos * 4 + c) * 2 + 1) * 7 + 3) % p) for pos in range(P4)] for c in range(4)]
    std = [shift_perm(tuple(int(i == mu) for i in range(4))) for mu in range(4)]
    D0 = dirac(psi, G, std)
    ok = True
    for x, y in U1:
        A, B = AB(x, y)
        ok &= dirac(transport(psi, x, y), hat(A, B), frame_perms(x, y)) == transport(D0, x, y)
    R.check("D4", "exact covariance D_{Lambda,S} T psi = T D psi on the fixed spinor field over F_13^4, all 14 norm-one boosts", ok)

    m = 7
    def factorises(gams, perms):
        Dm = fadd(dirac(psi, gams, perms), fsc(m, psi))
        return fsub(dirac(Dm, gams, perms), fsc(m, Dm)) == fsub(kg(psi, perms), fsc(m * m, psi))
    x, y = U1[1]
    ok = factorises(G, std) and factorises(hat(*AB(x, y)), frame_perms(x, y))
    R.check("D5", "the Dirac -> Klein-Gordon factorisation (D - m)(D + m) = KG - m^2 on the fixed field, in the standard frame and a boosted frame", ok)

    xg, yg = next((x, y) for x, y in U1 if y != 0)
    cur, order = (1, 0), 0
    while True:
        cur = ((cur[0] * xg + nu * cur[1] * yg) % p, (cur[0] * yg + cur[1] * xg) % p); order += 1
        if cur == (1, 0): break
    f = psi
    for _ in range(order): f = transport(f, xg, yg)
    Pw, half = Id, None
    for k in range(order):
        Pw = mm(Pw, spin(xg, yg))
        if k + 1 == order // 2: half = Pw
    R.check("D6", "closure of the boost cycle: transport around the generator's orbit returns S^n psi exactly, no accumulated deformation; the spinor double cover S^((p+1)/2) = -I",
            f == mvec(Pw, psi) and half == msc((p - 1, 0), Id), f"orbit of the generator {(xg, yg)}: {order} steps, S^{order // 2} = -I")

    # The package's field is 7·index + 3 mod 13, and the strides 13, 13², 13³ of t, x, y vanish mod 13. So it depends on
    # z alone, and D4 and D5 test only the z-direction. D7 repeats them on point sources, which test every coefficient
    # of both operators at once. A sparse field is a dict from points to spinors over K.
    def sp_add(f, g, sign=1):
        out = {w: list(v) for w, v in f.items()}
        for w, v in g.items():
            cur = out.setdefault(w, [Z0] * 4)
            out[w] = [K.add(a, b) if sign > 0 else K.sub(a, b) for a, b in zip(cur, v)]
        return {w: v for w, v in out.items() if any(c != Z0 for c in v)}
    def sp_mvec(X, f, c=(1, 0)):
        out = {w: [K.mul(c, _ksum(K, (K.mul(a, v[k]) for k, a in X[i].items()))) for i in range(4)] for w, v in f.items()}
        return {w: v for w, v in out.items() if any(e != Z0 for e in v)}
    def sp_nabla(f, vec):                                                     # f(z + vec) − f(z)
        return sp_add({tuple((a - b) % p for a, b in zip(w, vec)): v for w, v in f.items()}, f, -1)
    def sp_dirac(f, gams, frame):
        out = {}
        for mu in range(4): out = sp_add(out, sp_mvec(gams[mu], sp_nabla(f, frame[mu])))
        return out
    def sp_transport(f, x, y):                                                # (T f)(Λw) = S f(w)
        L = lam(x, y)
        return sp_mvec(spin(x, y), {tuple(sum(L[i][j] * w[j] for j in range(4)) % p for i in range(4)): v for w, v in f.items()})
    def sp_frame(x, y):
        L = lam(x, y)
        return [tuple(L[i][mu] for i in range(4)) for mu in range(4)]
    rnd = random.Random(13)
    ok = True
    for _ in range(3):
        psi = {tuple(rnd.randrange(p) for _ in range(4)): [(rnd.randrange(p), rnd.randrange(p)) for _ in range(4)] for _ in range(3)}
        D0 = sp_dirac(psi, G, sp_frame(1, 0))
        for x, y in U1:
            ok &= sp_dirac(sp_transport(psi, x, y), hat(*AB(x, y)), sp_frame(x, y)) == sp_transport(D0, x, y)
        for x, y in [(1, 0), U1[1]]:
            gams, frame = (G if (x, y) == (1, 0) else hat(*AB(x, y))), sp_frame(x, y)
            Dm = sp_add(sp_dirac(psi, gams, frame), sp_mvec(Id, psi, (m, 0)))
            kgf = {}
            for mu in range(4): kgf = sp_add(kgf, sp_mvec(Id, sp_nabla(sp_nabla(psi, frame[mu]), frame[mu]), (eta[mu], 0)))
            ok &= sp_add(sp_dirac(Dm, gams, frame), sp_mvec(Id, Dm, (m, 0)), -1) == sp_add(kgf, sp_mvec(Id, psi, (m * m % p, 0)), -1)
    R.check("D7", "D4 and D5 again on point sources, which test every coefficient of both operators (the package's field depends on z alone mod 13): covariance under all 14 norm-one boosts, the factorisation in the standard and a boosted frame",
            ok, "three fields of three random point sources")
    ok = True
    for _ in range(3):
        f0 = {tuple(rnd.randrange(p) for _ in range(4)): [(rnd.randrange(p), rnd.randrange(p)) for _ in range(4)] for _ in range(3)}
        f, Pw = f0, Id
        for k in range(1, order + 1):
            f = sp_transport(f, xg, yg); Pw = mm(Pw, spin(xg, yg))
            moved = f != sp_mvec(Pw, f0)                                       # Lambda^k moves the support unless Lambda^k = 1 (order 7 on the points: Lambda(z) = conj(z)^2)
            ok &= moved == (k % (order // 2) != 0)
            if k == order // 2: ok &= f == sp_mvec(msc((p - 1, 0), Id), f0)   # the double cover's sign on the field at the half orbit
        ok &= f == f0 and order == p + 1
    # 22:P4 (p22055)
    R.check("D8", "closure of the boost cycle on point-source fields, step by step: Lambda^k moves the support exactly when 7 does not divide k (Lambda has order 7 on the points), at the half orbit T^7 psi = -psi (the double cover's sign), and T^14 psi = psi exactly; nothing short of the orbit returns",
            ok and half == msc((p - 1, 0), Id), f"three point-source fields, {order} steps")


def _ksum(K, xs):
    out = (0, 0)
    for x in xs: out = K.add(out, x)
    return out


# ------------------------------------------------------------------------------------------------------------
# block C: the composite gate and the CHSH test (composite.py, C1–C8, 22:C15–C17, P3, X7)
# The Carrier is F_641 (g = 3). The Object pair O_17 x O_17 (C_16, g_O = 3^40 = 601, g_O^8 = −1) is read by S_41 (C_40),
# with core C_8 and quotient C_2. The drive conserves the relative offset, and the doublet readout is σ_x. Over ℤ[ζ_80]
# the checks cover the singlet law E(Δ) = cos(πΔ/40), its reduction to F_641 and no-signalling. The exhaustive 80³ CHSH
# sweep runs in floating point, in the chart. It reaches 2√2 and never exceeds it. In ℤ[ζ_8] the optimum is
# S = 2(ζ_8 + ζ_8^{-1}), with S² = 8.
@R.block("C", BLOCK["C"])
def block_C():
    """Block C — composite.py, the composite gate (EXACT; C7 CHART, by certified brackets): C1–C8, the package's 12 checks C1–C8."""
    p, g = 641, 3
    N = p - 1
    gO = pow(g, N // 16, p)
    ok = p % 4 == 1 and arith.order(g, p) == N and gO == 601 and arith.order(gO, p) == 16
    ok &= N % 40 == 0 and N % 16 == 0 and gcd(40, 16) == 8 and 16 // 8 == 2 and pow(gO, 8, p) == p - 1
    R.check("C1", "F_641 = 4*160 + 1, g = 3 primitive, g_O = 601 of order 16, g_O^8 = -1; 40 | 640, 16 | 640, core gcd(40, 16) = 8, quotient C_2", ok)

    HO = [pow(gO, j, p) for j in range(16)]
    off = lambda u, v: u * pow(v, -1, p) % p
    ok = all(off(gO * u % p, gO * v % p) == off(u, v) for u in HO for v in HO)
    orbit, (u, v) = {(1, 1)}, (1, 1)
    for _ in range(16):
        u, v = gO * u % p, gO * v % p; orbit.add((u, v))
    R.check("C2", "the drive conserves the relative offset on all 256 pairs; the synchronised orbit (the Bell state) has length 16", ok and len(orbit) == 16)

    core = [pow(gO, 2 * l, p) for l in range(8)]
    ok = True
    for s in range(16):
        r = s % 8
        for j in range(80):
            lam = pow(g, 8 * j, p)
            psi = lambda w: (pow(w, s, p) + lam * pow(w, s + 8, p)) % p
            P0 = sum((pow(k, (8 - r) % 8, p) if r else 1) * psi(k) for k in core) % p
            P1 = sum((pow(k, (8 - r) % 8, p) if r else 1) * psi(gO * k % p) for k in core) % p
            ok &= P0 == 8 * (1 + lam) % p and P1 == 8 * pow(gO, s, p) * (1 - lam) % p
    # 22:C16 (p22032)
    R.check("C3", "the doublet readout psi = u^s + lam u^{s+8}: Psi(0) = 8(1 + lam), Psi(1) = 8 g_O^s (1 - lam), a sigma_x measurement (16 windings x 80 settings)", ok)

    Z = Cyclotomic(80)
    red8 = pow(g, 8, p)                                                       # the shadow of zeta_80
    ok4 = ok5 = ok6 = True
    for D in range(80):
        lam, lamc = Z.zeta(D), Z.zeta(-D)
        w = {}
        for al in (0, 1):
            for be in (0, 1):
                sg = 1 if (al + be) % 2 == 0 else -1
                w[(al, be)] = Z.mul(Z.add(Z.one, Z.scale(sg, lam)), Z.add(Z.one, Z.scale(sg, lamc)))
                lp = pow(red8, D, p)
                ok5 &= Z.shadow(w[(al, be)], p, red8) == (1 + sg * lp) * (1 + sg * pow(lp, -1, p)) % p
        ok4 &= Z.sum(w.values()) == Z.const(8)
        ok4 &= Z.sub(Z.add(w[(0, 0)], w[(1, 1)]), Z.add(w[(0, 1)], w[(1, 0)])) == Z.add(Z.zeta(D, 4), Z.zeta(-D, 4))
        ok6 &= all(Z.add(w[(al, 0)], w[(al, 1)]) == Z.const(4) for al in (0, 1))
    # 22:C17 (p22033)
    R.check("C4", "the singlet law: total weight 8 and E(Delta) = (zeta^D + zeta^-D)/2 = cos(pi Delta/40) exactly, all 80 settings (Z[zeta_80])", ok4)
    R.check("C5", "the composite reduction commutes: Z[zeta_80] -> F_641, zeta_80 -> g^8, on all weights", ok5)
    R.check("C6", "no-signalling: each marginal is 4 of 8 = 1/2 exactly, independent of the far setting", ok6)

    below, at, over = CQ.chsh_bound(80)                                       # every triple's S bracketed by certified cosines
    two_root_two = Z.scale(2, Z.add(Z.zeta(10), Z.zeta(-10)))                   # 2(zeta_8 + zeta_8^-1) = 2 sqrt 2 in Z[zeta_80]
    E_exact = lambda D: Z.scale(Fr(1, 2), Z.add(Z.zeta(D), Z.zeta(-D)))
    saturate = all(Z.sub(Z.sum([E_exact(d1), E_exact(d2), E_exact(d3)]), E_exact(d4)) == two_root_two for d1, d2, d3, d4 in at)
    R.check("C7", "the exhaustive 80^3 CHSH sweep never exceeds 2 sqrt 2: every triple's S lies below the bracket of 2 sqrt 2 by certified cosine brackets, except the saturating triples, where S = 2(zeta_8 + zeta_8^-1) exactly in Z[zeta_80]",
            below + len(at) == 80 ** 3 and not over and len(at) > 0 and saturate, f"{below} triples below, {len(at)} saturating {at}", kind="CHART")

    Z8 = Cyclotomic(8)
    S8 = Z8.sub(Z8.scale(Fr(3, 2), Z8.add(Z8.zeta(1), Z8.zeta(-1))), Z8.scale(Fr(1, 2), Z8.add(Z8.zeta(3), Z8.zeta(-3))))
    # 22:X7 (p22050), 22:C25 (p22041)
    R.check("C8", "Tsirelson saturation as a ring identity: S = 3 cos(pi/4) - cos(3 pi/4) = 2(zeta_8 + zeta_8^-1) in Z[zeta_8], S^2 = 8",
            S8 == Z8.scale(2, Z8.add(Z8.zeta(1), Z8.zeta(-1))) and Z8.mul(S8, S8) == Z8.const(8))


# ------------------------------------------------------------------------------------------------------------
# block U: the unequal-cycle gate (composite.py, U1–U6, 22:C26)
# On F_421 the pair S_61 x O_29 has the cycles C_60 and C_28. The joint recurrence is lcm = 420, and the four gcd-offset
# sectors are conserved. The recurrence T' = lcm(n_j / gcd(s_j, n_j)) is checked for every winding vector. Four
# characters are orbit-trivial, and the other 1676 cancel. The cancellation holds in the Carrier too. The last check is
# the Born window guard of the worked pair state.
@R.block("U", BLOCK["U"])
def block_U():
    """Block U — composite.py, the unequal-cycle gate (EXACT): U1–U6, the package's 6 checks."""
    p, g, n1, n2 = 421, 2, 60, 28
    N = p - 1
    R.check("U1", "421 = 4*105 + 1, g = 2 primitive; 60, 28 | 420; gcd(60, 28) = 4 = |Q4|, lcm = 420",
            p % 4 == 1 and arith.order(g, p) == N and N % n1 == 0 and N % n2 == 0 and gcd(n1, n2) == 4 and lcm(n1, n2) == 420)
    T = lcm(n1, n2)
    orbit, a, b = set(), 0, 0
    for _ in range(T):
        orbit.add((a, b)); a, b = (a + 1) % n1, (b + 1) % n2
    sectors = {}
    for a0 in range(n1):
        for b0 in range(n2): sectors[(a0 - b0) % 4] = sectors.get((a0 - b0) % 4, 0) + 1
    a, b, cons = 7, 3, True
    for _ in range(T):
        a, b = (a + 1) % n1, (b + 1) % n2; cons &= (a - b) % 4 == (7 - 3) % 4
    # 22:C26 (p22042)
    R.check("U2", "the unit-winding joint orbit has length 420; 1680/420 = 4 sectors of 420 each; the gcd-offset a - b mod 4 is conserved over the recurrence",
            len(orbit) == T and n1 * n2 // T == 4 and cons and sorted(sectors) == [0, 1, 2, 3] and all(c == 420 for c in sectors.values()))
    ok = True
    for s1 in range(n1):
        for s2 in range(n2):
            t = next(t for t in range(1, n1 * n2 + 1) if (t * s1) % n1 == 0 and (t * s2) % n2 == 0)
            ok &= t == lcm(n1 // gcd(s1, n1), n2 // gcd(s2, n2))
    R.check("U3", "T' = lcm(n_j/gcd(s_j, n_j)) is the recurrence of every one of the 1680 winding vectors", ok)
    triv = sum(1 for k1 in range(n1) for k2 in range(n2) if (7 * k1 + 15 * k2) % 420 == 0)
    ok = triv == 4 and n1 * n2 - triv == 1676
    for k1, k2 in [(1, 0), (0, 1), (7, 3), (59, 27), (30, 14), (2, 25)]:
        e = (7 * k1 + 15 * k2) % 420
        if e == 0: continue
        hits = {}
        for t in range(420): hits[e * t % 420] = hits.get(e * t % 420, 0) + 1
        ok &= set(hits) == set(range(0, 420, gcd(e, 420))) and all(c == gcd(e, 420) for c in hits.values())
    R.check("U4", "4 orbit-trivial characters (the sector labels), 1676 nontrivial; the sampled nontrivial characters cancel exactly over one recurrence", ok)
    ok = True
    for k in [1, 3, 10, 100]:
        z = pow(g, k, p)
        ok &= (sum(pow(z, t, p) for t in range(420)) % p == 0) == (k % 420 != 0)
    R.check("U5", "the carrier-internal reduction: the nontrivial character sums vanish in F_421", ok)
    R.check("U6", "the Born window guard of the worked pair state: 4 ||psi||^2 = 16 < 421", 4 * 4 < p)


# ------------------------------------------------------------------------------------------------------------
# block M: m-body synchronisation (synchronisation.py, 22:C15)
# The cycles C_N are equal, and the single drive acts diagonally on C_N^m. The offset vector ρ(u) = (u_i u_1^{-1}) is
# conserved on every configuration. Every orbit has length N, and ρ labels the N^{m-1} orbits bijectively. The
# synchronised orbit is the unique one with ρ = 1, and on it |Σ_i χ(u_i)|² = m². Over an offset-uniform sector the
# average is m, by the orthogonality of the characters (exact in ℤ[ζ_N]). The checks are exhaustive on F_641/C_16
# (m ≤ 4) and on F_13/C_4 (m ≤ 6).
@R.block("M", BLOCK["M"])
def block_M():
    """Block M — synchronisation.py (EXACT): M1–M5, the package's 26 checks."""
    CARRIERS = [(641, 3, 16), (13, 2, 4)]
    CASES = [(0, 2), (0, 3), (0, 4), (1, 2), (1, 3), (1, 4), (1, 6)]
    ok = all(p % 4 == 1 and arith.order(g, p) == p - 1 and arith.order(pow(g, (p - 1) // N, p), p) == N and (p - 1) % N == 0
             for p, g, N in CARRIERS)
    R.check("M1", "F_641 (C_16, g_0 = 601, as in the composite gate) and F_13 (C_4): admissible carriers and drives", ok and pow(3, 640 // 16, 641) == 601)
    ok2 = ok3 = ok4 = True; det = []
    for ci, m in CASES:
        p, g, N = CARRIERS[ci]
        g0 = pow(g, (p - 1) // N, p)
        H = [pow(g0, j, p) for j in range(N)]
        inv = {h: pow(h, -1, p) for h in H}
        drive = lambda u: tuple(g0 * x % p for x in u)
        rho = lambda u: tuple(x * inv[u[0]] % p for x in u[1:])
        configs = list(product(H, repeat=m))
        ok2 &= len(configs) == N ** m and all(rho(drive(u)) == rho(u) for u in configs)
        seen, orbits = set(), []
        for u in configs:
            if u in seen: continue
            orb, x = [], u
            for _ in range(N + 1):
                orb.append(x); seen.add(x); x = drive(x)
                if x == u: break
            orbits.append(orb)
        fibres = {}
        for u in configs: fibres.setdefault(rho(u), []).append(u)
        ok3 &= all(len(o) == N for o in orbits) and len(orbits) == N ** (m - 1)
        ok3 &= all(len({rho(x) for x in o}) == 1 for o in orbits) and len({rho(o[0]) for o in orbits}) == len(orbits)
        ok3 &= len(fibres) == N ** (m - 1) and all(len(f) == N for f in fibres.values())
        ok4 &= set(fibres[(1,) * (m - 1)]) == {(w,) * m for w in H}
        Z = Cyclotomic(N)
        for s in range(N):                                                    # on Δ all m phases coincide
            for k in range(N):
                S = Z.sum(Z.zeta(k * s) for _ in range(m))
                ok4 &= S == Z.zeta(k * s, m) and Z.norm2(S) == Z.const(m * m)
        det.append(f"F_{p} C_{N} m={m}: {N ** m} configs, {len(orbits)} orbits")
    R.check("M2", "the offset vector is conserved by the drive on every configuration (all seven cases)", ok2, "; ".join(det))
    # 22:C15 (p22031)
    R.check("M3", "every orbit has length N, there are N^(m-1) orbits, and the offset vector labels them bijectively (each fibre is one orbit)", ok3)
    R.check("M4", "the synchronised orbit is the unique zero-offset orbit, of length N; on it sum_i chi(u_i) = m chi(w), |.|^2 = m^2 exactly (Z[zeta_N])", ok4)
    zero = lambda N, k: Cyclotomic(N).sum(Cyclotomic(N).zeta(k * s) for s in range(N)) == Cyclotomic(N).zero
    ok = all(zero(N, k) for _, _, N in CARRIERS for k in range(1, N))
    ok &= all(zero(N, k) for N, m, k in [(4, 2, 1), (4, 3, 1), (4, 3, 2), (4, 6, 3), (16, 2, 1), (16, 3, 5)])
    R.check("M5", "character orthogonality sum_s zeta_N^{ks} = 0 (k != 0) for every nontrivial character of C_16 and C_4, so the offset-uniform average |sum_i chi(u_i)|^2 is m", ok)


# ------------------------------------------------------------------------------------------------------------
# block R: the real-versus-complex network (renou.py, 22:C18, P3)
# Two sources each emit |Φ+⟩. Alice measures X, Y and Z, Bob makes the Bell-state measurement, and Charlie measures the
# six (A ± B)/√2. The arithmetic is exact in Q(ζ_8), with √2 = ζ − ζ³ and i = ζ². Bob's four orbit-sector states are
# the Bell basis, and entanglement swapping holds. The conditional correlation table of the network equals the
# complex-quantum table entry by entry. The canonical witness is 6√2 exactly, above the protocol's real-quantum bound
# 7.6605. The sources are independent: the state factorises across the source cut, the two offsets are separately
# conserved, and the joint sector distribution is a product.
@R.block("R", BLOCK["R"])
def block_R():
    """Block R — renou.py (EXACT): R1–R5, the package's 10 checks."""
    Z = Cyclotomic(8)
    ZERO, ONE, I8 = Z.zero, Z.one, Z.zeta(2)
    S2 = Z.sub(Z.zeta(1), Z.zeta(3))                                          # √2
    HALF, S2INV = Z.const(Fr(1, 2)), Z.scale(Fr(1, 2), S2)
    def mat(a, b, c, d): return ((a, b), (c, d))
    X, Y, Zm = mat(ZERO, ONE, ONE, ZERO), mat(ZERO, Z.neg(I8), I8, ZERO), mat(ONE, ZERO, ZERO, Z.neg(ONE))
    ID = mat(ONE, ZERO, ZERO, ONE)
    madd = lambda A, B: tuple(tuple(Z.add(A[i][j], B[i][j]) for j in range(2)) for i in range(2))
    msca = lambda s, A: tuple(tuple(Z.mul(s, A[i][j]) for j in range(2)) for i in range(2))
    neg = lambda A: msca(Z.neg(ONE), A)
    AX = [X, Y, Zm]
    CZ = [msca(S2INV, madd(X, Y)), msca(S2INV, madd(X, neg(Y))), msca(S2INV, madd(Y, Zm)), msca(S2INV, madd(Y, neg(Zm))),
          msca(S2INV, madd(X, Zm)), msca(S2INV, madd(X, neg(Zm)))]
    ket = lambda k: {k: ONE}
    def kadd(u, v):
        w = dict(u)
        for k, a in v.items(): w[k] = Z.add(w.get(k, ZERO), a)
        return {k: a for k, a in w.items() if a != ZERO}
    ksca = lambda s, u: {k: Z.mul(s, a) for k, a in u.items()}
    def braket(u, v): return Z.sum(Z.mul(Z.conj(u[k]), a) for k, a in v.items() if k in u)
    bit = lambda k, q: (k >> (3 - q)) & 1
    def apply1(M, q, u):
        out = {}
        for k, a in u.items():
            for nb in (0, 1):
                if M[nb][bit(k, q)] != ZERO:
                    nk = (k & ~(1 << (3 - q))) | (nb << (3 - q))
                    out[nk] = Z.add(out.get(nk, ZERO), Z.mul(M[nb][bit(k, q)], a))
        return {k: a for k, a in out.items() if a != ZERO}
    PSI = {}
    for a in (0, 1):
        for c in (0, 1): PSI = kadd(PSI, ket((a << 3) | (a << 2) | (c << 1) | c))   # |a a c c⟩
    def bell(off, sgn):
        return kadd(ket(0b0000), ksca(Z.const(sgn), ket(0b0110))) if off == 0 else kadd(ket(0b0100), ksca(Z.const(sgn), ket(0b0010)))
    BELL = {("Phi", 1): bell(0, 1), ("Phi", -1): bell(0, -1), ("Psi", 1): bell(1, 1), ("Psi", -1): bell(1, -1)}
    R.check("R1", "Bob's four orbit-sector states are the Bell basis: <b|b'> = 2 delta, exact",
            all(braket(BELL[x], BELL[y]) == (Z.const(2) if x == y else ZERO) for x in BELL for y in BELL))

    def project_b(off, sgn, u):
        out = {}
        for k, a in u.items():
            b1, b2 = bit(k, 1), bit(k, 2)
            comp = {(0, (0, 0)): ONE, (0, (1, 1)): Z.const(sgn), (1, (0, 1)): ONE, (1, (1, 0)): Z.const(sgn)}.get((off, (b1, b2)))
            if comp is None: continue
            out[k & 0b1001] = Z.add(out.get(k & 0b1001, ZERO), Z.mul(Z.conj(comp), a))
        return out
    SIG = {("Phi", 1): ID, ("Phi", -1): Zm, ("Psi", 1): X, ("Psi", -1): None}
    def reference(name_sgn):
        ref = kadd(ket(0b0000), ket(0b1001))
        return apply1(SIG[name_sgn], 3, ref) if SIG[name_sgn] is not None else apply1(Zm, 3, apply1(X, 3, ref))
    ok = True
    for (name, sgn) in SIG:
        cond, ref = project_b(0 if name == "Phi" else 1, sgn, PSI), reference((name, sgn))
        lam, good = None, True
        for k in set(cond) | set(ref):
            c, r = cond.get(k, ZERO), ref.get(k, ZERO)
            if r == ZERO:
                good &= c == ZERO; continue
            l = c if r == ONE else Z.neg(c)
            if lam is None: lam = l
            elif l != lam: good = False
        ok &= good and lam is not None and lam != ZERO
    R.check("R2", "entanglement swapping: conditioned on Bob's outcome b the A-C state is (1 x sigma_b)|Phi+>, all four outcomes, exact", ok)

    expect2 = lambda A, C, u: braket(u, apply1(A, 0, apply1(C, 3, u)))
    okT = okP = True; table = {}
    for (name, sgn) in BELL:
        cond = project_b(0 if name == "Phi" else 1, sgn, PSI)
        okP &= braket(cond, cond) == Z.const(2)
        ref = reference((name, sgn))
        for xi, A in enumerate(AX):
            for zi, C in enumerate(CZ):
                t = Z.mul(expect2(A, C, cond), HALF)
                okT &= t == Z.mul(expect2(A, C, ref), HALF)
                table[(name, sgn, xi, zi)] = t
    # The complex-quantum table in closed form, written without the operators: on (1 x sigma_b)|Phi+> the expectation
    # <P x P'> is [P = P'] e(P) s_b(P) with e(X) = e(Z) = 1, e(Y) = -1 (Y^T = -Y) and s_b(P) = +-1 as sigma_b commutes
    # or anticommutes with P; C_z = (P_u +- P_v)/sqrt2 gives (e(u) s_b(u) [A = P_u] +- e(v) s_b(v) [A = P_v])/sqrt2.
    E_ = {"X": 1, "Y": -1, "Z": 1}
    comm = lambda a, b: 1 if (a == b or a == "I" or b == "I") else -1
    SIGB = {("Phi", 1): "I", ("Phi", -1): "Z", ("Psi", 1): "X", ("Psi", -1): "Y"}
    CZn, AXn = [("X", "Y", 1), ("X", "Y", -1), ("Y", "Z", 1), ("Y", "Z", -1), ("X", "Z", 1), ("X", "Z", -1)], ["X", "Y", "Z"]
    def closed(name, sgn, xi, zi):
        u, w, sg = CZn[zi]; a_, sb = AXn[xi], SIGB[(name, sgn)]
        return Z.scale(Fr((E_[u] * comm(sb, u) if a_ == u else 0) + sg * (E_[w] * comm(sb, w) if a_ == w else 0)), S2INV)
    okC = all(table[k] == closed(*k) for k in table) and len(table) == 72 and Z.mul(S2, S2) == Z.const(2) and S2 != ZERO
    # 22:C18 (p22034)
    R.check("R3", "P(b) = 1/4 for each Bell outcome; the full conditional table <A_x C_z | b> (3 x 6 x 4 entries) equals the complex-quantum table exactly, computed in closed form from the Pauli commutation signs (entries 0 and +-1/sqrt2), and the reference states",
            okT and okP and okC)

    def gt_q2(x, y):                                                          # a + b√2 > c + d√2, exactly
        pp, q = x[0] - y[0], x[1] - y[1]
        if q == 0: return pp > 0
        if pp >= 0 and q > 0: return True
        if pp <= 0 and q < 0: return False
        if pp > 0 and q < 0: return pp * pp > 2 * q * q
        return 2 * q * q > pp * pp
    pairs = {("X", "Y"): (0, 1, 0, 1), ("Y", "Z"): (1, 2, 2, 3), ("X", "Z"): (0, 2, 4, 5)}
    score = ZERO
    for (name, sgn) in BELL:
        for (xj, xk, zp, zm) in pairs.values():
            best = None
            for s1, s2, s3, s4 in product((1, -1), repeat=4):
                v = Z.sum([Z.scale(s1, table[(name, sgn, xj, zp)]), Z.scale(s2, table[(name, sgn, xk, zp)]),
                           Z.scale(s3, table[(name, sgn, xj, zm)]), Z.scale(s4, table[(name, sgn, xk, zm)])])
                rp = (v[0], (v[1] - v[3]) * Fr(1, 2))                         # Re v = v0 + (v1 − v3)/2 · √2
                if best is None or gt_q2(rp, best[0]): best = (rp, v)
            score = Z.add(score, best[1])
    # 22:P3 (p22054)
    R.check("R4", "the canonical witness: score/4 = 6 sqrt 2 = 6(zeta - zeta^3) exactly (score 24 sqrt 2), three conditional CHSH at 2 sqrt 2; 72 > 7.6605^2, above the real-quantum bound",
            Z.scale(Fr(1, 4), score) == Z.scale(6, S2) and score == Z.scale(24, S2) and Z.is_rational(Z.norm2(Z.scale(Fr(1, 4), score)))
            and Z.norm2(Z.scale(Fr(1, 4), score))[0] == 72 and 72 > Fr(76605, 10000) ** 2)

    def k_of(i, j): return ((i >> 1) << 3) | ((i & 1) << 2) | ((j >> 1) << 1) | (j & 1)
    amp = [[PSI.get(k_of(i, j), ZERO) for j in range(4)] for i in range(4)]
    src = [ONE, ZERO, ZERO, ONE]
    ok5a = all(Z.sub(Z.mul(amp[i][j], amp[i2][j2]), Z.mul(amp[i][j2], amp[i2][j])) == ZERO for i, i2, j, j2 in product(range(4), repeat=4))
    ok5a &= all(amp[i][j] == Z.mul(src[i], src[j]) for i in range(4) for j in range(4))
    def drive_pair(u, qx, qy):
        out = {}
        for k, a in u.items():
            nk = k ^ (1 << (3 - qx)) ^ (1 << (3 - qy)); out[nk] = Z.add(out.get(nk, ZERO), a)
        return {k: a for k, a in out.items() if a != ZERO}
    offset = lambda k, qx, qy: bit(k, qx) ^ bit(k, qy)
    D1, D2 = (lambda u: drive_pair(u, 0, 1)), (lambda u: drive_pair(u, 2, 3))
    ok5b = True
    for k in range(16):
        k1, k2 = next(iter(D1(ket(k)))), next(iter(D2(ket(k))))
        ok5b &= offset(k1, 0, 1) == offset(k, 0, 1) and offset(k2, 2, 3) == offset(k, 2, 3)
        ok5b &= offset(k1, 2, 3) == offset(k, 2, 3) and offset(k2, 0, 1) == offset(k, 0, 1) and D1(D2(ket(k))) == D2(D1(ket(k)))
    wt, tot = {}, ZERO
    for k, a in PSI.items():
        w = Z.mul(Z.conj(a), a); s = (offset(k, 0, 1), offset(k, 2, 3))
        wt[s] = Z.add(wt.get(s, ZERO), w); tot = Z.add(tot, w)
    m1, m2 = {0: ZERO, 1: ZERO}, {0: ZERO, 1: ZERO}
    for (o1, o2), w in wt.items(): m1[o1] = Z.add(m1[o1], w); m2[o2] = Z.add(m2[o2], w)
    ok5c = all(Z.mul(wt.get((o1, o2), ZERO), tot) == Z.mul(m1[o1], m2[o2]) for o1 in (0, 1) for o2 in (0, 1))
    R.check("R5", "source independence: the state factorises across the source cut (every 2 x 2 minor vanishes); the two offsets are separately conserved by commuting drives; the joint sector distribution is the product of its marginals",
            ok5a and ok5b and ok5c)


# ------------------------------------------------------------------------------------------------------------
# block B: the gravitational channel (bmv.py, 22:C19, P1)
# Two clusters in path superposition carry the conditional phase ζ_80^k on |11⟩, with amplitudes (1, 1, 1, ζ^k). At
# k = 0 the state is a product. Over the sweep C² = |ad − bc|²/4 = sin²(φ/2) exactly. The Horodecki bound is
# S²_max = 4 + |ad − bc|², above 4 for k ≠ 0 and equal to 8 at φ = π. The coupling commutes with the drive, and Alice's
# marginal ignores Bob's local operations. The complementarity V² + C² = 1 holds as a ring identity.
@R.block("B", BLOCK["B"])
def block_B():
    """Block B — bmv.py (EXACT): B1–B5, the package's 6 checks."""
    Z = Cyclotomic(80)
    amps = lambda k: [Z.one, Z.one, Z.one, Z.zeta(k)]
    det = lambda a: Z.sub(Z.mul(a[0], a[3]), Z.mul(a[1], a[2]))
    R.check("B1", "zero coupling: ad - bc = 0 exactly, a product state (concurrence 0)", det(amps(0)) == Z.zero)
    c2 = [Z.norm2(det(amps(k))) for k in range(80)]
    # 22:C19 (p22035)
    R.check("B2", "4 C^2 = |ad - bc|^2 = 2 - zeta^k - zeta^-k, i.e. C^2 = sin^2(phi/2) exactly, the full sweep phi = 2 pi k/80",
            all(c2[k] == Z.sub(Z.const(2), Z.add(Z.zeta(k), Z.zeta(-k))) for k in range(80)))
    smax2 = [Z.add(Z.const(4), c) for c in c2]
    R.check("B3", "Horodecki S_max^2 = 4(1 + C^2) = 4 + |ad - bc|^2: above 4 for every k != 0, and 8 (S_max = 2 sqrt 2) at phi = pi",
            all(c2[k] != Z.zero for k in range(1, 80)) and smax2[40] == Z.const(8))
    II, ONE, ZERO = Z.zeta(20), Z.one, Z.zero
    locB = [[[ZERO, ONE], [ONE, ZERO]], [[ONE, ZERO], [ZERO, Z.neg(ONE)]], [[ZERO, Z.neg(II)], [II, ZERO]]]
    rhoA = lambda psi: [[Z.add(Z.mul(psi[2 * a], Z.conj(psi[2 * b])), Z.mul(psi[2 * a + 1], Z.conj(psi[2 * b + 1]))) for b in (0, 1)] for a in (0, 1)]
    Dd = [ONE, II, II, Z.neg(ONE)]
    ok_a = ok_b = True
    for k in (1, 7, 20, 40, 63):
        Gd = [ONE, ONE, ONE, Z.zeta(k)]
        ok_a &= all(Z.mul(Gd[j], Dd[j]) == Z.mul(Dd[j], Gd[j]) for j in range(4))
        psi = amps(k)
        for U in locB:
            psiU = [Z.add(Z.mul(U[b][0], psi[2 * a]), Z.mul(U[b][1], psi[2 * a + 1])) for a in (0, 1) for b in (0, 1)]
            ok_b &= rhoA(psiU) == rhoA(psi)
    R.check("B4", "the coupling commutes with the diagonal drive (offset-diagonal); Alice's reduced state is invariant under Bob's local X, Y, Z (no signalling), exact", ok_a and ok_b)
    # The visibility from the reduced state: for the unnormalised amplitudes (1, 1, 1, zeta^k) the norm is 4 and
    # Alice's reduced matrix has the off-diagonal rho_01 = (1 + zeta^-k)/4, so V = 2 |rho_01| gives 4 V^2 = |1 + zeta^k|^2;
    # the concurrence from the determinant (B2): 4 C^2 = |ad - bc|^2. Their sum is computed, not asserted.
    ok = True
    for k in range(80):
        rho = rhoA(amps(k))
        v2 = Z.norm2(rho[0][1])                                               # 4 V^2 = |rho_01|^2 (the norm 4 absorbed)
        ok &= Z.add(v2, c2[k]) == Z.const(4) and v2 == Z.add(Z.const(2), Z.add(Z.zeta(k), Z.zeta(-k)))
    ok &= Z.norm2(rhoA(amps(0))[0][1]) == Z.const(4) and Z.norm2(rhoA(amps(40))[0][1]) == Z.zero
    # 22:P1 (p22052)
    R.check("B5", "the complementarity V^2 + C^2 = 1 over the full sweep, with 4V^2 = |rho_01|^2 computed from Alice's reduced state and 4C^2 = |ad - bc|^2 from the determinant: the sum is 4 at every k, V = 1 at k = 0 and V = 0 at the half turn", ok)


# ------------------------------------------------------------------------------------------------------------
# block Q: the decoherence floor (decoherence.py, 22:C7, C20)
# Over ℚ(ζ_40) an isolated doublet keeps contrast 1 at every drive time. The dilation dephasing V(τ)² = |Σ_E p_E ζ^{Eτ}|²
# is real and equals 1 at τ = 0. Its Gaussian envelope for the binomial distribution is computed in floating point, in
# the chart. The revival V(40)² = 1 is exact. Over ℤ[ζ_7] (F_421, O_29, quotient C_7) the snapshot pair-count of
# ψ_0 + ψ_4 is not an integer. The registered drive-frequency count over the recurrence lcm(60, 28) = 420 is 13440 for
# every outcome, so P = 1/7.
@R.block("Q", BLOCK["Q"])
def block_Q():
    """Block Q — decoherence.py (EXACT; Q3 CHART): Q1–Q7, the package's 7 checks."""
    n = 40
    Z = Cyclotomic(n)
    ok = True
    for j in (0, 3, 11):
        for tau in (0, 1, 5, 17, 39):
            vals = [Z.add(Z.const(2), Z.add(Z.zeta(j + 8 * tau + jp), Z.zeta(-(j + 8 * tau + jp)))) for jp in range(n)]
            ok &= Z.const(4) in vals and Z.zero in vals
    # 22:C20 (p22036)
    R.check("Q1", "an isolated doublet keeps fringe contrast 1 exactly (weights 4 and 0 both occur) at every drive time and phase: no spontaneous collapse", ok)
    M = 8
    pE = {E: Fr(comb(M, E), 2 ** M) for E in range(M + 1)}
    def V2(tau):
        s = Z.from_exponents((E * tau, c) for E, c in pE.items())
        return Z.norm2(s)
    R.check("Q2", "V(tau)^2 = |characteristic function of the internal windings|^2 is real for every drive time and 1 at tau = 0, exact",
            all(V2(t) == Z.conj(V2(t)) for t in range(n)) and V2(0) == Z.one)
    env = CQ.envelope(M, n, (1, 2, 3, 4))
    R.check("Q3", "the Gaussian envelope V = exp(-sigma^2 theta^2/2) of the binomial distribution (sigma^2 = M/4) within 0.02, tau = 1..4: the large-M image of the exact ring form",
            all(abs(chi - ga_) <= Fr(2, 100) for _, chi, ga_ in env), "; ".join(f"tau={t}: {chi:.4f} vs {ga_:.4f}" for t, chi, ga_ in env), kind="CHART")
    R.check("Q4", "the exact revival V(n)^2 = 1 at the cycle period n = 40: dephasing, never collapse", V2(n) == Z.one)

    Z7 = Cyclotomic(7)
    T7 = lcm(60, 28)
    Psi = lambda a: Z7.scale(4, Z7.add(Z7.one, Z7.zeta(a)))
    snap = [Z7.norm2(Psi(a)) for a in range(7)]
    tot = Z7.sum(snap)
    R.check("Q5", "the snapshot pair-count w_0(1) = 16(2 + zeta_7 + zeta_7^-1) is a real algebraic integer not in Z; the sum over the seven outcomes is 224",
            not Z7.is_rational(snap[1]) and tot == Z7.const(224))
    W = [Z7.sum(Z7.norm2(Psi(a - t)) for t in range(T7)) for a in range(7)]
    Wv = [w[0] for w in W]
    R.check("Q6", "the registered drive-frequency count W_0(a) = 13440 = 420 * 32 for every outcome over the recurrence T = lcm(60, 28) = 420: an ordinary integer, uniform",
            all(Z7.is_rational(w) for w in W) and len(set(Wv)) == 1 and Wv[0] == 13440)
    R.check("Q7", "the registered probability P_0(a) = 1/7; the count per chronon is 32 = |c_0|^2 + |c_4|^2 (incoherent)",
            Fr(Wv[0], sum(Wv)) == Fr(1, 7) and Wv[0] // T7 == 16 + 16)


# ------------------------------------------------------------------------------------------------------------
# block E: the two scaling laws and the equivalence principle (equivalence.py, 22:C22)
# The Poisson equation on the periodic 4 x 4 x 4 lattice is solved exactly over ℚ, in the zero-mean gauge. The field is
# linear in its sources, and a cluster of m sources has coefficient exactly m. The acceleration of a locked test cluster
# is independent of its mass, so η = 0. For unlocked phases E|Σζ^θ|² = m by character orthogonality, against m² for a
# locked cluster. The sampled √m scaling runs in floating point, in the chart. In the package it is an illustration
# that decides nothing.
@R.block("E", BLOCK["E"])
def block_E():
    """Block E — equivalence.py (EXACT): E1–E4, the package's exact checks (its sampled illustration, which decided nothing, is not carried)."""
    L = 4; Ncell = L ** 3
    idx = lambda x, y, z: (x % L) * L * L + (y % L) * L + (z % L)
    A = [[0] * Ncell for _ in range(Ncell)]
    for X, Y, Zc in product(range(L), repeat=3):
        i = idx(X, Y, Zc); A[i][i] = -6
        for dx, dy, dz in ((1, 0, 0), (-1, 0, 0), (0, 1, 0), (0, -1, 0), (0, 0, 1), (0, 0, -1)): A[i][idx(X + dx, Y + dy, Zc + dz)] += 1
    def solve(rhos):
        """A u = −(ρ − mean ρ) with Σu = 0 (the last row replaced by the gauge), by Gauss–Jordan over ℚ, every ρ at once."""
        Mx = [[Fr(a) for a in A[i]] + [-(Fr(r[i]) - Fr(sum(r), Ncell)) for r in rhos] for i in range(Ncell)]
        Mx[-1] = [Fr(1)] * Ncell + [Fr(0)] * len(rhos)
        for col in range(Ncell):
            piv = next(r for r in range(col, Ncell) if Mx[r][col] != 0)
            Mx[col], Mx[piv] = Mx[piv], Mx[col]
            pv = Mx[col][col]; Mx[col] = [v / pv for v in Mx[col]]
            for r in range(Ncell):
                if r != col and Mx[r][col] != 0:
                    f = Mx[r][col]; Mx[r] = [vr - f * vc for vr, vc in zip(Mx[r], Mx[col])]
        return [[Mx[i][Ncell + j] for i in range(Ncell)] for j in range(len(rhos))]
    rho1, rho2, unit = [0] * Ncell, [0] * Ncell, [0] * Ncell
    rho1[idx(0, 0, 0)] = 3; rho2[idx(2, 1, 3)] = 7; unit[idx(0, 0, 0)] = 1
    u1, u2, u12, uu = solve([rho1, rho2, [a + b for a, b in zip(rho1, rho2)], unit])
    R.check("E1", "exact superposition on the lattice: u(m1 + m2) = u(m1) + u(m2) in all 64 cells (rational arithmetic)", all(a + b == c for a, b, c in zip(u1, u2, u12)))
    # 22:C22 (p22038)
    R.check("E2", "the source coefficient is exactly m: u(m = 3 cluster) = 3 u(unit), every cell, and u(m = 7) = 7 u(unit) (the field linear in its sources, coefficient m)",
            all(3 * a == b for a, b in zip(uu, u1)) and solve([[7 * r for r in unit]])[0] == [7 * a for a in uu])
    # The pull on a locked test cluster of m_t unit cells at a probe of nonzero gradient: each cell responds to the
    # solved field, so the pull is m_t times the gradient and the acceleration pull/m_t is the gradient, for m_t = 3
    # and 7 — the lattice model's reading of eta = 0 (the row's exact content is E1, E2 and E4; this is their consequence).
    probe = next(P for P in product(range(L), repeat=3) if u12[idx(P[0] + 1, P[1], P[2])] - u12[idx(P[0] - 1, P[1], P[2])] != 0)
    gx = u12[idx(probe[0] + 1, probe[1], probe[2])] - u12[idx(probe[0] - 1, probe[1], probe[2])]
    pull = {mt: sum(gx for _ in range(mt)) for mt in (3, 7)}
    R.check("E3", "the equivalence principle as the model's null: at a probe of nonzero gradient the pull on a locked cluster of m_t cells is m_t times the gradient, so the acceleration pull/m_t is the gradient for m_t = 3 and 7 (eta = 0 by construction, the content being E1, E2, E4)",
            gx != 0 and all(pull[mt] / mt == gx for mt in (3, 7)), f"probe {probe}, grad u = {gx}")
    Z8 = Cyclotomic(8)
    R.check("E4", "unlocked phases: E|sum zeta^theta|^2 = m exactly (the m^2 - m cross terms vanish, sum_k zeta_8^k = 0); a locked cluster gives m^2, |5 zeta|^2 = 25",
            Z8.sum(Z8.zeta(k) for k in range(8)) == Z8.zero and Z8.norm2(Z8.zeta(1, 5)) == Z8.const(25))


# ------------------------------------------------------------------------------------------------------------
# block G: the granularity ceiling (granularity.py, 22:C14, P5)
# The arithmetic is exact in ℚ(ζ_8), with 1/√2 = (ζ − ζ³)/2. After k Hadamard layers the minimal denominator is
# 2^⌈k/2⌉, and the minimal tally norm is W(k) = 2^k (k even) or 2^(k+1) (k odd). The ceiling is the largest k with
# d·W(k) < Ω. In F_641 it is k* = 8 for the unit core and 6 for the Bell core (d = 8). At the master's anchor
# Ω ∼ 1.3 × 10^123 it is 408 and 204 at √Ω, by the bit length of the certified bracket's ends. Past k* two valid lifts
# give different Born ratios, and they differ by multiples of Ω. Over ℚ(i) the Gaussian Hadamard gives the same law.
@R.block("G", BLOCK["G"])
def block_G():
    """Block G — granularity.py (EXACT): G1–G7, the package's 7 checks (and the corpus ceilings it prints)."""
    Z = Cyclotomic(8)
    S2INV = Z.scale(Fr(1, 2), Z.sub(Z.zeta(1), Z.zeta(3)))
    ok1 = ok2 = True
    W = lambda k: 2 ** k if k % 2 == 0 else 2 ** (k + 1)
    for k in range(1, 13):
        amp = Z.const(Fr(1))
        for _ in range(k): amp = Z.mul(amp, S2INV)
        D = 1
        for f in amp:
            if f != 0: D = lcm(D, Fr(f).denominator)
        ints = [int(Fr(f) * D) for f in amp]
        ok1 &= D == 2 ** ((k + 1) // 2) and gcd(*ints) == 1
        n1 = Z.norm2(tuple(ints))
        ok2 &= Z.is_rational(n1) and 2 ** k * n1[0] == W(k)
    R.check("G1", "the denominator law: after k Hadamard layers the minimal denominator is 2^ceil(k/2), k = 1..12, exact in Q(zeta_8) (2 ramified)", ok1)
    R.check("G2", "the tally law: the minimal integer-tally norm is 2^k (k even) and 2^(k+1) (k odd), exactly", ok2)
    p = 641
    kstar, kstar8 = max(k for k in range(1, 12) if W(k) < p), max(k for k in range(1, 12) if 8 * W(k) < p)
    # 22:C14 (p22030)
    R.check("G3", "the exact ceilings in F_641: k* = max{k : W(k) < 641} = 8 (unit core, bit-length label 9); max{k : 8 W(k) < 641} = 6 (Bell core)",
            kstar == 8 and p.bit_length() - 1 == 9 and kstar8 == 6, f"k* = {kstar}, Bell core {kstar8}")
    # The ceiling at the master's anchor (00:A7, the scale import's certified bracket, frc/chart.py): T(k) < Omega iff
    # k + [k odd] <= floor(log2 Omega), the bit length less one, so k* = b - b % 2 for b = floor(log2 Omega); no number
    # above Omega is formed. Both ends of the bracket have bit length 410 (b = 409), and their integer square roots bit
    # length 205 (b = 204).
    lo, hi = CH.omega_bracket()
    ends = (int(lo), int(hi) + 1)
    bits = {e.bit_length() - 1 for e in ends}
    rbits = {isqrt(e).bit_length() - 1 for e in ends}
    kstar_of = lambda b: b - b % 2
    dO = {kstar_of(b) for b in bits}; dsO = {kstar_of(b) for b in rbits}
    passes = lambda k, b: k + k % 2 <= b                                      # W(k) = 2^(k + k%2) < Omega iff k + k%2 <= b, read on the exponent: no number above Omega is formed
    ok = len(bits) == 1 and len(rbits) == 1
    ok &= all(W(kstar_of(b)) < e and passes(kstar_of(b), b) and not passes(kstar_of(b) + 1, b) for b in bits for e in ends)
    ok &= all(W(kstar_of(b)) < isqrt(e) and passes(kstar_of(b), b) and not passes(kstar_of(b) + 1, b) for b in rbits for e in ends)
    ok &= all(e // 10 ** 123 == 1 for e in ends)
    # 22:P5 (p22056)
    R.check("G4", "the ceilings at the master's anchor Omega ~ 1.3 x 10^123 (the certified bracket of the scale import, 00:A7), by the bit length of its ends: k* = 408 for the unit core and 204 at the coherence horizon sqrt(Omega)",
            ok and dO == {408} and dsO == {204}, f"k* = {sorted(dO)} (Omega, bit length {sorted(b + 1 for b in bits)}), {sorted(dsO)} (sqrt Omega)")
    ok3a = ok3b = ok4 = True
    for k in range(1, 12):
        Wk = W(k); wplus = Wk // 2 + 2 ** (k // 2)
        if k <= kstar and Wk < p: ok3a &= wplus < p
        if Wk > p:
            sh = wplus % p
            ok4 &= (sh + p) - sh == p
            ok3b &= Fr(sh, Wk) != Fr(sh + p, Wk)
    R.check("G5", "sub-horizon depths have the unique window lift; past k* two valid lifts give different Born ratios (the ambiguity onset)", ok3a and ok3b)
    R.check("G6", "the lift discrepancies are multiples of p (wrap quantisation)", ok4)
    h = (Fr(1, 2), Fr(1, 2))
    H = [[h, h], [h, (-h[0], -h[1])]]
    Pm = [[ga(gm(H[a][0], gc(H[b][0])), gm(H[a][1], gc(H[b][1]))) for b in range(2)] for a in range(2)]
    ok7 = Pm == [[(1, 0), (0, 0)], [(0, 0), (1, 0)]] and all(gnorm(x) == Fr(1, 2) for row in H for x in row)
    for k in range(1, 13):
        z = (1, 0)
        for _ in range(k): z = (z[0] - z[1], z[0] + z[1])                     # (1 + i)^k
        den = 2 ** k
        g_ = gcd(gcd(abs(z[0]) or den, abs(z[1]) or den), den)
        ok7 &= den // g_ == 2 ** ((k + 1) // 2) and 2 ** k * 2 ** (2 * ((k + 1) // 2) - k) == W(k)
    R.check("G7", "the conductor-4 splitting law: the Gaussian Hadamard (1 + i)/2 is unitary and balanced over Q(i); denominator 2^ceil(k/2) and tally norm W(k) with no zeta_8 (k = 1..12)", ok7)


# ------------------------------------------------------------------------------------------------------------
# block T: the two probability strata (stratum.py, 22:C10, C11)
# The two-way part of ℤ[i] is the tally line. On Ω = 641 the engineered-core weights W± = 2 ± r (r² = 2) are exact
# residues. The element c = 1 + ζ_12 marks the hypothesis boundary, and r is a grid point g^n of the Subject chart. The
# framed readout uses the integer square root. Its instances are 23/54, the largest-remainder allocation
# 35 + 34 + 6 + 6 = 81, the grid nesting, the √3 instance and the canonical radicands. The conjugate-pair trace tally
# is computed in ℤ[√2]. The dial-ensemble Parseval tally (160) is computed in ℤ[x]/(x^40 + 1), the ring of the package.
@R.block("T", BLOCK["T"])
def block_T():
    """Block T — stratum.py (EXACT): T1–T11, the package's 12 checks."""
    # The counting Born rule on a fixed Gaussian-integer state over the Object cycle C_12 of F_157 (g_O = 22, the core
    # Q4, channels (r, a)): the channel weights w = N(Psi_{r,a}) are integers below the window Omega = 641, so each is
    # the unique lift of its shadow; the drive U psi(u) = psi(g^-1 u) presents the ensemble, and the coincidence counts
    # registered over its completed period of 12 chronons (on one fibre, and on all) give the registered frequencies,
    # framed rationals equal to the structural ratios sum_a w_{r,a} / W with W = 4 ||psi||^2 (Parseval): the two strata
    # coincide on the stationary core-valued sector, and the ratios sum to 1.
    pT, gT, Om = 157, 22, 157                                                  # the window is the carrier's count
    HT = sorted({pow(gT, k, pT) for k in range(12)})
    psiT = {u: ((i % 5) - 2, (i % 3) - 1) for i, u in enumerate(HT)}
    def ampT(state, r, a):
        s_ = (0, 0)
        for l in range(4): s_ = ga(s_, gm(gc(I4[(r * l) % 4]), state[pow(gT, a + 3 * l, pT)]))
        return s_
    ginv = pow(gT, 11, pT)
    driveT = lambda st: {u: st[(u * ginv) % pT] for u in HT}
    RAT = [(r, a) for r in range(4) for a in range(3)]
    wT = {x: gnorm(ampT(psiT, *x)) for x in RAT}; WT = sum(wT.values())
    lifts_ok = all(0 <= w_ < Om and (w_ % Om) == w_ for w_ in wT.values())                  # below the window: the least lift of the shadow is the weight itself
    st, cnt_all, cnt_one = psiT, {r: 0 for r in range(4)}, {r: 0 for r in range(4)}
    for _ in range(12):
        for r in range(4):
            cnt_one[r] += gnorm(ampT(st, r, 0))
            for a in range(3): cnt_all[r] += gnorm(ampT(st, r, a))
        st = driveT(st)
    freq_all = {r: Fr(cnt_all[r], sum(cnt_all.values())) for r in range(4)}
    freq_one = {r: Fr(cnt_one[r], sum(cnt_one.values())) for r in range(4)}
    struct = {r: Fr(sum(wT[(r, a)] for a in range(3)), WT) for r in range(4)}
    ok = st == psiT and WT == 4 * sum(gnorm(z) for z in psiT.values()) and lifts_ok and any(w_ > 0 for w_ in wT.values())
    ok &= freq_all == struct and freq_one == struct and sum(struct.values()) == 1 and all(f.denominator > 1 for f in struct.values())
    ok &= all(WT % f.denominator == 0 for f in struct.values())                              # framed rationals: denominators divide the tally W
    # 22:C10 (p22026)
    R.check("T1", "the counting Born rule on a fixed Z[i] state over C_12 of F_157: the channel weights N(Psi) are integers below the carrier's window 157, each the unique lift of its shadow; the coincidence counts over the drive's completed period (12 chronons, one fibre and all fibres) give registered frequencies equal to the structural ratios sum_a w / W, W = 4 ||psi||^2, framed rationals summing to 1 (the two strata coincide)",
            ok, f"W = {WT}, ratios {[str(struct[r]) for r in range(4)]}")
    R.check("T12", "the two-way (conjugation-invariant) part of Z[i] is the tally line b = 0 (exhaustive, |a|, |b| <= 6; the hypothesis boundary of the strata, an identity of Z[i])",
            all((b == 0) == ((a, b) == (a, -b)) for a in range(-6, 7) for b in range(-6, 7)))
    Om = 641
    r = next(x for x in range(1, Om) if x * x % Om == 2)
    Wp, Wm = (2 + r) % Om, (2 - r) % Om
    R.check("T2", "on Omega = 641: r^2 = 2 exists (641 = 1 mod 8); W+ + W- = 4 and W+ W- = 2 exactly", (Wp + Wm) % Om == 4 and Wp * Wm % Om == 2, f"r = {r}")
    Z = Cyclotomic(12)
    zin = Z.sub(Z.zeta(1), Z.zeta(3))                                         # ζ_12^{-1} = ζ − ζ³
    cc = Z.mul(Z.add(Z.one, Z.zeta(1)), Z.add(Z.one, zin))
    R.check("T3", "zeta_12^-1 = zeta - zeta^3 exactly; c = 1 + zeta_12 gives c cbar = 2 + (zeta + zeta^-1), off the tally line (the hypothesis boundary)",
            Z.mul(Z.zeta(1), zin) == Z.one and cc[0] == 2 and any(cc[1:]))
    g = 3
    dl = {pow(g, k, Om): k for k in range(Om - 1)}
    R.check("T4", "r is on the Subject zoom grid, r = g^n for the chart generator g = 3 (scale-periodic)", r in dl, f"r = 3^{dl[r]}")
    s_n = lambda m, n: isqrt(m * g ** (2 * n))
    num, den = 2 * g ** 4 + s_n(2, 4), 8 * g ** 4
    # 22:C11 (p22027), 22:X6 (p22049)
    R.check("T5", "the framed readout R_4((2 + sqrt 2)/8) = (2*81 + 114)/(8*81) = 23/54, the grid bound s^2 <= 2 g^8 < (s + 1)^2 exact",
            s_n(2, 4) == 114 and s_n(2, 4) ** 2 <= 2 * g ** 8 < (s_n(2, 4) + 1) ** 2 and Fr(num, den) == Fr(23, 54), f"{num}/{den}")
    B = 81
    probs = [Fr(23, 54), Fr(23, 54), Fr(2, 27), Fr(2, 27)]
    prov = [(B * q).numerator // (B * q).denominator for q in probs]
    rem = [B * q - v for q, v in zip(probs, prov)]
    counts = prov[:]
    for t in range(B - sum(prov)): counts[sorted(range(4), key=lambda i: (-rem[i], i))[t]] += 1
    R.check("T6", "the largest-remainder allocation at B = 81: provisional 34 + 34 + 6 + 6, final 35 + 34 + 6 + 6 = 81", sum(counts) == B and counts == [35, 34, 6, 6], f"{prov} -> {counts}")
    ok = all(s_n(2, n) ** 2 <= 2 * g ** (2 * n) < (s_n(2, n) + 1) ** 2 for n in range(1, 8))
    R.check("T7", "the grid bound at every scale n = 1..7, and the readouts nest: s_{n+1} - 3 s_n in {0, .., 3}", ok and all(0 <= s_n(2, n + 1) - g * s_n(2, n) <= g for n in range(1, 8)))
    R.check("T8", "the M3 readout: s_3(sqrt 3) = isqrt(3 * 3^6), grid bound exact", s_n(3, 3) ** 2 <= 3 * g ** 6 < (s_n(3, 3) + 1) ** 2, f"s_3 = {s_n(3, 3)}")
    def canon(u, v, m, b):
        f, d, mm = 1, 2, m
        while d * d <= mm:
            while mm % (d * d) == 0: mm //= d * d; f *= d
            d += 1
        gg = gcd(gcd(abs(u), abs(v * f)), b)
        return (u // gg, v * f // gg, mm, b // gg)
    R.check("T9", "canonical radicands: sqrt(8)/4 reduces to the canonical triple of sqrt(2)/2, (0, 1, 2, 2) (a representation-independent readout)",
            canon(0, 1, 8, 4) == (0, 1, 2, 2) and canon(0, 1, 2, 2) == (0, 1, 2, 2))
    mul2 = lambda x, y: (x[0] * y[0] + 2 * x[1] * y[1], x[0] * y[1] + x[1] * y[0])
    def pow2(x, n):
        out = (1, 0)
        for _ in range(n): out = mul2(out, x)
        return out
    t = {0: 2, 1: 4}
    for m in range(2, 14): t[m] = 4 * t[m - 1] - 2 * t[m - 2]
    ok = t[2] == 12 and t[3] == 40
    for Bn in range(1, 13):
        for k in range(Bn + 1):
            x, y = mul2(pow2((2, 1), k), pow2((2, -1), Bn - k)), mul2(pow2((2, -1), k), pow2((2, 1), Bn - k))
            ok &= (x[0] + y[0], x[1] + y[1]) == (2 ** min(k, Bn - k) * t[abs(Bn - 2 * k)], 0)
    def vec(e):                                                               # x^e in Z[x]/(x^40 + 1)
        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)]
    ok &= all(vadd(vec(40 - D), vec(D - 40)) == [-x for x in vadd(vec(D), vec(-D))] for D in range(80))
    R.check("T10", "the conjugate-pair trace tally: W+^k W-^(B-k) + W-^k W+^(B-k) = 2^min(k, B-k) t_|B-2k| in Z[sqrt 2], B <= 12; w(40 - D) = -w(D) in Z[x]/(x^40 + 1)", ok)
    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))
    R.check("T11", "the dial-ensemble Parseval tally over Z_80: sum w+ = sum w- = sum w+ w- = 160 exactly in Z[x]/(x^40 + 1)",
            sp == sm == spm == [160 * x for x in one])


# ------------------------------------------------------------------------------------------------------------
# block F: the coherent-fraction channel (gravfraction.py, 22:C21)
# The cells live on C_16, with the ledger ℤ[ζ_16] (ζ^8 = −1). The synchronised branch phase is ζ^{m_c a}, and the
# pairwise phase is ζ^{m_c1 m_c2 a}. The offset-spread systematic phase vanishes by complete character sums. The
# envelope |Σ|² is m² when synchronised and 0 for a complete spread. The reduced channel Γ = ζ^{m_c a} χ_inc factorises,
# and the mixed complementarity 4(V² + C²) = 2(1 + |Γ|²) holds. A complete-spread state is (1/4) times the partition
# matrix of the four branches. It is PPT, hence separable, unless the partition has a block of three. Then the least
# eigenvalue of its partial transpose is (1 − √3)/4 exactly. Locally additive spread phases never make a block of
# three. The signs of the eigenvalues are decided from the exact characteristic polynomial.
@R.block("F", BLOCK["F"])
def block_F():
    """Block F — gravfraction.py (EXACT): F1–F12, the package's 12 checks."""
    Z = Cyclotomic(16)
    zp = Z.zeta
    def power(a, k):                                                          # (ζ^a)^k by k multiplications
        out = Z.one
        for _ in range(k): out = Z.mul(out, zp(a))
        return out
    R.check("F1", "the synchronised branch phase is zeta^{m_c a} exactly (amplitudes multiply), m_c in {2, 3, 4}, every unit phase a",
            all(power(a, mc) == zp(mc * a) for a in range(1, 16) for mc in (2, 3, 4)))
    R.check("F2", "the offset-spread systematic branch phase vanishes: sum_s zeta^{a s} = 0 over the complete sector, every a != 0",
            all(Z.sum(zp(a * s) for s in range(16)) == Z.zero for a in range(1, 16)))
    R.check("F3", "the pairwise entangling phase is zeta^{m_c1 m_c2 a} exactly", all(power(a, m1 * m2) == zp(m1 * m2 * a) for a in range(1, 16) for m1 in (2, 3) for m2 in (2, 4)))
    sector = lambda offs, a: Z.sum(zp(a * s) for s in offs)
    R.check("F4", "the envelope: |sync sum|^2 = m^2 = 16 exactly; the complete C_4 spread sums to 0", Z.norm2(sector([0, 0, 0, 0], 1)) == Z.const(16) and sector([0, 4, 8, 12], 1) == Z.zero)
    avg = lambda offs, a, mc: Z.sum(Z.mul(zp(mc * a), zp(a * s)) for s in offs)
    R.check("F5", "the reduced channel factorises: the ensemble average is zeta^{m_c a} chi_inc (complete spread: both zero)", avg([0, 4, 8, 12], 3, 2) == Z.mul(zp(6), sector([0, 4, 8, 12], 3)))
    n2 = Z.norm2(sector([0, 0, 4, 8], 3))
    R.check("F6", "a nonuniform thermal chi_inc: the factorisation is exact and 0 < |chi|^2 < m^2", avg([0, 0, 4, 8], 3, 2) == Z.mul(zp(6), sector([0, 0, 4, 8], 3)) and any(n2) and n2 != Z.const(16))
    def comp(G):
        m1 = Z.mul(Z.sub(Z.one, G), Z.sub(Z.one, Z.conj(G))); m2 = Z.mul(Z.add(Z.one, G), Z.add(Z.one, Z.conj(G)))
        return Z.add(m1, m2) == Z.add(Z.const(2), Z.scale(2, Z.norm2(G)))
    R.check("F7", "the mixed complementarity 4(V^2 + C^2) = 2(1 + |Gamma|^2) as a ring identity (every pure phase and the mixed zeta + zeta^6)",
            all(comp(zp(e)) for e in range(16)) and comp(Z.add(zp(1), zp(6))))
    R.check("F8", "the pure-channel 4C^2 = (1 - zeta^e)(1 - zeta^-e) = 2 - (zeta^e + zeta^-e) exactly (the sin^2 chart reading)",
            Z.mul(Z.sub(Z.one, zp(3)), Z.sub(Z.one, zp(-3))) == Z.sub(Z.const(2), Z.add(zp(3), zp(-3))))
    R.check("F9", "the complete spread kills every cross-branch coherence (a complete character sum): rho diagonal, separable", all(Z.sum(zp(d * s) for s in range(16)) == Z.zero for d in range(1, 16)))
    q = Fr(1, 4)
    rho = [[q if a == b else q * Fr(1, 2) for b in range(4)] for a in range(4)]
    R.check("F10", "the symmetric damped state (systematic phase 0, Gamma = 1/2) is PPT, hence separable, exactly", nonneg_spectrum(partial_transpose(rho)))
    def canon(labels):
        seen = {}
        return tuple(seen.setdefault(x, len(seen)) for x in labels)
    part = lambda lab: [[q if lab[a] == lab[b] else 0 for b in range(4)] for a in range(4)]
    parts = sorted({canon(l) for l in product(range(4), repeat=4)})
    npt = [Fr(1), Fr(-1), Fr(3, 16), Fr(1, 32), Fr(-1, 128)]                  # (x − 1/4)²(x² − x/2 − 1/8): roots 1/4, 1/4, (1 ± √3)/4
    ok = len(parts) == 15
    for lab in parts:
        pt = partial_transpose(part(lab))
        ok &= charpoly(pt) == npt if 3 in [lab.count(v) for v in set(lab)] else nonneg_spectrum(pt)
    # 22:C21 (p22037)
    R.check("F11", "all 15 branch partitions at complete spread: NPT exactly at the blocks of three (spectrum of the partial transpose 1/4, 1/4, (1 +- sqrt 3)/4, least (1 - sqrt 3)/4), every other partition PPT", ok)
    achievable = {canon(((aL + bL) % n, (aL + bR) % n, (aR + bL) % n, (aR + bR) % n)) for n in range(2, 7) for aL, aR, bL, bR in product(range(n), repeat=4)}
    ok = all(3 not in [lab.count(v) for v in set(lab)] and nonneg_spectrum(partial_transpose(part(lab))) for lab in achievable)
    R.check("F12", "local additivity: the partitions of additive spread phases a_x + b_y (n <= 6) have no block of three and are PPT; theta = (0, 0, 0, 1) is not additively achievable",
            ok and canon((0, 0, 0, 1)) not in achievable, f"{len(achievable)} achievable partitions")


# ------------------------------------------------------------------------------------------------------------
# block L: uniqueness of the pair tally (gleason.py, 22:C12)
# The kernels live on the Q4 core with values in ℤ[i]. The kernels Σ_r c_r i^{rd} with nonnegative tallies c are two-way
# and tally-valued, and Fourier inversion recovers c (exhaustive, c ∈ 0..3). A negative coefficient is witnessed by its
# character state. A single-channel response holds iff c is a scaled unit vector, the channel fixing. The fibre norm and
# the w_r/16 multiplier are the counterexamples, and the linear kernels are excluded. The pure-winding fixing reads
# F(ψ_k) = 16 c_{k mod 4}. The core DFT has det −16i, so the responses fix the kernel.
@R.block("L", BLOCK["L"])
def block_L():
    """Block L — gleason.py (EXACT): L1–L9, the package's 9 checks."""
    ipow = lambda k: I4[k % 4]
    def kernel(c): return [tuple(sum(cr * ipow(r * d)[j] for r, cr in enumerate(c)) for j in range(2)) for d in range(4)]
    def F(K, psi):
        tot = (0, 0)
        for u in range(4):
            for v in range(4): tot = ga(tot, gm(gm(K[(v - u) % 4], psi[u]), gc(psi[v])))
        return tot
    chars = [[ipow(r * u) for u in range(4)] for r in range(4)]
    tests = [[(1, 0), (0, 0), (0, 0), (0, 0)], [(1, 0)] * 4, chars[1], [(1, 0), (1, 0), (0, 0), (0, 0)]]
    ok1 = ok2 = True
    for c in product(range(4), repeat=4):
        K = kernel(c)
        ok1 &= all(K[(-d) % 4] == gc(K[d]) for d in range(4)) and all(F(K, s)[1] == 0 and F(K, s)[0] >= 0 for s in tests)
        ok2 &= all(_gsum(gm(K[d], ipow(-r * d)) for d in range(4)) == (4 * c[r], 0) for r in range(4))
    # 22:C12 (p22028)
    R.check("L1", "the nonnegative-tally character combinations are two-way and tally-valued on the test states (exhaustive, c in 0..3)", ok1)
    R.check("L2", "Fourier inversion recovers every coefficient exactly", ok2)
    R.check("L3", "a negative coefficient c = (1, -1, 1, 0) is witnessed by its character state: F = -16 < 0", F(kernel((1, -1, 1, 0)), chars[1]) == (-16, 0))
    ok = True
    for c in product(range(4), repeat=4):
        resp = [F(kernel(c), chars[r])[0] for r in range(4)]
        ok &= (sum(1 for x in resp if x) == 1) == (sum(1 for x in c if x) == 1)
    R.check("L4", "a single-channel response holds iff the coefficient vector is a scaled unit vector (channel fixing, exhaustive)", ok)
    Kfn = [(1, 0), (0, 0), (0, 0), (0, 0)]
    resp = [F(Kfn, chars[r])[0] for r in range(4)]
    inv = [_gsum(gm(Kfn[d], ipow(-r * d)) for d in range(4)) for r in range(4)]
    R.check("L5", "the fibre norm K = [delta = 1]: responses (4, 4, 4, 4), 4 c_r = 1 each (c_r = 1/4, not a tally), so it fails channel selectivity",
            resp == [4, 4, 4, 4] and all(x == (1, 0) for x in inv))
    c_num, c_den = 1, 16
    R.check("L6", "the multiplier F = w_r/16: d^2 c = 16/16 = 1 is realised, c = 1/16 is not a tally (ray uniqueness only)", (16 * c_num) % c_den == 0 and c_den != 1)
    ok = all(_gsum(ipow(k * u) for u in range(4)) == (0, 0) for k in range(1, 4))
    ok &= all(not (gm((0, 1), (4 * c, 0))[1] == 0 and gm((0, 1), (4 * c, 0))[0] >= 0) for c in range(1, 5))
    R.check("L7", "the linear exclusion: a linear drive-invariant kernel vanishes on the nontrivial windings, and F(i psi_0) = 4ci leaves the tally cone unless c = 0", ok)
    R.check("L8", "pure-winding fixing: F(psi_k) = 16 c_{k mod 4} for every admissible kernel and winding, every channel index reached (exhaustive)",
            all(F(kernel(c), chars[k]) == (16 * c[k], 0) for c in product(range(4), repeat=4) for k in range(4)))
    det = (Fr(0), Fr(0))
    for perm in permutations(range(4)):
        sgn = (-1) ** sum(1 for a in range(4) for b in range(a + 1, 4) if perm[a] > perm[b])
        term = (Fr(sgn), Fr(0))
        for r in range(4): term = gm(term, chars[r][perm[r]])
        det = ga(det, term)
    def responses(K):
        out = [F(K, chars[k]) for k in range(4)]
        for k in range(4):
            for kp in range(k + 1, 4):
                out.append(F(K, [ga(chars[k][u], chars[kp][u]) for u in range(4)]))
                out.append(F(K, [ga(chars[k][u], gm((0, 1), chars[kp][u])) for u in range(4)]))
        return tuple(out)
    seen, ok = {}, det == (0, -16)
    for c in product(range(3), repeat=4):
        K = tuple(kernel(c)); key = responses(K)
        ok &= seen.setdefault(key, K) == K
    R.check("L9", "spanning and polarisation: the core DFT has det -16i (invertible over Q(i)); equal responses on the admissible class force equal kernels (exhaustive)", ok)


def _gsum(zs):
    out = (0, 0)
    for z in zs: out = ga(out, z)
    return out


# ------------------------------------------------------------------------------------------------------------
# block O: the Ω ledger (omega.py, 22:A5, Z2)
# The anchor is the master's A7, the certified bracket of the scale import (frc/chart.py, omega_bracket: Ω = 4S + 1
# from the fitted Λ and the Planck length), Ω ∼ 1.3 × 10^123 as an order of magnitude, with √Ω ∼ 3.6 × 10^61 and
# Ω^(1/4) ∼ 6.0 × 10^30. The null channels put floors on Ω: the Riemann height (3·10^12)^4, the Sorkin and Born tallies
# 10^22, and the granularity 2^60. Every floor lies below the anchor, and its margin in orders of ten is recorded; the
# binding floor is the Riemann height, seventy-three orders below. The scales are the integer roots of one Ω. Every
# comparison is of integers, and no number above Ω is formed.
@R.block("O", BLOCK["O"])
def block_O():
    """Block O — omega.py (EXACT): O1–O4, the package's 4 checks, on the master's anchor."""
    lo, hi = CH.omega_bracket()
    L, H = int(lo), int(hi) + 1                                               # the bracket's ends, as integers
    floors = [("Riemann zero verification (rh paper)", (3 * 10 ** 12) ** 4), ("Sorkin third-order nullity (exp I)", 10 ** 22),
              ("Born readout window (companion Thm)", 10 ** 22), ("Granularity ceiling (exp V)", 2 ** 60)]
    def orders(x):                                                            # the margin floor(log10(Omega/x)) at the lower end
        q = Fr(L, x); k = 0
        while 10 ** (k + 1) <= q: k += 1
        return k
    # 22:A5 (p22005)
    R.check("O1", "every floor lies below the anchor Omega ~ 1.3 x 10^123 (the certified bracket's lower end), with its margin in orders of ten", all(f < L for _, f in floors),
            "margins " + ", ".join(str(orders(f)) for _, f in floors))
    omega_min = max(f for _, f in floors)
    R.check("O2", "the binding floor Omega > 8.1 x 10^49 lies seventy-three orders below the anchor", omega_min < L and omega_min == 81 * 10 ** 48 and orders(omega_min) == 73,
            f"margin {orders(omega_min)} orders")
    rt, qt = isqrt(L), isqrt(isqrt(L))
    R.check("O3", "the scales are the integer roots of one Omega: sqrt(Omega) ~ 3.6 x 10^61 and Omega^(1/4) ~ 6.0 x 10^30 (36 x 10^60 < sqrt < 37 x 10^60, 6 x 10^30 < quarter root < 7 x 10^30), the Riemann height 3 x 10^12 below the quarter root",
            rt * rt <= L < (rt + 1) ** 2 and qt ** 4 <= L < (qt + 1) ** 4 and 36 * 10 ** 60 < rt < 37 * 10 ** 60 and 6 * 10 ** 30 < qt < 7 * 10 ** 30 and 3 * 10 ** 12 < qt
            and L // 10 ** 122 == 13 and H // 10 ** 122 == 13)
    binding = max((f, n) for n, f in floors)
    # 22:Z2 (p22061)
    R.check("O4", "the binding floor is the Riemann height, (3 x 10^12)^4 = 8.1 x 10^49, the largest of the floors, 73 orders below the anchor's lower end and below the quarter root's fourth power (the carrier scale fixed through Omega^(1/4)): the channel next-generation experiments push first",
            binding[1].startswith("Riemann") and binding[0] == (3 * 10 ** 12) ** 4 == 81 * 10 ** 48 and binding[0] < L and orders(binding[0]) == 73
            and 3 * 10 ** 12 < qt and binding[0] < qt ** 4 and all(f <= binding[0] for _, f in floors), binding[1])


# ------------------------------------------------------------------------------------------------------------
# block I: inter-Subject consistency (intersubject.py, 22:C23, X4)
# Two Subjects S, S' read one Object O in F_421, over the ledger ℤ[ζ_{n_O}]. In configuration A, O_29 is read by S_61 and
# S_13 (equal cores Q4). In configuration B, O_61 is read by S_29 and S_13 (embedded cores Q4 < C_12). The control R is
# C_24 with the incomparable cores C_12 and C_8. The joint refinement of the two fibre partitions is the partition by
# the common core, in either order. By the selection rule both Subjects induce the same core character η_{s mod 4}. A
# two-step registration is realisable exactly when its first step is selection-allowed, the fibres meet and the channels
# agree on Q4. It then reads the core character on the shared cell, in either order. A Gaussian-integer superposition
# input agrees on the shared cell, and channels that disagree on Q4 are null in both orders.
@R.block("I", BLOCK["I"])
def block_I():
    """Block I — intersubject.py (EXACT): I1–I7, the package's 22 checks."""
    p, g = 421, 2
    # A ledger value is kept in the group ring of C_n, as a dict {e: c} for Σ c ζ^e, so that a phase multiplies by a
    # shift. It is compared and tested for zero in ℤ[ζ_n] itself, by its canonical form (frc.quantum.Cyclotomic).
    rings = {}
    def ring(n):
        if n not in rings: rings[n] = Cyclotomic(n)
        return rings[n]
    def gadd(terms, n):
        out = {}
        for t in terms:
            for e, c in t.items(): out[e] = out.get(e, 0) + c
        return {e: c for e, c in out.items() if c}
    def rot(v, e, n): return {(k + e) % n: c for k, c in v.items()}
    def gmul(a, b, n): return gadd([{(i + j) % n: x * y} for i, x in a.items() for j, y in b.items()], n)
    canon = lambda v, n: ring(n).from_exponents(v)
    iszero = lambda v, n: canon(v, n) == ring(n).zero
    fibre = lambda nO, d, a: frozenset((a + (nO // d) * l) % nO for l in range(d))
    def eta(nO, d, r, l): return {(nO // d) * r * l % nO: 1}
    def amplitude(state, nO, d, r, a):
        st = nO // d
        return gadd([rot(state[(a + st * l) % nO], -st * r * l, nO) for l in range(d) if (a + st * l) % nO in state], nO)
    def luders(state, nO, d, r, a):
        psi = amplitude(state, nO, d, r, a)
        if iszero(psi, nO): return {}
        return {(a + (nO // d) * l) % nO: rot(psi, (nO // d) * r * l, nO) for l in range(d)}
    winding = lambda nO, s: {j: {s * j % nO: 1} for j in range(nO)}
    restrict = lambda state, cell: {j: state[j] for j in cell if j in state}
    def proportional(X, Y, nO):
        if set(X) != set(Y) or not X: return set(X) == set(Y)
        return all(canon(gmul(X[i], Y[j], nO), nO) == canon(gmul(X[j], Y[i], nO), nO) for i in X for j in X)
    def k_cosets(nO, e): return {frozenset((a + (nO // e) * l) % nO for l in range(e)) for a in range(nO)}
    def transported(nO, e, idx, coset):
        rep = min(coset)
        return {j: {(nO // e) * idx * (((j - rep) // (nO // e)) % e) % nO: 1} for j in coset}
    ok = iszero(gadd([{7 * l: 1} for l in range(4)], 28), 28) and p % 4 == 1 and arith.order(g, p) == p - 1
    A = dict(nO=28, nS=60, nSp=12, tag="A: O_29 read by S_61, S_13")
    B = dict(nO=60, nS=28, nSp=12, tag="B: O_61 read by S_29, S_13")
    for cfg in (A, B):
        nO = cfg["nO"]
        cfg.update(d=gcd(cfg["nS"], nO), dp=gcd(cfg["nSp"], nO), e=gcd(gcd(cfg["nS"], cfg["nSp"]), nO))
        ok &= cfg["e"] == gcd(cfg["d"], cfg["dp"]) and cfg["e"] % 4 == 0 and cfg["e"] == 4
    R.check("I1", "the ledger Z[zeta_28] is exact (1 + i + i^2 + i^3 = 0); F_421 admissible; the cores: A d = d' = 4, B d = 4 < d' = 12, the common core e = 4 = |Q4| in both", ok)

    def refinement(nO, d, dp, e):
        Kc = k_cosets(nO, e); cells = [f & fp for f in (fibre(nO, d, a) for a in range(nO // d)) for fp in (fibre(nO, dp, a) for a in range(nO // dp)) if f & fp]
        return all(c in Kc for c in cells), len(cells)
    ok = True
    for cfg in (A, B):
        good, n = refinement(cfg["nO"], cfg["d"], cfg["dp"], cfg["e"]); ok &= good and n == cfg["nO"] // cfg["e"]
    R.check("I2", "(I) each joint cell F cap F' is one coset of the common core, the same in either order; the joint refinement is the partition by Q4 (A: 7 cells, B: 15)", ok)
    good, n = refinement(24, 12, 8, 4)
    R.check("I3", "(I) the control C_24 with the incomparable cores C_12 and C_8: the joint cells are C_4-cosets, 24/4 = 6 cells", good and n == 6)

    ok_sel = ok_chr = True
    for cfg in (A, B):
        nO, d, dp, e = cfg["nO"], cfg["d"], cfg["dp"], cfg["e"]
        for s in range(nO):
            st = winding(nO, s)
            live = {r for r in range(d) if any(not iszero(amplitude(st, nO, d, r, a), nO) for a in range(nO // d))}
            livep = {r for r in range(dp) if any(not iszero(amplitude(st, nO, dp, r, a), nO) for a in range(nO // dp))}
            ok_sel &= live == {s % d} and livep == {s % dp} and (s % d) % e == s % e and (s % dp) % e == s % e
            ch, chp, chs = ([canon(eta(nO, e, x, l), nO) for l in range(e)] for x in ((s % d) % e, (s % dp) % e, s % e))
            ok_chr &= ch == chp == chs
    # 22:C23 (p22039)
    R.check("I4", "(II) for every winding the selection rule leaves S the channel s mod d and S' the channel s mod d', both s mod 4: the two Subjects induce the identical core character eta_(s mod 4) on Q4 (A and B)",
            ok_sel and ok_chr)

    def seq(state, first, second, nO, cache):
        if first not in cache: cache[first] = luders(state, nO, *first)
        s1 = cache[first]
        return luders(s1, nO, *second) if s1 else {}
    ok_pred = ok_value = ok_both = True; det = []
    for cfg in (A, B):
        nO, d, dp, e = cfg["nO"], cfg["d"], cfg["dp"], cfg["e"]
        Kset = k_cosets(nO, e); n_fwd = n_both = 0
        for s in range(lcm(d, dp)):
            st, cache = winding(nO, s), {}
            for r, a, rp, ap in product(range(d), range(nO // d), range(dp), range(nO // dp)):
                C = fibre(nO, d, a) & fibre(nO, dp, ap)
                agree = r % e == rp % e
                fwd, rev = seq(st, (d, r, a), (dp, rp, ap), nO, cache), seq(st, (dp, rp, ap), (d, r, a), nO, cache)
                ok_pred &= bool(fwd) == (bool(C) and r % d == s % d and agree) and bool(rev) == (bool(C) and rp % dp == s % dp and agree)
                ref = transported(nO, e, s % e, C) if C else None
                for out in (fwd, rev):
                    if out: ok_value &= C in Kset and proportional(restrict(out, C), ref, nO)
                n_fwd += bool(fwd)
                if fwd and rev:
                    n_both += 1; ok_both &= proportional(restrict(fwd, C), restrict(rev, C), nO)
        det.append(f"{cfg['tag'][:1]}: {n_fwd} forward, {n_both} both-order")
    # 22:X4 (p22047)
    R.check("I5", "(III) the realisability predicate is exact in both orders (first step selection-allowed, fibres meet, r = r' mod 4); every realisable sequence reads eta_(s mod 4) on its Q4-coset; both orders agree on the shared cell",
            ok_pred and ok_value and ok_both, "; ".join(det))

    nO, d, dp = A["nO"], A["d"], A["dp"]
    st = {}
    for j in range(nO):
        acc = gadd([{s * j % nO: 1 + s, (nO // 4 + s * j) % nO: 1 + s % 5} for s in range(nO)], nO)   # Σ_s c_s ζ^{sj}
        if not iszero(acc, nO): st[j] = acc
    ok, both, cache = True, 0, {}
    for r, a, rp, ap in product(range(d), range(nO // d), range(dp), range(nO // dp)):
        C = fibre(nO, d, a) & fibre(nO, dp, ap)
        fwd, rev = seq(st, (d, r, a), (dp, rp, ap), nO, cache), seq(st, (dp, rp, ap), (d, r, a), nO, cache)
        if fwd and rev:
            both += 1; ok &= proportional(restrict(fwd, C), restrict(rev, C), nO)
    R.check("I6", "(III') a Gaussian-integer superposition input (A): every both-order sequence agrees on the shared cell", ok, f"{both} both-order sequences")
    st, bad, cache = winding(nO, 1), [], {}
    for r, a, rp, ap in product(range(d), range(nO // d), range(dp), range(nO // dp)):
        if r % 4 != rp % 4:
            bad.append(bool(seq(st, (d, r, a), (dp, rp, ap), nO, cache)) or bool(seq(st, (dp, rp, ap), (d, r, a), nO, cache)))
    R.check("I7", "channels that disagree on Q4 (r != r' mod 4) are null in both orders: an inconsistency would show as nullity, never as a contradiction", len(bad) > 0 and not any(bad))


# ------------------------------------------------------------------------------------------------------------
# block K: quarter-turn transport (transport.py, 22:C27)
# Let C_n be an embedded cycle of F_P^×, with n = 4κ_n dividing P − 1 = 4κ. The winding reduction g^a ↦ g_n^{a mod n}
# carries the ambient quarter-turn i = g^{−κ} onto i_n = g_n^{−κ_n} iff κ ≡ κ_n (mod n). It carries i onto −i_n iff
# κ ≡ −κ_n, and it keeps the half-turn iff κ ≡ ±κ_n (mod n/2). The criterion is checked against the computed elements
# on six instances.
@R.block("K", BLOCK["K"])
def block_K():
    """Block K — transport.py (EXACT): K1, the package's 6 checks K1–K6."""
    def transport(P, g, n):
        N = P - 1; kap, kn = N // 4, n // 4
        assert P % 4 == 1 and N % n == 0 and n % 4 == 0 and arith.order(g, P) == N
        gS = pow(g, N // n, P)
        i_n, Pi_i = pow(gS, n - kn, P), pow(gS, (N - kap) % n, P)
        faithful, conjugate, half = kap % n == kn % n, kap % n == (n - kn) % n, kap % (n // 2) == kn % (n // 2)
        ok = (Pi_i == i_n) == faithful and (Pi_i == P - i_n) == conjugate and (Pi_i * Pi_i % P == P - 1) == half
        return ok, faithful, conjugate, half, Pi_i
    cases = [(157, 5, 12, "faithful"), (421, 2, 12, "conjugate"), (421, 2, 60, "conjugate"), (421, 2, 28, "conjugate"),
             (421, 2, 4, "faithful"), (641, 3, 40, "broken"), (157, 5, 52, "conjugate")]
    ok = True; det = []
    for P, g, n, kind in cases:
        good, f, c, h, Pi_i = transport(P, g, n)
        ok &= good and {"faithful": f and not c, "conjugate": (not f) and c and h, "broken": not (f or c or h) and Pi_i == 1}[kind]
        det.append(f"F_{P} -> C_{n}: {kind}")
    # 22:C27 (p22043)
    R.check("K1", "the quarter-turn transport trichotomy against the computed elements: faithful iff kappa = kappa_n (mod n), conjugate iff kappa = -kappa_n, the half-turn iff kappa = +-kappa_n (mod n/2)",
            ok, "; ".join(det))


if __name__ == "__main__":
    want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)
    bad = [b for b in want if b not in BLOCK]
    if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")
    for b in want: R.run_block(b)
    sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCK) else None) else 1)