"""master/quantum — a ledger file of the master's blocks F and P, quantum: the rows the quantum theme proves (ledger migration,
task LM28, 6 October 2026).

The master's block F is bound by this file (the quantum theme). It binds F2, multi-body registration, and F5, the graded registration law (task LM42, 7 October 2026; its source 39-s173 is
unpublished, named and not linked, Q04), since 17 October 2026 F4, the Q₄ quotient of the Object cycle, and F6, the
binding lift (00-ledger-20260816/reports/block-f-f4-f6-glyphs-20261017.md, decisions D1–D5), and since 19 October 2026
the prediction P2, the coherent-fraction channel (block P, 22:C21's theorems): the table of keys (generated from
docs/00-ledger.json and docs/predictions.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the
cycles, and the checks, which call the quantum theme (frc/quantum.py). The Lean side is lean/FrcCore/Theme/Quantum.lean
and Theme/Composite.lean, the key file lean/FrcCore/Keys/Quantum.lean and the certificate lean/FrcCore/Ledgers/Master/Quantum.lean.

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

Blocks:  B  the binding lift: fusion iff coprime, the deuteron and hydrogen, dephasing   EXACT  (00:F6)
         C  the coherent-fraction channel: phases, spread, factorisation, separability EXACT  (00:P2)
         J  the unequal-cycle composite: joint recurrence, gcd offset, dephasing     EXACT  (00:F2)
         Q  the Q₄ quotient of the Object cycle: the division fold, channels, fibres  EXACT  (00:F4)
         R  the graded registration law: depth, home, sign, visibility              EXACT  (00:F5)

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

from frc import arith
from frc.registry import Registry
from frc.quantum import (joint_period, orbits, offset, reach, root_of_unity, character_sums, components, depth, home,
                         cycle, division_fold, core_cosets, fusion, Cyclotomic, charpoly, nonneg_spectrum, partial_transpose)
from frc.subject import frame, fold_solutions

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "FP"
KEYS = {"F1": "p00059", "F2": "p00191", "F4": "p00062", "F5": "p00194", "F6": "p00064", "P1": "p00133", "P2": "p00061", "P3": "p00180", "P4": "p00091"}       # every row of the blocks: its label and its accession key
LEAN = {"F2": "core", "F4": "core", "F5": "core", "F6": "core", "P2": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them
# ---- end of the generated table ----

# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys
# FRC.Ledger.p<key> from them). The master's block file is the binding's source, as a paper's \lean{} cells are its own.
PROOFS = {
    "F2": ["FRC.Quantum.joint_recurrence", "FRC.Quantum.joint_least", "FRC.Quantum.pair_offset",
           "FRC.Quantum.dephasing"],
    "F4": ["FRC.Observation.quotient_fold", "FRC.Observation.fold_core", "FRC.Subject.spinor",
           "FRC.Observation.shared_core", "FRC.Observation.orthogonality", "FRC.Observation.selection",
           "FRC.Observation.lueders", "FRC.Observation.parseval", "FRC.Observation.classicality_index"],
    "F5": ["FRC.Quantum.absorbed", "FRC.Quantum.unique_home", "FRC.Quantum.two_part_homes", "FRC.Quantum.sign_both",
           "FRC.Quantum.visibility_cap", "FRC.Quantum.registration_instances"],
    "F6": ["FRC.Quantum.fusion_iff", "FRC.Composite.winding_period", "FRC.Composite.winding_confined",
           "FRC.Quantum.pair_offset", "FRC.Composite.cluster_offset", "FRC.Composite.fused_rung",
           "FRC.Observation.selection", "FRC.Observation.orthogonality", "FRC.Quantum.dephasing",
           "FRC.Subject.spinor", "FRC.Quantum.binding_instances", "FRC.Quantum.binding_census"],
    "P2": ["FRC.Composite.branch_phase", "FRC.Composite.pair_product", "FRC.Composite.spread_cancels",
           "FRC.Composite.channel_assembly"],                                   # 19 October 2026: 22:C21's theorems, the coherent-fraction channel
}

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

PAIRS = 30                      # every pair of periods a, b ≤ PAIRS
TRIPLES = 10                    # every triple of periods ≤ TRIPLES

SUBJECTS = 6000                 # the Subjects p ≡ 1 (mod 4) with κ odd below it, every Object q ≡ 1 (mod 4) with q² < p

FRAMES = 400                    # every frame p = 4κ + 1 below it, with its drive (the division fold, 00:F4)
CYCLES = 20                     # every pair of cycles a, b ≤ CYCLES (the binding lift, 00:F6)

LEDGER = {"J1": "00:F2", "J2": "00:F2", "J3": "00:F2", "R1": "00:F5", "R2": "00:F5", "R3": "00:F5",
          "Q1": "00:F4", "Q2": "00:F4", "Q3": "00:F4", "B1": "00:F6", "B2": "00:F6", "B3": "00:F6", "C1": "00:P2", "C2": "00:P2"}
BLOCKS = {"J": "the unequal-cycle composite: joint recurrence, gcd offset, dephasing",
          "R": "the graded registration law: depth, home, sign, visibility",
          "Q": "the Q₄ quotient of the Object cycle: the division fold, the pointer channels, the fibres",
          "B": "the binding lift: fusion iff coprime, the deuteron and hydrogen, exact dephasing",
          "C": "the coherent-fraction channel: the branch and pair phases, the spread, the factorisation, separability"}
PREDICATES = {"00:F2": "J1", "00:F5": "R1", "00:F4": "Q1", "00:F6": "B1", "00:P2": "C1"}

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


def _prime_1_mod(N):
    q = N + 1
    while not arith.is_prime(q): q += N
    return q


# ------------------------------------------------------------------------------------------------------------
# block J: the unequal-cycle composite (00:F2)
# the joint recurrence is the lcm of the periods; two joint states share an orbit exactly when their offsets agree
# modulo g, g T = a b; every character the drive moves sums to zero over every joint recurrence (Quantum.lean:
# joint_recurrence, joint_least, pair_offset, dephasing).
@R.block("J", BLOCKS["J"])
def block_J():
    """Block J — the unequal-cycle composite (EXACT): J1–J3."""
    # 00:F2 (p00191)
    bad = []
    for a in range(1, PAIRS + 1):
        for b in range(1, PAIRS + 1):
            T = joint_period([a, b])
            g = a * b // T
            orbs = orbits(a, b)
            ok = T == lcm(a, b) and g == gcd(a, b) and g * T == a * b
            ok &= all((t % a == 0 and t % b == 0) == (t % T == 0) for t in range(3 * a * b))
            ok &= len(orbs) == g and all(len(o) == T for o in orbs)
            ok &= all(len({offset(x, y, g) for x, y in o}) == 1 for o in orbs)
            ok &= len({offset(o[0][0], o[0][1], g) for o in orbs}) == g
            if not ok: bad.append((a, b))
    bad3 = [(a, b, c) for a in range(1, TRIPLES + 1) for b in range(1, TRIPLES + 1) for c in range(1, TRIPLES + 1)
            if joint_period([a, b, c]) != lcm(a, b, c)]
    R.check("J1", f"every pair of periods a, b ≤ {PAIRS}: the joint recurrences are exactly the multiples of T = lcm(a, b); "
            "the joint drive has g = gcd(a, b) orbits of T states, g T = a b, each orbit one offset class (x − y) mod g, "
            f"the g classes all occupied; every triple ≤ {TRIPLES}: the joint period is lcm(a, b, c)", not bad and not bad3,
            f"{PAIRS * PAIRS} pairs, {TRIPLES ** 3} triples; exceptions {bad[:3]} {bad3[:3]}")
    # J2 a second method: reachability by search against the offset criterion, random pairs up to 200
    rng = random.Random(28)
    bad = []
    for _ in range(300):
        a, b = rng.randrange(1, 200), rng.randrange(1, 200)
        g = gcd(a, b)
        x, y, x2, y2 = rng.randrange(a), rng.randrange(b), rng.randrange(a), rng.randrange(b)
        if (reach(x, y, x2, y2, a, b) is not None) != ((x + y2) % g == (x2 + y) % g): bad.append((a, b))
    R.check("J2", "300 random pairs of periods below 200 and random states: a chronon carries (x, y) to (x', y') exactly when "
            "(x + y') ≡ (x' + y) mod g, by search", not bad, f"exceptions {bad[:3]}")
    # J3 dephasing: every character of ℤ/a × ℤ/b in 𝔽_q, q ≡ 1 (mod lcm(a, b))
    tot, moved, bad = 0, 0, []
    for a, b in [(4, 6), (12, 232), (5, 7), (8, 12), (10, 14)]:
        T = lcm(a, b); q = _prime_1_mod(T)
        for M in (T, a * b):
            sums = character_sums(q, a, b, M)
            tot += len(sums)
            moved += sum(1 for m, _ in sums if m)
            if not all((s == 0) if m else (s == M % q) for m, s in sums): bad.append((a, b, M))
    R.check("J3", "the cycles (4, 6), (12, 232), (5, 7), (8, 12), (10, 14) in 𝔽_q with q ≡ 1 mod lcm: every character the drive "
            "moves sums to zero along it over one joint period T and over the product period a b; the others give T or a b",
            not bad, f"{moved} of {tot} character sums cancel; exceptions {bad}")




# ------------------------------------------------------------------------------------------------------------
# block R: the graded registration law (00:F5; 39-s173, rows B1–B5)
# an Object component ℓᵃ registers at depth d = ord_{ℓᵃ}(p): d = 1 absorbed in C_{p−1}, its image unique; d = 2 for odd
# ℓ on the boost torus C_{p+1}, the home unique (gcd(p − 1, p + 1) = 2); a 2-component past the quarter off both tori;
# the sign on both faces; the cap 2 where p² < Ω < p³ (Quantum.lean: absorbed, unique_home, two_part_homes, sign_both,
# visibility_cap, registration_instances).
@R.block("R", BLOCKS["R"])
def block_R():
    """Block R — the graded registration law (EXACT): R1–R3."""
    # 00:F5 (p00194)
    bad, n_towers, n_comp, seen = [], 0, 0, {"absorbed": 0, "torus": 0, "quadratic": 0, "beyond": 0}
    for p in range(13, SUBJECTS, 4):
        if not arith.is_prime(p) or ((p - 1) // 4) % 2 == 0: continue
        for q in range(5, p, 4):
            if q * q >= p: break
            if not arith.is_prime(q): continue
            n_towers += 1
            for face in (q - 1, q + 1):
                for l, a, n in components(face):
                    n_comp += 1
                    d, h = depth(n, p), home(n, p)
                    seen[h] += 1
                    ok = (d == 1) == (h == "absorbed")                                   # d = 1 iff absorbed
                    if l > 2: ok &= (d == 2) == (h == "torus")                          # odd ℓ: d = 2 iff on the boost torus
                    else: ok &= (n <= 4) == (h == "absorbed") and h != "torus" if n > 2 else h == "absorbed"
                    ok &= (h != "quadratic" or d == 2) and (h != "beyond" or d > 2)
                    if not ok: bad.append((q, p, n, d, h))
            ok = pow(p - 1, p - 1, p) == 1 and pow(p - 1, p + 1, p) == 1 and gcd(p - 1, p + 1) == 2
            if not ok: bad.append((q, p, "sign"))
    R.check("R1", f"every Subject p ≡ 1 (mod 4) with κ odd below {SUBJECTS}, every Object q ≡ 1 (mod 4) prime with q² < p, every "
            "primary component ℓᵃ of q − 1 and q + 1: depth 1 iff absorbed in C_{p−1}; for odd ℓ depth 2 iff on the boost torus "
            "C_{p+1}, gcd(p − 1, p + 1) = 2; the 2-components 2 and 4 absorbed, 8 and beyond on neither torus; the sign on both "
            "faces", not bad, f"{n_towers} towers, {n_comp} components {seen}; exceptions {bad[:3]}")
    # R2 the instances (39:B2, B3, B5): decided directly
    roots4 = sorted(x for x in range(1, 173) if pow(x, 4, 173) == 1)
    ok = (depth(7, 173), depth(7, 181), depth(7, 197)) == (6, 2, 1) and roots4 == [1, 80, 93, 172]
    ok &= home(4, 173) == "absorbed" and home(3, 173) == "torus" and home(7, 173) == "beyond"           # hydrogen, q = 13
    ok &= all(depth(n, 173) <= 2 for f in (4, 6) for _, _, n in components(f))                           # the proton, q = 5
    ok &= 5 * 5 > 13                                                                                      # (5, 13) refused
    R.check("R2", "the instances: the depth of hydrogen's interior 7 is 6 at 173, 2 at 181, 1 at 197; the quarter absorbed at 173 "
            "with the images {1, 80, 93, 172}, the triality on the torus, the 7 beyond; the proton whole (depth ≤ 2); (5, 13) "
            "refused, 25 > 13", ok, f"4th roots of unity in 𝔽_173: {roots4}")
    # R3 the cap: p² < Ω < p³ on the minimal tower and the laboratory tower; every saturating tower p² < Ω ≤ (p + 1)²
    ok = 173 ** 2 < 30089 <= 174 ** 2 and 30089 < 173 ** 3 and 1373 ** 2 < 2408561 < 1373 ** 3
    ok &= all((p + 1) ** 2 < p ** 3 for p in range(3, 2000))
    R.check("R3", "the visibility cap 2: (173, 30 089) saturating, 173² < Ω ≤ 174² < 173³; the laboratory (1 373, 2 408 561) "
            "with p² < Ω < p³; (p + 1)² < p³ for every 3 ≤ p < 2000", ok, "")

# ------------------------------------------------------------------------------------------------------------
# block Q: the Q₄ quotient of the Object cycle (00:F4)
# the division fold x = iʳ gˢ (i = g^{3κ} = −g^κ, the class r < 4, the rung s < κ) is a bijection of [0, 4) × [0, κ) onto
# every cycle of order 4κ, on every capacity; the product fold iʳ (g⁴)ˢ is one iff κ is odd (C16); the fibres are the κ
# cosets gˢ·Q₄ (i² = −1, i of order 4: fold_core); the pointer channels are the four characters of Q₄, orthogonal; the
# amplitude is the coherent fibre sum, with the selection rule, Parseval and the resolution of identity; the outcomes are
# the cosets, κ of them, one iff the cycle is the core (Observation.lean: quotient_fold, fold_core, orthogonality,
# selection, lueders, parseval, shared_core, classicality_index; Subject.lean: spinor).
@R.block("Q", BLOCKS["Q"])
def block_Q():
    """Block Q — the Q₄ quotient of the Object cycle (EXACT): Q1–Q3."""
    # the cycles: every frame below FRAMES with its drive, and three Object cycles inside Subjects (22-quantum's carriers)
    cases = []
    for p in range(5, FRAMES, 4):
        if arith.is_prime(p): cases.append((p, frame(p)[1], p - 1))
    cases += [(157, pow(5, 156 // 12, 157), 12), (421, pow(2, 420 // 28, 421), 28), (641, 601, 16)]
    # 00:F4 (p00062)
    bad, n_odd = [], 0
    for q, g, n in cases:
        cyc, k = cycle(q, g), n // 4
        if len(cyc) != n: bad.append((q, g, "order")); continue
        fold = division_fold(q, g)
        ok = len(fold) == n and sorted(fold.values()) == sorted(cyc)                       # a bijection onto the cycle
        ok &= all(fold[(r, s)] == cyc[(3 * k * r + s) % n] for r, s in fold)              # the exponent 3κr + s
        ok &= all(fold[(r, s)] == pow(g, 3 * k, q) * fold[(r - 1, s)] % q for r in range(1, 4) for s in range(k))
        ok &= pow(g, 3 * k, q) == (-pow(g, k, q)) % q and pow(g, 6 * k, q) == q - 1        # i = −g^κ, i² = −1
        i, g4 = pow(g, 3 * k, q), pow(g, 4, q)
        prod = [pow(i, r, q) * pow(g4, s, q) % q for r in range(4) for s in range(k)]      # the product fold (C16)
        ok &= (len(set(prod)) == n) == (k % 2 == 1) == bool(fold_solutions(k))
        n_odd += k % 2
        if not ok: bad.append((q, g, n))
    R.check("Q1", f"every frame p = 4κ + 1 below {FRAMES} with its drive, and the Object cycles C_12 in 𝔽_157, C_28 in 𝔽_421, "
            "C_16 in 𝔽_641: the division fold (r, s) ↦ iʳ gˢ, i = g^{3κ} = −g^κ, r < 4, s < κ, is a bijection onto the cycle, "
            "the exponent 3κr + s; the product fold iʳ (g⁴)ˢ is one exactly when κ is odd, exactly when 3κr + 4s ≡ 1 (mod 4κ) "
            "is solvable", not bad and len(cases) == 40 and n_odd == 24, f"{len(cases)} cycles, {n_odd} with κ odd; exceptions {bad[:3]}")
    # Q2 the pointer channels and the amplitude, over ℤ[ζ_n] and in the shell: the cycles C_12 ⊂ 𝔽_13 and C_28 ⊂ 𝔽_421
    bad, n_amp = [], 0
    for q, g, n in [(13, 2, 12), (421, pow(2, 420 // 28, 421), 28)]:
        k = n // 4; Z = Cyclotomic(n); I = Z.zeta(3 * k)                                   # i = ζ^{3κ} in ℤ[ζ_n], i² = −1
        ok = Z.mul(I, I) == Z.neg(Z.one)
        eta = lambda r, l: Z.zeta(3 * k * r * l)                                           # η_r(iˡ) = i^{rl}
        ok &= all(Z.sum(Z.mul(eta(r, l), Z.conj(eta(r2, l))) for l in range(4)) == (Z.const(4) if r == r2 else Z.zero)
                  for r in range(4) for r2 in range(4))                                    # orthogonality of the four channels
        cyc = cycle(q, g)
        psi = {x: (e * e + 3 * e) % 11 - 5 for e, x in enumerate(cyc)}                     # a fixed integer state on the cycle
        pt = lambda s, l: pow(g, s, q) * pow(g, 3 * k * l, q) % q                          # the point gˢ iˡ of the fibre s
        A = {(r, s): Z.sum(Z.mul(Z.conj(eta(r, l)), Z.const(psi[pt(s, l)])) for l in range(4)) for r in range(4) for s in range(k)}
        n_amp += len(A)
        # the resolution of identity Σ_{r,s} b_{r,s}(u) A_{r,s} = 4 ψ(u), the measurement vector η_r(g^{−s} u) on the fibre s
        ok &= all(Z.sum(Z.mul(eta(r, l), A[(r, s)]) for r in range(4)) == Z.const(4 * psi[pt(s, l)]) for s in range(k) for l in range(4))
        ok &= Z.sum(Z.norm2(a) for a in A.values()) == Z.const(4 * sum(v * v for v in psi.values()))   # Parseval
        # the selection rule on the pure windings ψ_k(gᵉ) = ζ^{ke}: the channel r couples to k on every fibre iff k ≡ r (mod 4)
        for kk in range(n):
            for r in range(4):
                for s in range(k):
                    amp = Z.sum(Z.mul(Z.conj(eta(r, l)), Z.zeta(kk * (s + 3 * k * l))) for l in range(4))
                    ok &= amp == (Z.zeta(kk * s, 4) if (kk - r) % 4 == 0 else Z.zero)
        # the shadow ζ ↦ g carries every amplitude to the shell's own sum (Observation.lean's form)
        ok &= all(Z.shadow(A[(r, s)], q, g) == sum(pow(g, 3 * k * ((4 - r) * l), q) * psi[pt(s, l)] for l in range(4)) % q
                  for r in range(4) for s in range(k))
        if not ok: bad.append((q, n))
    R.check("Q2", "C_12 ⊂ 𝔽_13 and C_28 ⊂ 𝔽_421, over ℤ[ζ_n] with i = ζ^{3κ}: the four core characters η_r(iˡ) = i^{rl} are "
            "orthogonal, ⟨η_r, η_r'⟩ = 4δ; on a fixed integer state the amplitudes A_{r,s} = Σ_l η̄_r(iˡ) ψ(gˢ iˡ) give the "
            "resolution of identity Σ b A = 4ψ and Parseval Σ|A|² = 4⟨ψ,ψ⟩; a pure winding k couples to the channel r on every "
            "fibre exactly when k ≡ r (mod 4); the shadow ζ ↦ g carries every amplitude to the shell's sum", not bad,
            f"{n_amp} amplitudes; exceptions {bad}")
    # Q3 the fibres: κ cosets gˢ·Q₄, a partition, each invariant under the core; the outcomes are the cosets — one iff the
    # cycle is the core (𝔽_5: C_4 = Q₄, absorbed); the shared core of two cycles C_{4κ}, C_{4κ'} is Q₄ iff gcd(κ, κ') = 1
    bad = []
    for q, g, n in cases:
        k = n // 4; fib = core_cosets(q, g); cyc = cycle(q, g); i = pow(g, 3 * k, q)
        ok = len(fib) == k and all(len(f) == 4 for f in fib) and sorted(x for f in fib for x in f) == sorted(cyc)
        ok &= all(frozenset(x * i % q for x in f) == f and frozenset((-x) % q for x in f) == f for f in fib)
        ok &= all(frozenset(pow(g, s, q) * w % q for w in [1, i, q - 1, (q - i) % q]) == fib[s] for s in range(k))
        ok &= (k == 1) == (set(cyc) == {1, i, q - 1, (q - i) % q})                        # absorbed iff the cycle is the core
        if not ok: bad.append((q, g, n))
    ok = len(core_cosets(5, 2)) == 1 and sorted(core_cosets(5, 2)[0]) == [1, 2, 3, 4]      # 𝔽_5: one outcome, classical
    shared = []
    for ka in range(1, 12):
        for kb in range(1, 12):
            q = _prime_1_mod(lcm(4 * ka, 4 * kb))
            common = [x for x in range(1, q) if pow(x, 4 * ka, q) == 1 and pow(x, 4 * kb, q) == 1]
            roots4 = [x for x in range(1, q) if pow(x, 4, q) == 1]
            shared.append((len(common) == 4 * gcd(ka, kb), (sorted(common) == sorted(roots4)) == (gcd(ka, kb) == 1)))
    ok &= all(a and b for a, b in shared)
    R.check("Q3", f"the fibres of every cycle of Q1 are the κ cosets gˢ·Q₄, a partition of the cycle, each carried to itself by "
            "i and by −1; one outcome exactly when the cycle is the core (𝔽_5); the shared core of C_{4κ} and C_{4κ'} in a shell "
            "holding both, κ, κ' < 12, has 4 gcd(κ, κ') elements and is Q₄ exactly when κ, κ' are coprime", ok and not bad,
            f"{len(shared)} pairs of capacities; exceptions {bad[:3]}")


# ------------------------------------------------------------------------------------------------------------
# block B: the binding lift (00:F6; 39-s173, rows C1 and E1)
# a pair of cycles fuses — the joint drive with unit windings reaches every state from every state — exactly when the
# cycles are coprime, exactly when the joint period is the product; otherwise the F2 offsets stay drive-confined (the
# deuteron (4, 4)); a non-unit winding confines its part to a class, so the pair does not fuse (C26); fusion carries
# the offsets on the odd cycle onto the F4 rungs (hydrogen (4, 3) → C_12 = C_4 × C_3, κ = 3 odd), the pointer channels
# the core's characters; the stations of the rung on 174 = 173 + 1; the census per node (6, 2, 2); the characters the
# drive moves dephase exactly over the fused period T' = 516 (Quantum.lean: fusion_iff, pair_offset, dephasing,
# binding_instances, binding_census; Composite.lean: winding_period, winding_confined, cluster_offset, fused_rung; Observation.lean:
# selection, orthogonality; Subject.lean: spinor).
@R.block("B", BLOCKS["B"])
def block_B():
    """Block B — the binding lift (EXACT): B1–B3."""
    # 00:F6 (p00064)
    bad, n_fused, n_pairs = [], 0, 0
    for a in range(1, CYCLES + 1):
        for b in range(2, CYCLES + 1):
            g, T = gcd(a, b), lcm(a, b)
            fused = fusion(a, b)
            ok = fused == (g == 1) == (T == a * b) == (joint_period([a, b]) == a * b)
            if a * b <= 36:                                                                 # fusion: every state reaches every state
                ok &= fused == all(reach(x, y, x2, y2, a, b) is not None for x in range(a) for y in range(b) for x2 in range(a) for y2 in range(b))
            orbs = orbits(a, b)
            if g > 1: ok &= reach(0, 0, 0, 1, a, b) is None and len(orbs) == g and all(len(o) == T for o in orbs)   # drive-confined: (0, 0) never reaches (0, 1)
            else: ok &= len(orbs) == 1 and len(orbs[0]) == a * b
            ok &= all(len({offset(x, y, g) for x, y in o}) == 1 for o in orbs)              # each orbit one offset class (x − y) mod g
            ok &= len({offset(o[0][0], o[0][1], g) for o in orbs}) == g                      # the g classes, one orbit each
            n_fused += fused; n_pairs += 1
            if not ok: bad.append((a, b))
    # the windings must be units: a winding u on the cycle a has the period a / gcd(a, u) (C26), so a coprime pair with a
    # non-unit winding does not fuse
    bad_w = []
    for a in range(2, 13):
        for b in range(2, 13):
            if gcd(a, b) != 1: continue
            for u in range(1, a):
                for v in range(1, b):
                    orb, st = [], (0, 0)
                    while st not in orb: orb.append(st); st = ((st[0] + u) % a, (st[1] + v) % b)
                    per = lcm(a // gcd(a, u), b // gcd(b, v))
                    if not (len(orb) == per and (len(orb) == a * b) == (gcd(a, u) == 1 and gcd(b, v) == 1)): bad_w.append((a, b, u, v))
    R.check("B1", f"every pair of cycles a ≤ {CYCLES}, 2 ≤ b ≤ {CYCLES}, unit windings: the joint drive has one orbit exactly when "
            "gcd(a, b) = 1, exactly when the joint period is a b; otherwise (0, 0) never reaches (0, 1) and the gcd(a, b) orbits "
            "of lcm(a, b) states are the offset classes (x − y) mod g, one each; on coprime pairs 2 ≤ a, b ≤ 12 a winding (u, v) "
            "has the period lcm(a/gcd(a, u), b/gcd(b, v)), the whole product exactly for unit windings",
            not bad and not bad_w and n_pairs == CYCLES * (CYCLES - 1) and n_fused > 0,
            f"{n_pairs} pairs, {n_fused} fused; exceptions {bad[:3]} {bad_w[:3]}")
    # B2 the instances (39:C1, E1): the deuteron (4, 4) and hydrogen (4, 3); the fused cycle C_12 = C_4 × C_3 on 𝔽_13 and the
    # F4 rungs; T' = lcm(172, 3) = 516; the stations of the rung on 174
    ok = not fusion(4, 4) and len(orbits(4, 4)) == 4 and reach(0, 0, 0, 1, 4, 4) is None
    ok &= all(len({offset(x, y, 4) for x, y in o}) == 1 for o in orbits(4, 4))             # the deuteron's offsets stay
    ok &= fusion(4, 3) and len(orbits(4, 3)[0]) == 12
    ok &= sorted((e % 4, e % 3) for e in range(12)) == [(x, y) for x in range(4) for y in range(3)]   # C_12 ≅ C_4 × C_3
    ok &= 12 % 8 == 4 and bool(fold_solutions(3)) and not fold_solutions(4)               # κ = 3 odd: the product form
    fold = division_fold(13, 2); inv = {x: rs for rs, x in fold.items()}; cyc = cycle(13, 2)
    ok &= all(inv[cyc[e]] == ((3 * (e // 3)) % 4, e % 3) for e in range(12))             # the rung s = e mod 3: the offset on C_3
    p, g = 173, frame(173)[1]
    ok &= joint_period([p - 1, 3]) == 516 == lcm(p - 1, 3) and 516 % 12 == 0 and (p - 1) % 4 == 0
    ok &= (p + 1) % 3 == 0 and (p - 1) % 3 != 0 and home(3, p) == "torus"                   # the 3-cycle on the boost torus
    ok &= [s * (p + 1) // 3 for s in range(3)] == [0, 58, 116] and 3 * 58 == p + 1          # the stations of the rung
    # "ground first" (39-s173, the census): per node x₀ of 𝔽_173^×, over T' = 516 chronons, the sign coincidences
    # x₀ gᵗ ∈ {±1} with s t ≡ 0 (mod 3) number 6 on the ground rung s = 0 and 2 on each lift: W_s = 2 gcd(s, 3), 3 : 1 : 1
    census = {x0: [sum(1 for t in range(516) if x0 * pow(g, t, p) % p in (1, p - 1) and s * t % 3 == 0) for s in range(3)]
              for x0 in range(1, p)}
    ok &= len(census) == p - 1 and all(w == [6, 2, 2] for w in census.values()) and [2 * gcd(s, 3) for s in range(3)] == [6, 2, 2]
    R.check("B2", "the deuteron (4, 4): four orbits, each one offset, (0, 0) never reaches (0, 1), no fusion; hydrogen (4, 3): one "
            "orbit of 12, C_12 ≅ C_4 × C_3, κ = 3 odd (12 % 8 ≠ 0, 3κr + 4s ≡ 1 solvable); on C_12 = ⟨2⟩ ⊂ 𝔽_13 the rung of the "
            "division fold is the offset e mod 3; T' = lcm(172, 3) = 516, 12 | 516; the stations {0, 58, 116} of the rung on "
            "174 = 173 + 1 = 3·58, the 3-cycle on the boost torus of 173; the census per node of 𝔽_173^× over T': 6 sign "
            "coincidences on the ground rung and 2 on each lift, W_s = 2 gcd(s, 3), the rates 3 : 1 : 1, the ground rung first",
            ok, f"{len(census)} nodes, the census {sorted(set(map(tuple, census.values())))}")
    # B3 dephasing over the fused period: the (172, 3) composite in 𝔽_1033 (1033 = 2·516 + 1), every character the drive moves
    # sums to zero over T' = 516; 1 + ω + ω² = 0 exactly in ℤ[ζ_3], and the cubic character over 516 steps in 𝔽_13
    q = 1033
    ok = arith.is_prime(q) and q == 2 * 516 + 1
    sums = character_sums(q, 172, 3, 516)
    moved = [s for m, s in sums if m]; still = [s for m, s in sums if not m]
    ok &= len(sums) == 516 and len(moved) == 515 and all(s == 0 for s in moved) and still == [516 % q]
    Z3 = Cyclotomic(3)
    ok &= Z3.sum(Z3.zeta(e) for e in range(3)) == Z3.zero                                   # 1 + ω + ω² = 0 in ℤ[ζ_3]
    w = root_of_unity(13, 3)
    ok &= w == 3 and (1 + w + w * w) % 13 == 0 and sum(pow(w, t, 13) for t in range(516)) % 13 == 0
    R.check("B3", "the (172, 3) composite in 𝔽_1033: of the 516 characters the 515 the drive moves sum to zero over the fused period "
            "T' = 516 and the trivial one to 516 (Born lands with exact dephasing); 1 + ω + ω² = 0 in ℤ[ζ_3]; the cubic "
            "character ω = 3 of 𝔽_13 sums to zero over 516 steps", ok, f"{len(moved)} of {len(sums)} character sums cancel")


# ------------------------------------------------------------------------------------------------------------
# block C: the coherent-fraction channel (00:P2) — 22:C21's content: the cells on C_16 with the ledger ℤ[ζ_16]
@R.block("C", BLOCKS["C"])
def block_C():
    """Block C — the coherent-fraction channel (EXACT): C1–C2."""
    # 00:P2 (p00061)
    Z = Cyclotomic(16); zp = Z.zeta
    def power(a, k):
        out = Z.one
        for _ in range(k): out = Z.mul(out, zp(a))
        return out
    branch = all(power(a, mc) == zp(mc * a) for a in range(1, 16) for mc in (2, 3, 4))            # the synchronised branch phase ζ^{m_c a}
    pair = 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))   # the pairwise phase ζ^{m₁m₂a}
    spread = all(Z.sum(zp(a * s) for s in range(16)) == Z.zero for a in range(1, 16))              # a complete spread sums to zero
    sector = lambda offs, a: Z.sum(zp(a * s) for s in offs)
    avg = lambda offs, a, mc: Z.sum(Z.mul(zp(mc * a), zp(a * s)) for s in offs)
    factor = avg([0, 4, 8, 12], 3, 2) == Z.mul(zp(6), sector([0, 4, 8, 12], 3)) and avg([0, 0, 4, 8], 3, 2) == Z.mul(zp(6), sector([0, 0, 4, 8], 3))
    envelope = Z.norm2(sector([0, 0, 0, 0], 1)) == Z.const(16) and sector([0, 4, 8, 12], 1) == Z.zero
    R.check("C1", "the coherent-fraction channel on C_16 in ℤ[ζ_16]: the synchronised branch phase is ζ^{m_c a} exactly (m_c = 2, 3, 4, "
            "every a), the pairwise entangling phase ζ^{m₁ m₂ a} (force by full masses, entanglement by the coherent fractions), "
            "a complete offset spread sums to zero for every a ≠ 0, the reduced channel factorises as ζ^{m_c a} χ_inc for a "
            "complete and a nonuniform spread, and the envelope |Σ|² is m² = 16 synchronised and 0 at complete spread",
            branch and pair and spread and factor and envelope)
    q = Fr(1, 4)
    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)
    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)
    ok &= canon((0, 0, 0, 1)) not in achievable
    R.check("C2", "the incoherent channel is separable at generic geometry: of the 15 branch partitions at complete spread, the "
            "partial transpose is negative exactly at the blocks of three (spectrum 1/4, 1/4, (1 ± √3)/4) and positive "
            "otherwise; locally additive spread phases a_x + b_y (n ≤ 6) never make a block of three, so every achievable "
            "partition is PPT, hence separable (C = 0 at f = 0)", ok, f"{len(achievable)} achievable partitions")


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