"""master/subject — the ledger file of the master's block C, the Subject (ledger migration, task LM24, 5 October 2026).

The master predicate ledger (00-ledger/predicates/index.md, published as docs/00-ledger.json) states block C. 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 subject theme
(frc/subject.py). Each check names the rows it decides or corroborates (LEDGER), under a `# 00:C1 (p00021)` marker on
the check that decides the row (PREDICATES).

The rows are C1, C3, C8, C14, C16, C20 and C25, proved in lean/FrcCore/Theme/Subject.lean on the Subject's frame
(τ; 0, 1, g) and on the prime field of lean/FrcCore/Theme/Field.lean. C13 is an X row: its parts are 10:G2 (p10038) and
10:E9 (p10032), paper 10's keys; the theme proves 10:G2 on every capacity (`FRC.Subject.exponent_ladder`), and paper 10's
migration (LM36) binds it. The checks run on the three Subjects p = 13, 173 and 1 373 with their Carriers Ω = 233,
30 089 and 2 408 561, and as sweeps over every prime p = 4κ + 1 below a bound. The Lean side is the key file
lean/FrcCore/Keys/Subject.lean and the certificate lean/FrcCore/Ledgers/Master/Subject.lean.

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

Blocks:  K  the frame's web                              EXACT  (00:C1)
         I  the Euclidean–Lorentzian dichotomy           EXACT  (00:C3)
         Q  the square class is chronon parity           EXACT  (00:C8)
         O  the quarter-turn is the odd member           EXACT  (00:C14)
         V  the spinor dichotomy                         EXACT  (00:C16)
         M  the mass–energy channel                      EXACT  (00:C20)
         H  the horizon is the origin's antipode         EXACT  (00:C25)

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

from frc import arith
from frc.registry import Registry
from frc.extension import Ext
from frc.foundation import quarter_turn, quarter_turns, element_order
from frc.carrier import octant, tsirelson
from frc.subject import (frame, frames, euler, chirality, fold_image, fold_solutions, two_parts, channel,
                         projective_line, torsor, boost_act)

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "C"
KEYS = {"C1": "p00021", "C2": "p00022", "C3": "p00150", "C4": "p00024", "C5": "p00025", "C6": "p00171", "C7": "p00189", "C8": "p00028", "C9": "p00029", "C10": "p00030", "C11": "p22028", "C12": "p00032", "C14": "p00034", "C16": "p00151", "C19": "p00190", "C20": "p00040", "C21": "p00041", "C22": "p00152", "C23": "p00182", "C24": "p13064", "C25": "p00139", "C26": "p00174", "C27": "p00183"}       # every row of the block: its label and its accession key
LEAN = {"C1": "core", "C3": "core", "C8": "core", "C14": "core", "C16": "core", "C20": "core", "C25": "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 = {
    "C1": ["FRC.Subject.frame_web"],
    "C3": ["FRC.Subject.signature", "FRC.Subject.half_class"],
    "C8": ["FRC.Subject.square_class", "FRC.Subject.half_class", "FRC.Shell.Prime.tsirelson", "FRC.Extension.Ext.norm_scale"],
    "C14": ["FRC.Subject.quarter_turn_odd",
            "FRC.Shell.Frame.euler_identity"],      # 6:B2 (p06009), the Euler identity as a chart-class property (6-fourier's propagation list, row 5; 9 October 2026)
    "C16": ["FRC.Subject.spinor", "FRC.Subject.no_iso", "FRC.Subject.two_part"],
    "C20": ["FRC.Subject.channel", "FRC.Subject.channel_233"],
    "C25": ["FRC.Subject.horizon_antipode", "FRC.Subject.horizon_generator", "FRC.Subject.boost_unique"],
}

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

# The Subjects p = 4κ + 1 with their Carriers Ω = 4S + 1, as in the Carrier's block file: p² < Ω.
SHELLS = [(13, 233), (173, 30089), (1373, 2408561)]
SWEEP = 5000                    # the sweeps run over every prime p = 4κ + 1 below it
SMALL = 400                     # the sweeps over every drive of p run below it

# The rows each check decides or corroborates.
LEDGER = {
    "K1": "00:C1", "K2": "00:C1",
    "I1": "00:C3", "I2": "00:C3", "I3": "00:C3, 00:C8",
    "Q1": "00:C8", "Q2": "00:C8", "Q3": "00:C8",
    "O1": "00:C14", "O2": "00:C14",
    "V1": "00:C16", "V2": "00:C16", "V3": "00:C16",
    "M1": "00:C20", "M2": "00:C20", "M3": "00:C20",
    "H1": "00:C25", "H2": "00:C25", "H3": "00:C25",
}

BLOCKS = {"K": "the frame's web", "I": "the Euclidean–Lorentzian dichotomy", "Q": "the square class is chronon parity",
          "O": "the quarter-turn is the odd member", "V": "the spinor dichotomy", "M": "the mass–energy channel",
          "H": "the horizon is the origin's antipode"}

# the deciding check of each row: the three Subjects (C16: the sweep, which decides the four-way equivalence); the rest
# corroborate
PREDICATES = {"00:C1": "K1", "00:C3": "I1", "00:C8": "Q1", "00:C14": "O1", "00:C16": "V1", "00:C20": "M1",
              "00:C25": "H1"}

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

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


def squares(p):
    """Every square x² mod p, 0 included, by search: a set."""
    return {x * x % p for x in range(p)}


def _shells(lo, hi):
    """The primes p = 4κ + 1 in [lo, hi)."""
    return [n for n in range(lo, hi) if n % 4 == 1 and arith.is_prime(n)]


def _web(p, g):
    """The frame's web on (p, g): 2π ≡ −1, g^π ≡ −1, −π·2 ≡ 1, i² ≡ −1 (C1)."""
    k = (p - 1) // 4
    pi, i = 2 * k, (-pow(g, k, p)) % p
    return 2 * pi % p == p - 1 and pow(g, pi, p) == p - 1 and (-pi) * 2 % p == 1 and i * i % p == p - 1


# ------------------------------------------------------------------------------------------------------------
# block K: the frame's web (00:C1)
# on every frame π = 2κ and i = −g^κ: 2π ≡ −1, g^π ≡ −1, −π = 2⁻¹, i² = −1; 0 and 1 are squares and the drive is not
# (Subject.lean, frame_web).
@R.block("K", BLOCKS["K"])
def block_K():
    """Block K — the frame's web (EXACT): K1, K2."""
    # 00:C1 (p00021)
    ok, det = True, []
    for p, Om in SHELLS:
        for q in (p, Om):
            g = frame(q)[1]
            ok &= _web(q, g)
            if q < 10 ** 5:
                sq = squares(q)
                ok &= g not in sq and 0 in sq and 1 in sq and element_order(g, q) == q - 1
            else:
                ok &= pow(g, (q - 1) // 2, q) == q - 1
        det.append(f"p={p}: (κ, g, π, i) = {frame(p)}; Ω={Om}: g={frame(Om)[1]}, i={frame(Om)[3]}")
    R.check("K1", "on the three Subjects and their Carriers, with the drive g the generator-free proof builds: 2π ≡ −1, g^π ≡ −1, "
            "−π·2 ≡ 1 and i² ≡ −1 for π = 2κ, i = −g^κ; 0 and 1 are squares and g is not (by search below 10⁵, by Euler's "
            "criterion on Ω = 2 408 561)", ok, "; ".join(det))
    # K2 every prime p = 4κ + 1 below SWEEP with its drive, and every drive below SMALL: the web holds
    bad = [p for p in _shells(5, SWEEP) if not _web(p, frame(p)[1])]
    bad += [(p, g) for p in _shells(5, SMALL) for g in frames(p) if not (_web(p, g) and g not in squares(p))]
    R.check("K2", f"every prime p = 4κ + 1 below {SWEEP} with its drive, and every drive of every such p below {SMALL} (by "
            "iteration): the web closes and the drive is a nonsquare", not bad,
            f"{len(_shells(5, SWEEP))} shells; exceptions {bad[:5]}")


# ------------------------------------------------------------------------------------------------------------
# block I: the Euclidean–Lorentzian dichotomy (00:C3)
# ν = g is a nonsquare; x² − ν t² has a zero with t ≠ 0 iff ν is a square; ν = 2⁻¹·(2g), 2⁻¹ a square iff κ is even and
# 2g a square iff κ is odd (Subject.lean, signature; Field.lean, half_square_iff).
@R.block("I", BLOCKS["I"])
def block_I():
    """Block I — the Euclidean–Lorentzian dichotomy (EXACT): I1–I3."""
    # 00:C3 (p00150)
    ok, det = True, []
    for p, Om in SHELLS:
        k, g, _, _ = frame(p)
        sq = squares(p)
        iso = {nu for nu in range(p) if any(nu * t * t % p in sq for t in range(1, p))}     # x² = ν t², t ≠ 0, by search
        h = pow(2, -1, p)
        ok &= iso == sq and g not in iso and h * (2 * g) % p == g and h == 2 * k + 1
        ok &= (h in sq) == (k % 2 == 0) and (2 * g % p in sq) == (k % 2 == 1)
        det.append(f"p={p} (κ={k}): 2⁻¹={h} {'square' if h in sq else 'nonsquare'}, 2g={2 * g % p} "
                   f"{'square' if 2 * g % p in sq else 'nonsquare'}")
    R.check("I1", "on the three Subjects: the norm form x² − ν t² has a zero with t ≠ 0 exactly for the square ν (by search over every "
            "ν and t), so ν = g is non-split; ν = 2⁻¹·(2g) with 2⁻¹ = 2κ + 1, a square iff κ is even, and 2g a square iff κ is odd",
            ok, "; ".join(det))
    # I2 every prime p = 4κ + 1 below SWEEP: 2⁻¹ = 2κ + 1 is a square iff κ is even, and 2g iff κ is odd (by search)
    bad = []
    for p in _shells(5, SWEEP):
        k, g, _, _ = frame(p)
        sq = squares(p)
        if ((2 * k + 1) in sq) != (k % 2 == 0) or ((2 * g % p) in sq) != (k % 2 == 1): bad.append(p)
    R.check("I2", f"every prime p = 4κ + 1 below {SWEEP}: the classes of 2⁻¹ = 2κ + 1 and of 2g are fixed by the parity of κ (by search)",
            not bad, f"{len(_shells(5, SWEEP))} shells; exceptions {bad[:5]}")
    # I3 the Carriers: c² = 2⁻¹ = 2S + 1 is a square, S even
    ok, det = True, []
    for _, Om in SHELLS:
        S = (Om - 1) // 4
        ok &= S % 2 == 0 and (2 * S + 1) * 2 % Om == 1 and pow(2 * S + 1, (Om - 1) // 2, Om) == 1
        det.append(f"Ω={Om}: S={S}")
    R.check("I3", "on the three Carriers: S is even and c² = 2⁻¹ = 2S + 1 is a square (Euler's criterion), so η₀₀ = −c² carries the "
            "chart's class, not the frame's", ok, "; ".join(det))


# ------------------------------------------------------------------------------------------------------------
# block Q: the square class is chronon parity (00:C8)
# g^m is a square iff m is even; the inverse drive is a nonsquare; g² is a square (Subject.lean, square_class); on the
# Carrier [c²] = [2⁻¹] is even iff S is even (half_square_iff), and (ζ + ζ⁷)² = 2 for ζ⁴ = −1 (tsirelson).
@R.block("Q", BLOCKS["Q"])
def block_Q():
    """Block Q — the square class is chronon parity (EXACT): Q1–Q3."""
    # 00:C8 (p00028)
    ok, det = True, []
    for p, _ in SHELLS:
        _, g, _, _ = frame(p)
        sq = squares(p)
        par = all((pow(g, m, p) in sq) == (m % 2 == 0) for m in range(p - 1))
        ginv = pow(g, -1, p)
        ok &= par and ginv not in sq and g * g % p in sq
        det.append(f"p={p}: g={g}, g⁻¹={ginv}")
    R.check("Q1", "on the three Subjects: g^m is a square iff m is even, for every m < p − 1 (by search); the inverse drive g⁻¹ is a "
            "nonsquare and the registered transport g² a square", ok, "; ".join(det))
    # Q2 every prime Ω = 4S + 1 below SWEEP: [c²] = [2S + 1] is the even class iff S is even
    bad = [Om for Om in _shells(5, SWEEP) if ((2 * ((Om - 1) // 4) + 1) in squares(Om)) != (((Om - 1) // 4) % 2 == 0)]
    R.check("Q2", f"every prime Ω = 4S + 1 below {SWEEP}: c² = 2⁻¹ = 2S + 1 is a square iff S is even (by search)", not bad,
            f"{len(_shells(5, SWEEP))} charts; exceptions {bad[:5]}")
    # Q3 the Tsirelson square on the Carriers: ζ of order eight, (ζ + ζ⁷)² = 2
    ok, det = True, []
    for _, Om in SHELLS:
        z = octant(Om)
        ok &= z is not None and pow(z, 4, Om) == Om - 1 and tsirelson(z, Om) == 2
        det.append(f"Ω={Om}: ζ={z}")
    R.check("Q3", "on the three Carriers: ζ = a^((Ω−1)/8) has ζ⁴ = −1 and (ζ + ζ⁷)² = 2, the two-way symmetrisation √2", ok,
            "; ".join(det))


# ------------------------------------------------------------------------------------------------------------
# block O: the quarter-turn is the odd member of the ±√−1 pair (00:C14)
# e^{jπ} := (g^j)^{j·2κ} = (−1)^j; the roots h, −h of −1 have representatives of opposite parity, so e^{hπ} = −1 exactly
# on the odd one; the inverse drive is a frame with quarter-turn −i; every frame is g^u with u odd, its quarter-turn i
# when u ≡ 1 (mod 4) and −i when u ≡ 3, and the parity names the class (Subject.lean, quarter_turn_odd).
def _odd_member(p, g):
    k = (p - 1) // 4
    i = (-pow(g, k, p)) % p
    roots = quarter_turns(p)
    ok = all(euler(g, j, p) == (1 if j % 2 == 0 else p - 1) for j in range(p))
    ok &= len(roots) == 2 and roots[0] % 2 != roots[1] % 2
    ok &= all((euler(g, h, p) == p - 1) == (h % 2 == 1) for h in roots)
    gi = pow(g, -1, p)
    ok &= element_order(gi, p) == p - 1 and (-pow(gi, k, p)) % p == (p - i) % p
    for g2 in frames(p):
        u = chirality(g, g2, p)
        i2 = (-pow(g2, k, p)) % p
        ok &= u is not None and u % 2 == 1 and (i2 == i) == (u % 4 == 1) and (i2 == (p - i) % p) == (u % 4 == 3)
        ok &= ((i2 % 2) == (i % 2)) == (u % 4 == 1)
    return ok


@R.block("O", BLOCKS["O"])
def block_O():
    """Block O — the quarter-turn is the odd member (EXACT): O1, O2."""
    # 00:C14 (p00034)
    ok, det = True, []
    for p, _ in SHELLS:
        k, g, _, i = frame(p)
        ok &= _odd_member(p, g)
        odd = next(h for h in quarter_turns(p) if h % 2 == 1)
        det.append(f"p={p}: i={i}, the odd member {odd}, {len(frames(p))} frames")
    R.check("O1", "on the three Subjects: e^{jπ} = (g^j)^{2κj} = (−1)^j for every lift j < p; the roots of −1 have opposite parity and "
            "e^{hπ} = −1 exactly on the odd one; the inverse drive is a frame with quarter-turn −i; every frame g' = g^u has u "
            "odd, quarter-turn i iff u ≡ 1 (mod 4), −i iff u ≡ 3, and the same parity as i iff u ≡ 1", ok, "; ".join(det))
    # O2 every prime p = 4κ + 1 below SMALL, every drive as the reference frame
    bad = [(p, g) for p in _shells(5, SMALL) for g in frames(p)[:4] if not _odd_member(p, g)]
    R.check("O2", f"every prime p = 4κ + 1 below {SMALL}, the first four drives each as the reference frame: the same clauses", not bad,
            f"{len(_shells(5, SMALL))} shells; exceptions {bad[:5]}")


# ------------------------------------------------------------------------------------------------------------
# block V: the spinor dichotomy (00:C16)
# κ odd iff v₂(p − 1) = 2 iff the fold (r, s) ↦ iʳ (g⁴)ˢ is injective on C₄ × C_κ (and then onto F_p^×) iff
# 3κr + 4s ≡ 1 (mod 4κ) is solvable (Subject.lean, spinor); the shared 2-part 2^m, m = min(v₂(p−1), v₂(Ω−1)), the cover
# degree 2^{v₂(Ω−1)−m}, and the Carrier's 2-part 8 iff S ≡ 2 (mod 4) (two_part).
@R.block("V", BLOCKS["V"])
def block_V():
    """Block V — the spinor dichotomy (EXACT): V1–V3."""
    # 00:C16 (p00151)
    bad, odd = [], 0
    for p in _shells(5, SWEEP):
        k, g, _, _ = frame(p)
        img = fold_image(p, g)
        inj, onto = len(set(img)) == 4 * k, set(img) == set(range(1, p))
        odd += k % 2
        if not ((k % 2 == 1) == ((p - 1) % 8 != 0) == inj == bool(fold_solutions(k)) and (inj <= onto)): bad.append(p)
    R.check("V1", f"every prime p = 4κ + 1 below {SWEEP}: κ odd ⟺ 8 ∤ p − 1 ⟺ the fold iʳ (g⁴)ˢ, r < 4, s < κ, is injective (by "
            "listing its 4κ values) ⟺ 3κr + 4s ≡ 1 (mod 4κ) has a solution (by search); an injective fold is onto F_p^×", not bad,
            f"{len(_shells(5, SWEEP))} shells, {odd} with κ odd; exceptions {bad[:5]}")
    # V2 the three pairs: the 2-parts
    ok, det = True, []
    for p, Om in SHELLS:
        a, b, m, cover, car = two_parts(p, Om)
        S = (Om - 1) // 4
        both = (p - 1) % 2 ** m == 0 and (Om - 1) % 2 ** m == 0
        ok &= both and not ((p - 1) % 2 ** (m + 1) == 0 and (Om - 1) % 2 ** (m + 1) == 0) and 2 ** m * cover == car
        ok &= (car == 8) == (S % 4 == 2) and a == 2 and ((p - 1) // 4) % 2 == 1
        det.append(f"(p, Ω)=({p}, {Om}): v₂ = {a}, {b}; shared C_{2 ** m}, cover degree {cover}, Carrier 2-part {car}, S mod 4 = {S % 4}")
    R.check("V2", "on the three pairs (κ = 3, 43, 343, all odd): 2^m divides p − 1 and Ω − 1 and 2^(m+1) not both, m = min of the "
            "2-adic valuations; the shared order 2^m times the cover degree is the Carrier's 2-part, 8 exactly when S ≡ 2 (mod 4)",
            ok, "; ".join(det))
    # V3 every pair of primes ≡ 1 (mod 4) below 600: the same arithmetic
    bad, n = [], 0
    for p in _shells(5, 600):
        for Om in _shells(5, 600):
            a, b, m, cover, car = two_parts(p, Om)
            n += 1
            if not ((p - 1) % 2 ** m == 0 and (Om - 1) % 2 ** m == 0 and 2 ** m * cover == car
                    and not ((p - 1) % 2 ** (m + 1) == 0 and (Om - 1) % 2 ** (m + 1) == 0)
                    and (car == 8) == (((Om - 1) // 4) % 4 == 2)): bad.append((p, Om))
    R.check("V3", "every pair of primes ≡ 1 (mod 4) below 600: the shared 2-part, the cover degree and the Carrier's 2-part as in V2",
            not bad, f"{n} pairs; exceptions {bad[:5]}")


# ------------------------------------------------------------------------------------------------------------
# block M: the mass–energy channel (00:C20)
# on a prime p with h² = −1: x^{p+1} = 1 iff x = ±1, x^{2(p+1)} = 1 iff x ∈ Q₄ = {±1, ±h}, h^{p+1} = −1 (Subject.lean,
# channel); the Carrier instance 78^58 = 89 = h on Ω = 233 (channel_233).
@R.block("M", BLOCKS["M"])
def block_M():
    """Block M — the mass–energy channel (EXACT): M1–M3."""
    # 00:C20 (p00040)
    ok, det = True, []
    for p, _ in SHELLS:
        h = quarter_turn(p)
        sign, q4 = channel(p, h)
        ok &= sign == [1, p - 1] and sorted(q4) == sorted({1, p - 1, h, p - h}) and pow(h, p + 1, p) == p - 1
        det.append(f"p={p}: h={h}, Q₄={sorted(q4)}")
    for p in (13, 173):                                         # the same inside F_{p²}, by search over every element
        K = Ext(p, frame(p)[1])
        h = quarter_turn(p)
        units = [z for z in K.elements() if z != (0, 0)]
        base = [z for z in units if K.pow(z, p - 1) == (1, 0)]
        boost = {z for z in units if K.pow(z, p + 1) == (1, 0)}
        cover = {z for z in units if K.pow(z, 2 * (p + 1)) == (1, 0)}
        ok &= sorted(base) == [(x, 0) for x in range(1, p)] and len(boost) == p + 1 and len(cover) == 2 * (p + 1)
        ok &= set(base) & boost == {(1, 0), (p - 1, 0)} and set(base) & cover == {(1, 0), (p - 1, 0), (h, 0), (p - h, 0)}
        ok &= K.norm((h, 0)) == p - 1
    R.check("M1", "on the three Subjects with h = ħ: the nonzero x with x^(p+1) = 1 are ±1 and those with x^(2(p+1)) = 1 are Q₄ = {±1, ±h} "
            "(by search), h^(p+1) = −1; inside F_{p²} for p = 13 and 173 (every element): C_{p−1} = F_p^×, it meets C_{p+1} in ±1 "
            "and C_{2(p+1)} in Q₄, and N(h) = h² = −1", ok, "; ".join(det))
    # M2 the Carrier instance
    R.check("M2", "the Carrier instance on Ω = 233: 78^58 = 89 and 89² = −1 (38:A4)", pow(78, 58, 233) == 89 and 89 * 89 % 233 == 232,
            f"78^58 mod 233 = {pow(78, 58, 233)}")
    # M3 every prime p = 4κ + 1 below SWEEP: the channel
    bad = []
    for p in _shells(5, SWEEP):
        h = quarter_turn(p)
        sign, q4 = channel(p, h)
        if not (sign == [1, p - 1] and sorted(q4) == sorted({1, p - 1, h, p - h})): bad.append(p)
    R.check("M3", f"every prime p = 4κ + 1 below {SWEEP}: the sign ±1 and Q₄ as in M1 (by search)", not bad,
            f"{len(_shells(5, SWEEP))} shells; exceptions {bad[:5]}")


# ------------------------------------------------------------------------------------------------------------
# block H: the horizon is the origin's antipode on the boost torus (00:C25)
# for w² = ν a nonsquare, the torsor map P ↦ u_P/ū_P from P¹(F_p) to C_{p+1} is an equivariant bijection, origin ↦ 1,
# horizon ↦ −1; ±1 are the rational norm-one elements; w acts as q ↦ ν/q and swaps origin and horizon; the additive
# antipode is no residue, the seam 2κ + 1 = 2⁻¹ = −2κ (Subject.lean, horizon_antipode).
def _horizon(p, nu, boosts=None):
    K = Ext(p, nu)
    P1 = projective_line(p)
    tors = {P: torsor(P, nu, p) for P in P1}
    torus = set(K.norm_one()) if p < 2000 else None
    ok = len(set(tors.values())) == p + 1 and all(K.norm(t) == 1 for t in tors.values())
    if torus is not None: ok &= set(tors.values()) == torus
    ok &= tors[(0, 1)] == (1, 0) and tors[(1, 0)] == (p - 1, 0)
    vs = boosts if boosts is not None else [z for z in K.elements() if K.norm(z) != 0]
    for v in vs:
        rv = K.mul(K.scalar(pow(K.norm(v), -1, p)), K.mul(v, v))
        ok &= all(tors[boost_act(v, P, nu, p)] == K.mul(rv, tors[P]) for P in P1)
    w = (0, 1)
    ok &= all(boost_act(w, (x, 1), nu, p) == ((nu * pow(x, -1, p) % p, 1) if x else (1, 0)) for x in range(p))
    ok &= boost_act(w, (0, 1), nu, p) == (1, 0) and boost_act(w, (1, 0), nu, p) == (0, 1)
    if torus is not None:
        ok &= {t for t in torus if K.mul(t, t) == (1, 0)} == {(1, 0), (p - 1, 0)}
        ok &= {t for t in torus if t[1] == 0} == {(1, 0), (p - 1, 0)}
    k = (p - 1) // 4
    ok &= [s for s in range(p) if 2 * s % p == 0] == [0] and 2 * (2 * k + 1) % p == 1 and (-2 * k) % p == 2 * k + 1
    return ok


@R.block("H", BLOCKS["H"])
def block_H():
    """Block H — the horizon is the origin's antipode (EXACT): H1–H3."""
    # 00:C25 (p00139)
    nus13 = [nu for nu in range(1, 13) if nu not in squares(13)]
    ok = all(_horizon(13, nu) for nu in nus13)
    nu173 = [arith.nonresidue(173), frame(173)[1]]
    for nu in nu173:
        K = Ext(173, nu)
        sample = [z for z in K.elements() if K.norm(z) != 0][::97]
        ok &= _horizon(173, nu, sample)
    R.check("H1", "the torsor map P ↦ u_P/ū_P (u_P = ν y + x w) bijects P¹(F_p) onto the norm-one torus C_{p+1}, origin ↦ 1 and horizon ↦ −1, "
            "and is equivariant, tors(v·P) = (v/v̄)·tors(P); ±1 are the torus's rational elements and its only square roots of 1; w "
            "acts as q ↦ ν/q and swaps origin and horizon; 2s = 0 forces s = 0 and 2κ + 1 = 2⁻¹ = −2κ. On p = 13 for every "
            "nonsquare ν and every boost; on p = 173 for ν the least nonsquare and ν = g, every 97th boost", ok,
            f"p=13: {len(nus13)} values of ν; p=173: ν ∈ {nu173}, {len(sample)} boosts")
    # H2 the Subject 1373, ν the least nonsquare: the bijection, the two points, the swap, 40 boosts
    p, nu = 1373, arith.nonresidue(1373)
    K = Ext(p, nu)
    boosts = [(a, b) for a in range(0, p, 97) for b in range(1, p, 211) if K.norm((a, b)) != 0][:40]
    R.check("H2", f"the Subject p = 1373 with ν = {nu}: the torsor map is a bijection onto p + 1 norm-one elements with origin ↦ 1 and "
            "horizon ↦ −1, equivariant under 40 boosts, w swaps origin and horizon", _horizon(p, nu, boosts), f"{len(boosts)} boosts")
    # H3 every prime p = 4κ + 1 below SMALL, ν the least nonsquare: the full statement on every boost below 100, a sample above
    bad = []
    for p in _shells(5, SMALL):
        nu = arith.nonresidue(p)
        Kp = Ext(p, nu)
        vs = None if p < 100 else [z for z in Kp.elements() if Kp.norm(z) != 0][::max(1, p // 3)]
        if not _horizon(p, nu, vs): bad.append(p)
    R.check("H3", f"every prime p = 4κ + 1 below {SMALL} with ν the least nonsquare: the same clauses (every boost below 100, a sample "
            "of boosts above)", not bad, f"{len(_shells(5, SMALL))} shells; exceptions {bad[:5]}")


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)