"""master/foundation — the ledger file of the master's block A, the Foundation (ledger migration, task LM23, 5 October 2026).

The master predicate ledger (00-ledger/predicates/index.md, published as docs/00-ledger.json) states block A. This file
binds its theorem rows to the framework: the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py),
the Lean proofs each key conjoins (PROOFS, written here), the shells, and the checks, which call the foundation theme
(frc/foundation.py). Each check names the rows it decides or corroborates (LEDGER), under a `# 00:A5 (p00188)` marker on
the check that decides the row (PREDICATES).

The rows are A2, A3 and A4 (the three former pillars, theorems since 9 October 2026: the registered Universe of any
totality is finite and no reading registers an unlimited supply, with the agent's bound; the registration of any
totality is onto its registered Universe, and two totalities each registered whole within the other have one count;
the incompleteness of observation — every reading of a part identifies two members, complete only at the whole count,
and no frame sees more, the Carrier a translation torsor; until 9 October two rows, the bounded observer A4 and
Registration A5, merged that day; retitled with A3, Completeness of the totality, on 13 October), A5,
A10, A11 and A12, the block's T rows, proved in
lean/FrcCore/Theme/Foundation.lean and lean/FrcCore/Theme/Drive.lean with no generator assumed. A9, the trusted base, is
a D row: gate G19 enforces its clause on unboundedness, and every key's empty axiom list (gate G08) its kernel clause.
The checks run on the three Carriers of the Carrier's block file, Ω = 233, 30 089 and 2 408 561, with their Subjects
13, 173 and 1 373, and as sweeps over every modulus or prime below a bound. The Lean side is the key file
lean/FrcCore/Keys/Foundation.lean and the certificate lean/FrcCore/Ledgers/Master/Foundation.lean.

    python3 -m frc.ledgers.master.foundation        every block, the census; exit 1 if a check fails (≈ 15 s)
    python3 -m frc.ledgers.master.foundation M      one block (F, V, U, W, Q, I, H or M)
    from frc.ledgers.master.foundation import R; R.predicate("00:A12")    one row: its blocks run once per session

Blocks:  F  the registered Universe is finite; the agent's bound   EXACT  (00:A2)
         V  the registration is onto; mutual registration is one count  EXACT  (00:A3)
         U  every reading of a proper part identifies two members  EXACT  (00:A4)
         W  a complete reading needs the whole; the torsor EXACT  (00:A4)
         Q  counting closes by return                     EXACT  (00:A5)
         I  completeness is primality                     EXACT  (00:A10)
         H  the quarter-turn exists iff p ≡ 1 (mod 4)     EXACT  (00:A11)
         M  every prime carries a frame                   EXACT  (00:A12)

The notebook frc/ledgers/master/foundation.ipynb runs one row per cell, the cell's id its key (gate G13).
"""
import itertools
import sys

from frc import arith
from frc.registry import Registry
from frc.foundation import (half_power, quarter_turn, quarter_turns, successor_orbit, principal_ideal, is_complete,
                            zero_divisors, element_order, drive, collision)
from frc.formation import records

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "A"
KEYS = {"A1": "p00001", "A2": "p00004", "A3": "p00003", "A4": "p00197", "A5": "p00188", "A6": "p00008", "A7": "p00009", "A8": "p00010", "A9": "p00161", "A10": "p00162", "A11": "p00163", "A12": "p00164", "A13": "p00196"}       # every row of the block: its label and its accession key
LEAN = {"A2": "core", "A3": "core", "A4": "core", "A5": "core", "A10": "core", "A11": "core", "A12": "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 = {
    "A2": ["FRC.Foundation.registered_finite", "FRC.Foundation.no_unlimited_supply", "FRC.Foundation.agent_bound"],
    "A3": ["FRC.Foundation.registration_onto", "FRC.Foundation.mutual_registration_count"],
    "A4": ["FRC.Foundation.observer_part", "FRC.Foundation.complete_needs_whole", "FRC.Foundation.translation_torsor"],
    "A5": ["FRC.Foundation.successor_cycle"],
    "A10": ["FRC.Shell.Prime.isPrime_iff_complete"],
    "A11": ["FRC.Shell.Prime.quarter_turn_iff"],
    "A12": ["FRC.Shell.Prime.exists_drive"],
}

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

# The Carriers (Ω, the Subject p), as in the Carrier's block file: Ω = 4S + 1 prime, p prime with p² < Ω.
SHELLS = [(233, 13), (30089, 173), (2408561, 1373)]
SWEEP = 5000                    # the sweeps over primes run below it
SMALL = 6                       # the exhaustive readings run over every total of at most SMALL points

# The rows each check decides or corroborates.
LEDGER = {
    "F1": "00:A2", "F2": "00:A2", "F3": "00:A2", "F4": "00:A2",
    "V1": "00:A3", "V2": "00:A3", "V3": "00:A3",
    "U1": "00:A4", "U2": "00:A4", "U3": "00:A4",
    "W1": "00:A4", "W2": "00:A4",
    "Q1": "00:A5", "Q2": "00:A5",
    "I1": "00:A10", "I2": "00:A10",
    "H1": "00:A11", "H2": "00:A11",
    "M1": "00:A12", "M2": "00:A12", "M3": "00:A12",
}

BLOCKS = {"F": "the registered Universe of any totality is finite; no reading registers an unlimited supply; the agent's bound",
          "V": "the registration is onto its registered Universe; mutual registration is one count",
          "U": "every reading of a proper part identifies two members (a bounded observer is a proper part)",
          "W": "a complete reading needs the whole count; the Carrier is a translation torsor", "Q": "counting closes by return", "I": "completeness is primality",
          "H": "the quarter-turn exists iff p ≡ 1 (mod 4)", "M": "every prime carries a frame"}

# the deciding check of each row; the sweeps corroborate
PREDICATES = {"00:A2": "F1", "00:A3": "V3", "00:A4": "U1", "00:A5": "Q1", "00:A10": "I2", "00:A11": "H1", "00:A12": "M1"}

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

for _Om, _p in SHELLS:
    assert arith.is_prime(_Om) and _Om % 4 == 1 and arith.is_prime(_p) and _p * _p < _Om, (_Om, _p)


def _primes(lo, hi):
    return [n for n in range(lo, hi) if arith.is_prime(n)]


# ------------------------------------------------------------------------------------------------------------
# block F: the registered Universe is finite (00:A2)
# what a reading of capacity R registers of any totality — its residues — has at most R members, whatever the totality
# (Foundation.lean, registered_finite: the registered Universe embeds in the shell of R points); among any R + 1 members
# two share a residue (no_unlimited_supply); an agent of capacity K over s symbols has records(s, K) < s^(K+1) records,
# so a shell read whole into them has at most that many members (agent_bound, 5:C2).
def _injective(rho, n):
    return collision(rho, n) is None


def _registered(rho, members):
    """The registered Universe of the members under the reading rho: the set of residues (Foundation.lean, Registered)."""
    return sorted({rho(u) for u in members})


@R.block("F", BLOCKS["F"])
def block_F():
    """Block F — the registered Universe is finite; the agent's bound (EXACT): F1–F4."""
    # 00:A2 (p00004)
    bad, det = [], []
    totalities = {"[0, 10^5)": range(10 ** 5), "the odd naturals below 2·10^5": range(1, 2 * 10 ** 5, 2),
                  "the squares below 10^10": (k * k for k in range(10 ** 5))}
    for name, members in totalities.items():
        members = list(members)
        for R_ in (1, 2, 7, 13, 233):
            readings = {"u mod R": lambda u, R_=R_: u % R_, "u mod R, squared": lambda u, R_=R_: (u * u) % R_,
                        "min(u, R−1)": lambda u, R_=R_: min(u, R_ - 1)}
            for rname, rho in readings.items():
                reg = _registered(rho, members)
                emb = [r % R_ for r in reg]                                   # the embedding into the shell of R points, by ofNat
                if not (len(reg) <= R_ and all(0 <= r < R_ for r in reg) and len(set(emb)) == len(reg)): bad.append((name, R_, rname, len(reg)))
                # among any R + 1 members two share a residue: the first R + 1 members, and R + 1 members spread out
                for sample in (members[:R_ + 1], members[::max(1, len(members) // (R_ + 1))][:R_ + 1]):
                    if len(sample) == R_ + 1 and _injective(lambda i, s=sample, rho=rho: rho(s[i]), R_ + 1): bad.append((name, R_, rname, "no collision"))
        det.append(f"{name}: under every reading into R ∈ {{1, 2, 7, 13, 233}} records the residues number ≤ R and embed in the shell of R points")
    R.check("F1", "three totalities of 10^5 members, three readings each into R ∈ {1, 2, 7, 13, 233} records: the registered Universe (the "
            "residues) has at most R members and embeds in the shell of R points; among any R + 1 members two share a residue",
            not bad, "; ".join(det) + f"; exceptions {bad[:3]}")
    # F2 the same on the three Carriers as totalities read by their Subjects' capacities, and on an unbounded totality: the
    # naturals read into R records have exactly R residues, found below R, and every R + 1 of them collide
    bad, det = [], []
    for Om, p in SHELLS:
        reg = _registered(lambda u: u % p, range(Om))
        c = collision(lambda i: i % p, p + 1)
        if not (len(reg) == p and c is not None): bad.append((Om, p))
        det.append(f"Ω={Om} read into p={p} records: {len(reg)} residues; {c} collide among the first p + 1")
    for R_ in (3, 10, 1000):
        reg = _registered(lambda u: u % R_, range(10 * R_))
        if not (len(reg) == R_ and max(reg) == R_ - 1): bad.append(("naturals", R_))
    R.check("F2", "the three Carriers read into their Subjects' p records: exactly p residues, a collision among the first p + 1 "
            "members; the naturals read into R ∈ {3, 10, 1000} records: R residues, all below R", not bad, "; ".join(det))
    # F3 the agent's bound
    bad, det = [], []
    for s in (2, 3):
        for K in range(0, 3):
            rc = records(s, K)
            if not (rc == sum(s ** l for l in range(K + 1)) and rc < s ** (K + 1)): bad.append((s, K, rc))
            for n in range(1, min(rc, SMALL) + 3):                            # every reading of n members into rc records
                whole = any(_injective(lambda u: rho[u], n) for rho in itertools.product(range(rc), repeat=n))
                if whole != (n <= rc): bad.append((s, K, n))
            det.append(f"s={s}, K={K}: records {rc} < {s ** (K + 1)}; read whole iff n ≤ {rc}")
    R.check("F3", f"s ∈ {{2, 3}}, K ≤ 2: records(s, K) = Σ_{{l≤K}} s^l < s^(K+1), and a shell of n members is read whole (an injective "
            "reading, exhaustive over the readings) into records(s, K) records iff n ≤ records(s, K): the agent's bound",
            not bad, "; ".join(det[:3]) + f"; exceptions {bad}")
    # F4 the count bound alone, wider: records(s, K) < s^(K+1) for s ≤ 7 and K ≤ 12, and on the three Carriers an agent of
    # capacity K with records(2, K) < Ω reads the Carrier incompletely (a collision found by search)
    bad, det = [], []
    for s in range(2, 8):
        for K in range(0, 13):
            if not records(s, K) < s ** (K + 1): bad.append((s, K))
    for Om, p in SHELLS:
        K = max(k for k in range(60) if records(2, k) < Om)
        rc = records(2, K)
        c = collision(lambda x: x % rc, Om)
        if c is None or c[0] == c[1] or (c[0] % rc) != (c[1] % rc): bad.append((Om, K))
        det.append(f"Ω={Om}: K={K}, records(2, K)={rc} < Ω, x mod records identifies {c}")
    R.check("F4", "s ≤ 7, K ≤ 12: records(s, K) < s^(K+1); on the three Carriers, the largest K with records(2, K) < Ω: a reading "
            "into those records identifies two members (by search)", not bad, "; ".join(det))
# ------------------------------------------------------------------------------------------------------------
# block V: mutual registration is one count (00:A3)
# injections both ways between shells force equal counts (the pigeonhole both ways; Foundation.lean,
# mutual_registration_count); a larger shell registers a smaller, so the theorem is silent on a host.
@R.block("V", BLOCKS["V"])
def block_V():
    """Block V — the registration is onto; mutual registration is one count (EXACT): V1–V3."""
    # 00:A3 (p00003)
    bad = []
    for m in range(1, SMALL + 1):
        for n in range(1, SMALL + 1):
            inj_mn = any(_injective(lambda x: f[x], m) for f in itertools.product(range(n), repeat=m))
            inj_nm = any(_injective(lambda x: g[x], n) for g in itertools.product(range(m), repeat=n))
            if (inj_mn and inj_nm) != (m == n) or inj_mn != (m <= n): bad.append((m, n))
    R.check("V1", f"every m, n ≤ {SMALL}: an injective reading of m members into n exists iff m ≤ n (exhaustive), so injections both "
            "ways exist iff m = n: two totalities each registered whole within the other have one count", not bad, f"exceptions {bad}")
    # V2 on the three Carriers: the Subject's p members are registered injectively in the Carrier (the identity), the Carrier's
    # Ω are not registered injectively in p states (a collision found by search): the larger shell hosts the smaller
    ok, det = True, []
    for Om, p in SHELLS:
        c = collision(lambda x: x % p, Om)
        ok &= _injective(lambda x: x, p) and c is not None and (c[0] % p) == (c[1] % p) and c[0] != c[1]
        det.append(f"Ω={Om}, p={p}: x ↦ x identifies no two of the p; x mod p identifies {c} of the Ω")
    R.check("V2", "on the three Carriers: the Subject is registered injectively within the Carrier and the Carrier is not within "
            "the Subject (collision by search): a larger shell registers a smaller, the theorem silent on a host", ok, "; ".join(det))
    # V3 the registration is onto: every residue of the registered Universe is some member's, and every member has its residue —
    # on the three Carriers read into p records and on the naturals read into R records
    bad, det = [], []
    for Om, p in SHELLS:
        reg = _registered(lambda u: u % p, range(Om))
        preimages = {r: next(u for u in range(Om) if u % p == r) for r in reg}
        if not (all(preimages[r] % p == r for r in reg) and all((u % p) in set(reg) for u in range(0, Om, max(1, Om // 1000)))): bad.append(Om)
        det.append(f"Ω={Om}, p={p}: each of the {len(reg)} residues is a member's, each sampled member's residue is registered")
    for R_ in (3, 10, 1000):
        reg = _registered(lambda u: u % R_, range(10 * R_))
        if not all(any(u % R_ == r for u in range(10 * R_)) for r in reg): bad.append(("naturals", R_))
    R.check("V3", "the registration is onto its registered Universe: on the three Carriers read into p records and on the naturals "
            "read into R ∈ {3, 10, 1000} records, every registered residue is a member's and every member's residue is registered",
            not bad, "; ".join(det))


# ------------------------------------------------------------------------------------------------------------
# block U: every reading of a proper part identifies two members — a bounded observer is a proper part (00:A4)
# an observer with o < Ω states holds no injective encoding of the Ω points: every reading identifies two distinct points
# (Foundation.lean, observer_part; the pigeonhole). The row's other clauses are block W.
@R.block("U", BLOCKS["U"])
def block_U():
    """Block U — a bounded observer is a proper part (EXACT): U1–U3."""
    # 00:A4 (p00197)
    total, bad = 0, []
    for n in range(1, SMALL + 1):
        for o in range(n):
            for rho in itertools.product(range(o), repeat=n):
                total += 1
                if collision(lambda x: rho[x], n) is None: bad.append((n, o, rho))
    R.check("U1", f"every total of n ≤ {SMALL} points and every observer of o < n states: each of the o^n readings identifies two "
            "distinct points (exhaustive)", not bad, f"{total} readings; injective ones {bad[:3]}")
    # U2 the bound is sharp: o = n states admit an injective reading
    ok = all(collision(lambda x: x, n) is None for n in range(1, SMALL + 1)) and all(
        all(collision(lambda x: rho[x], n) is None for rho in itertools.permutations(range(n))) for n in range(1, SMALL + 1))
    R.check("U2", f"the bound is sharp: for every n ≤ {SMALL}, an observer of n states reads the n points injectively (each of the n! "
            "bijections, the identity among them)", ok, "o < n forces a collision, o = n does not")
    # U3 on the three Carriers, an observer of Ω − 1 states: three readings, each with two distinct points found by search
    ok, det = True, []
    for Om, p in SHELLS:
        o = Om - 1
        readings = {"x mod (Ω−1)": lambda x: x % o, "min(x, Ω−2)": lambda x: min(x, o - 1),
                    "p x mod (Ω−1)": lambda x: p * x % o}
        for name, rho in readings.items():
            c = collision(rho, Om)
            ok &= c is not None and c[0] != c[1] and rho(c[0]) == rho(c[1]) and all(0 <= rho(x) < o for x in (c[0], c[1]))
        det.append(f"Ω={Om}: x mod (Ω−1) identifies {collision(readings['x mod (Ω−1)'], Om)}")
    R.check("U3", "on the three Carriers, an observer of Ω − 1 states: the readings x mod (Ω−1), min(x, Ω−2) and p·x mod (Ω−1) each "
            "identify two distinct points, found by search", ok, "; ".join(det))


# ------------------------------------------------------------------------------------------------------------
# block W: a complete reading needs the whole count; the Carrier is a translation torsor (00:A4, with block U)
# a reading of the Ω members into o records that identifies no two has Ω ≤ o (the contrapositive of observer_part);
# exactly one translation carries each member to each (Foundation.lean, complete_needs_whole, translation_torsor).
@R.block("W", BLOCKS["W"])
def block_W():
    """Block W — a complete reading needs the whole count; the translation torsor (EXACT): W1, W2."""
    # the row's second and third clauses (the marker of 00:A4 is on block U's deciding check U1)
    bad = []
    for n in range(1, SMALL + 1):
        for o in range(1, n + 2):
            complete = [rho for rho in itertools.product(range(o), repeat=n) if _injective(lambda u: rho[u], n)]
            if (len(complete) > 0) != (n <= o): bad.append((n, o, len(complete)))
    R.check("W1", f"every n ≤ {SMALL} and o ≤ n + 1: a reading of the n members into o records that identifies no two exists iff "
            "n ≤ o (exhaustive): a complete reading needs the whole count (the contrapositive of U1), a part of o < n states reads incompletely",
            not bad, f"exceptions {bad}")
    # W2 the translation torsor: on every q ≤ 40 and every pair (x, y), exactly one t with x + t = y; on the three Carriers and
    # their Subjects, sampled pairs
    bad, det = [], []
    for q in range(1, 41):
        for x in range(q):
            for y in range(q):
                if [t for t in range(q) if (x + t) % q == y] != [(y - x) % q]: bad.append((q, x, y))
    for Om, p in SHELLS:
        for q in (Om, p):
            pairs = ((0, 1), (1, 0), (q - 1, q // 2), (q // 3, q - 2)) if q < 10 ** 5 else ((1, 0), (q // 3, q - 2))
            for x, y in pairs:
                sols = sum(1 for t in range(q) if (x + t) % q == y)              # every t, exhaustively
                if sols != 1 or (x + (y - x) % q) % q != y: bad.append((q, x, y, sols))
            det.append(f"q={q}: one t per pair, counted over all {q} translations")
    R.check("W2", "every q ≤ 40 and every pair (x, y): exactly one translation t with x + t = y (exhaustive); on the three Carriers "
            "and their Subjects, sampled pairs with every translation tried: exactly one. The origin is frame data (A6)", not bad, "; ".join(det[:3]))


# ------------------------------------------------------------------------------------------------------------
# block Q: counting closes by return (00:A5)
# on q ≥ 2 points the successor x ↦ x + 1 has no fixed point, returns after exactly the multiples of q steps and
# reaches every point (Foundation.lean, successor_cycle).
@R.block("Q", BLOCKS["Q"])
def block_Q():
    """Block Q — counting closes by return (EXACT): Q1, Q2."""
    # 00:A5 (p00188)
    ok, det = True, []
    for Om, p in SHELLS:
        for q in (Om, p):
            orb = successor_orbit(q, 0)
            ok &= len(orb) == q and sorted(orb) == list(range(q)) and all((x + 1) % q != x for x in (0, 1, q - 1))
        det.append(f"Ω={Om}: one cycle of {Om}; p={p}: one cycle of {p}")
    R.check("Q1", "on the three Carriers and their Subjects: the orbit of 0 under x ↦ x + 1 returns after exactly q steps and "
            "visits every point; x + 1 ≠ x", ok, "; ".join(det))
    # Q2 every q in [2, 400): the k-th iterate fixes a point iff q | k (k < 3q), every orbit is all of [0, q), no fixed point
    bad = []
    for q in range(2, 400):
        for x in (0, q // 2, q - 1):
            y, ret = x, []
            for k in range(1, 3 * q):
                y = (y + 1) % q
                if y == x: ret.append(k)
            if ret != [q, 2 * q] or sorted(successor_orbit(q, x)) != list(range(q)): bad.append((q, x))
        if any((x + 1) % q == x for x in range(q)): bad.append((q, "fixed point"))
    R.check("Q2", "every q in [2, 400) and x ∈ {0, ⌊q/2⌋, q−1}: C_q^k x = x for 0 < k < 3q exactly at k = q, 2q (by iteration); every "
            "orbit is all of [0, q); no point is fixed", not bad, f"exceptions {bad[:5]}")


# ------------------------------------------------------------------------------------------------------------
# block I: completeness is primality (00:A10)
# for q ≥ 2, every ideal of Z/q holding a nonzero residue holds every residue iff q is prime (Foundation.lean,
# isPrime_iff_complete): forward by the Fermat inverse a^(q−2), backward by the annihilator of a zero divisor.
@R.block("I", BLOCKS["I"])
def block_I():
    """Block I — completeness is primality (EXACT): I1, I2."""
    # I1 the forward construction on the Carriers and the Subjects: a^(q−2) inverts every nonzero a
    ok, det = True, []
    for Om, p in SHELLS[:2]:
        for q in (Om, p):
            ok &= all(a * pow(a, q - 2, q) % q == 1 for a in range(1, q))
        det.append(f"q={Om} and q={p}: a·a^(q−2) = 1 for every a ≠ 0")
    Om = SHELLS[2][0]
    ok &= all(a * pow(a, Om - 2, Om) % Om == 1 for a in range(1, 200001))
    det.append(f"q={Om}: for a < 200 001")
    R.check("I1", "on the Carriers and their Subjects: the Fermat inverse a^(q−2) of every nonzero a, so 1 lies in every ideal holding "
            "a, and with it every residue", ok, "; ".join(det))
    # 00:A10 (p00162)
    bad, det = [], []
    for q in range(2, 260):
        comp, prime, zd = is_complete(q), arith.is_prime(q), zero_divisors(q)
        if not (comp == prime == (not zd)): bad.append(q)
        if not prime:
            a, b = zd[0]
            ann = [x for x in range(q) if x * b % q == 0]                       # the annihilator of b, an ideal holding a
            if not (a in ann and 1 not in ann and principal_ideal(a, q) != list(range(q))): bad.append((q, "annihilator"))
    R.check("I2", "every q in [2, 260): Z/q has no proper nonzero ideal (every residue's ideal holds 1, by search) iff q is prime iff "
            "no zero divisors; for composite q the annihilator of a zero divisor b is a proper ideal holding a ≠ 0", not bad,
            f"258 moduli, {sum(1 for q in range(2, 260) if arith.is_prime(q))} prime; exceptions {bad[:5]}")


# ------------------------------------------------------------------------------------------------------------
# block H: the quarter-turn exists iff p ≡ 1 (mod 4) (00:A11)
# for an odd prime p, x² = −1 is solvable iff p ≡ 1 (mod 4) (Foundation.lean, quarter_turn_iff): backward ħ = a^((p−1)/4)
# with a^((p−1)/2) = −1; forward ħ⁴ = 1 and Fermat leave (p − 1) mod 4 = 0.
@R.block("H", BLOCKS["H"])
def block_H():
    """Block H — the quarter-turn exists iff p ≡ 1 (mod 4) (EXACT): H1, H2."""
    # 00:A11 (p00163)
    primes = _primes(3, SWEEP)
    bad = [p for p in primes if bool(quarter_turns(p)) != (p % 4 == 1)]
    built = [p for p in primes if p % 4 == 1 and quarter_turn(p) ** 2 % p != p - 1]
    R.check("H1", f"every odd prime p < {SWEEP}: x² = −1 has a root (by search) iff p ≡ 1 (mod 4); on p ≡ 1 (mod 4) the generator-free "
            "ħ = a^((p−1)/4) is one", not bad and not built, f"{len(primes)} primes; exceptions {bad + built}")
    # H2 the Carriers and their Subjects: ħ = a^S, ħ² = −1, and the two roots ±ħ
    ok, det = True, []
    for Om, p in SHELLS:
        for q in (Om, p):
            h = quarter_turn(q); a = half_power(q)
            ok &= q % 4 == 1 and pow(a, (q - 1) // 2, q) == q - 1 and h == pow(a, (q - 1) // 4, q) and h * h % q == q - 1
            if q < 10 ** 5: ok &= sorted(quarter_turns(q)) == sorted({h, q - h})
        det.append(f"Ω={Om}: ħ={quarter_turn(Om)}; p={p}: ħ={quarter_turn(p)}")
    R.check("H2", "on the three Carriers and their Subjects (all ≡ 1 mod 4): ħ = a^S with a^(2S) = −1 solves x² = −1, and below 10⁵ the "
            "roots are exactly ±ħ (by search)", ok, "; ".join(det))


# ------------------------------------------------------------------------------------------------------------
# block M: every prime carries a frame (00:A12)
# every prime field has a primitive root, and its powers reach every nonzero residue (Drive.lean, exists_drive): the
# proof's construction is the product over the prime powers qᵉ ∥ p − 1 of a^((p−1)/qᵉ), a the least with a^((p−1)/q) ≠ 1.
@R.block("M", BLOCKS["M"])
def block_M():
    """Block M — every prime carries a frame (EXACT): M1–M3."""
    # 00:A12 (p00164)
    ok, det = True, []
    for Om, p in SHELLS:
        for q in (Om, p):
            g = drive(q)
            n = element_order(g, q)                                          # by iteration
            powers, y = set(), 1
            for _ in range(q - 1):
                powers.add(y); y = y * g % q
            ok &= n == q - 1 and arith.is_primitive_root(g, q) and powers == set(range(1, q))
        det.append(f"Ω={Om}: g={drive(Om)}; p={p}: g={drive(p)}")
    R.check("M1", "on the three Carriers and their Subjects: the drive g built by the proof's construction has order p − 1 (by iteration "
            "and by the factorisation of p − 1), and g⁰, …, g^(p−2) are all p − 1 nonzero residues", ok, "; ".join(det))
    # M2 every prime below SWEEP: the construction gives a primitive root, each factor z_q of order exactly qᵉ
    bad = []
    for p in _primes(2, SWEEP):
        n = p - 1
        for q, e in arith.factorize(n).items():
            a = next(a for a in range(1, p) if pow(a, n // q, p) != 1)
            z = pow(a, n // q ** e, p)
            if not (pow(z, q ** e, p) == 1 and pow(z, q ** (e - 1), p) != 1): bad.append((p, q))
        if arith.order(drive(p), p) != n: bad.append(p)
    R.check("M2", f"every prime p < {SWEEP}: for each qᵉ ∥ p − 1 the factor z_q = a^((p−1)/qᵉ) has order exactly qᵉ, and their product "
            "is a primitive root", not bad, f"{len(_primes(2, SWEEP))} primes; exceptions {bad[:5]}")
    # M3 every prime below 400: the elements of order p − 1, by iteration, number φ(p − 1), the drive among them
    bad = []
    for p in _primes(2, 400):
        prim = [x for x in range(1, p) if element_order(x, p) == p - 1]
        if len(prim) != arith.phi(p - 1) or drive(p) not in prim: bad.append(p)
    R.check("M3", "every prime p < 400: the elements of order p − 1, found by iteration, number φ(p − 1) and include the drive", not bad,
            f"{len(_primes(2, 400))} primes; exceptions {bad}")


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)