"""p07_spacetime — the ledger file of 7-spacetime (the verification package of 31 October 2026).

"Emergent Lorentzian Space-Time over Finite Holographic Substrate" (Akhtman, 2026). The paper's predicate ledger is
docs/7-spacetime/7-spacetime-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 six blocks. Each check names the predicate(s) it witnesses
(LEDGER) under a `# 7:XN (<key>)` marker on the check that decides it (PREDICATES). The carried rows of block A keep
their origin keys (the master's 00:, 3-causality's 3:, 38-s13's 38:, 21-gravity's 21:) and are decided here again on
the themes: the frame and the signature (frc/subject.py), the quadratic forms and their counts (frc/shell.py), the
Hopf section, the frame triple, the frame group and its one form (frc/projective.py), the pair's drift and joint cycle
(frc/subject.py), completeness as primality (frc/foundation.py), the retarded flow (frc/covering.py), the single
arrow (frc/drift.py), the Carrier register's residues (frc/carrier.py), the domain of temperature (frc/shell.py's domain
lattice) and the weak-acceleration floor (an identity of exact rationals; the confrontation with the fitted value is
21-gravity's chart check). Since 6 November 2026 the three last rows cite their origin's Lean declarations (the paper's
reports/lean-a31-20261106/): the register (Keys/Carrier), the domain identities (the domain theme's Keys/Domain) and the
floor's identity in the core with its number on Mathlib. The paper's own rows are decided on the register square and the finite Lorentz group of
frc/projective.py (7-spacetime's section): the determinant of the Hermitian matrix, the congruence of SL₂(𝔽_{p²}) with
its kernel ±I and its image of index four, the cone, the two four-dimensional classes, the similitude, the fibration,
the class equation, the drive and the lift, the antipode at the half step, the three exclusions of the arrow, the
one-directional drift, the record's second law and, with the Carrier register of frc/carrier.py, the floor as the Carrier's
temperature. Everything is exact (gate G09); the SI readings in the details of A31 and P2 come through the chart theme
(frc/chart.py: floor, de_sitter_temperature). The Lean side is lean/FrcCore/Theme/Lorentz.lean (the projective theme)
with Theme/Spin.lean, Theme/Projective.lean, Theme/Hopf.lean, Theme/Pair.lean and Theme/Register.lean behind it, and lean/FrcMathlib/Theme/
Lorentz.lean for the isotropy of every three-dimensional subspace (Chevalley–Warning, D5), with Theme/Carrier.lean,
Theme/Domain.lean and Theme/Drift.lean behind the carried A33, A32 and A31 and lean/FrcMathlib/Theme/Chart.lean behind A31's
number; the paper modules are
lean/FrcCore/Spacetime.lean and lean/FrcMathlib/Spacetime.lean, the certificates lean/FrcCore/Ledgers/P07Spacetime.lean
and lean/FrcMathlib/Ledgers/P07Spacetime.lean.

    python3 -m frc.ledgers.p07_spacetime        every block, the census; exit 1 if a check fails (≈ 90 s: the one
                                                enumeration of SL₂(𝔽₁₆₉), 4 826 640 matrices, decides C2, D1 and F3)
    python3 -m frc.ledgers.p07_spacetime C      one block (A to F)
    from frc.ledgers.p07_spacetime import R; R.predicate("7:C2")    one predicate: its blocks run once per session

Blocks:  A  the inputs carried                         EXACT   (7:A4, A6, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A21, A23, A24, A25, A26, A28, A31, A32, A33)
         B  the register and the shell                 EXACT   (7:B1, B4, B5, B6)
         C  the forms, the cone and the fibration      EXACT   (7:C1, C2, C3, C4, C5, C6, C7, C8, C9, C10, X1, X2, X5)
         D  time and the antipode                       EXACT   (7:D1, D3, D4, D5, D6, X4)
         F  the arrow                                  EXACT   (7:F1, F3, F4, F5, X6)
         P  the predictions                            EXACT   (7:P1, P2)

The instances are the corpus's three laboratory pairs: the Subjects 𝔽₁₃ (κ = 3), 𝔽₁₇₃ (κ = 43) and 𝔽₁₅₄₉ (κ = 387),
each with the drive g = 2 (a generator and a nonsquare, p ≡ 5 mod 8) and its quadratic extension, inside the Carriers
𝔽₂₃₃, 𝔽₃₀₀₈₉ and 𝔽₂₄₀₈₅₆₁ (38-s13, 39-s173, 37-sim). The identities, the counts by formula and the drift run on all three
(SHELLS, PAIRS); the O(p²) searches on 𝔽₁₃ and 𝔽₁₇₃ (MID); the complete enumerations of SL₂(𝔽_{p²}), PGL₂(𝔽_p) and 𝔽_p⁴
on 𝔽₁₃ alone (ENUM). The notebook frc/ledgers/p07_spacetime.ipynb runs one predicate per cell, the cell's id its key
(gate G13).
"""
import sys
from fractions import Fraction
from math import gcd

from frc import arith
from frc import carrier as CA
from frc import chart as CH
from frc import covering as CV
from frc import drift as D
from frc import foundation as FO
from frc import projective as PJ
from frc import shell as SH
from frc import subject as SB
from frc.extension import Ext
from frc.registry import Registry

# ---- generated by ci/make_ledgers.py from docs/7-spacetime/7-spacetime-ledger.json; edit the ledger, not this table ----
PAPER = "7-spacetime"
KEYS = {"A1": "p03002", "A2": "p07001", "A3": "p07002", "A4": "p00021", "A5": "p00025", "A6": "p00150", "A7": "p03005", "A8": "p03008", "A9": "p03011", "A10": "p03013", "A11": "p00190", "A12": "p38050", "A13": "p00152", "A14": "p00183", "A15": "p00139", "A16": "p00028", "A17": "p00042", "A18": "p00044", "A19": "p00182", "A20": "p00198", "A21": "p38053", "A22": "p07041", "A23": "p00162", "A24": "p38044", "A25": "p38054", "A26": "p38016", "A27": "p00140", "A28": "p21018", "A29": "p00008", "A30": "p00153", "A31": "p21052", "A32": "p00032", "A33": "p00165", "A34": "p07053", "B1": "p07003", "B2": "p07004", "B3": "p07038", "B4": "p07042", "B5": "p07049", "B6": "p07050", "B7": "p07055", "C1": "p07005", "C2": "p07006", "C3": "p07007", "C4": "p07008", "C5": "p07009", "C6": "p07010", "C7": "p07031", "C8": "p07032", "C9": "p07040", "C10": "p07051", "D1": "p07011", "D3": "p07013", "D4": "p07014", "D5": "p07015", "D6": "p07033", "E1": "p07043", "F1": "p07044", "F2": "p07045", "F3": "p07046", "F4": "p07047", "F5": "p07052", "F6": "p07056", "X1": "p07020", "X2": "p07021", "X4": "p07023", "X5": "p07024", "X6": "p07048", "P1": "p07026", "P2": "p07054"}       # every row of the ledger: its label and its accession key
LEAN = {"A4": "core", "A6": "core", "A8": "core", "A9": "core", "A10": "core", "A11": "core", "A12": "core", "A13": "core", "A14": "core", "A15": "core", "A16": "core", "A17": "core", "A21": "core", "A23": "core", "A24": "core", "A25": "core", "A26": "core", "A28": "core", "A31": "core, ml", "A32": "core", "A33": "core", "B1": "core", "B4": "core", "B5": "core", "B6": "core", "C1": "core", "C2": "core", "C3": "core", "C4": "core", "C5": "core", "C6": "core", "C7": "core", "C8": "core", "C9": "core", "C10": "core", "D1": "core", "D3": "core", "D4": "core", "D5": "ml", "D6": "core", "F1": "core", "F3": "core", "F4": "core", "F5": "core", "X1": "core", "X2": "core", "X4": "core", "X5": "core", "X6": "core", "P1": "core", "P2": "core"}       # 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 (D5 is proved on Mathlib for every shell, Chevalley–Warning, and searched here at p = 13)

SHELLS = [(13, 2), (173, 2), (1549, 2)]       # (p, g): the three Subjects with the drive g = 2, a generator and a nonsquare; ν = g
MID = SHELLS[:2]                              # the O(p²) searches: 𝔽₁₃ and 𝔽₁₇₃
ENUM = SHELLS[:1]                             # the complete enumerations (p³ and p⁴): 𝔽₁₃
PAIRS = [(13, 233), (173, 30089), (1549, 2408561)]   # the laboratory pairs (Subject, Carrier) of 38-s13, 39-s173 and 37-sim
P, G, OM = 13, 2, 233
ADMISSIBLE = [(p, Om) for p in range(5, 200) for Om in range(p * p + 1, 3000)
              if SB.admissible(p, Om)["p_prime"] and Om % 48 == 41 and arith.is_prime(Om) and all(SB.admissible(p, Om).values())]

# The paper's predicate ledger (its appendix, predicates cited as 7:XN): the predicate(s) each check witnesses.
LEDGER = {
    "A4": "7:A4", "A6": "7:A6, 7:A10", "A8": "7:A8, 7:A9", "A11": "7:A11, 7:A12", "A13": "7:A13, 7:A14", "A15": "7:A15",
    "A16": "7:A16", "A17": "7:A17", "A21": "7:A21, 7:A24, 7:A25", "A23": "7:A23", "A26": "7:A26", "A28": "7:A28",
    "A31": "7:A31", "A32": "7:A32", "A33": "7:A33",
    "B1": "7:B1", "B4": "7:B4", "B5": "7:B5", "B6": "7:B6",
    "C1": "7:C1", "C2": "7:C2, 7:X4", "C3": "7:C3, 7:C4", "C5": "7:C5, 7:X1", "C6": "7:C6, 7:X5", "C7": "7:C7",
    "C8": "7:C8", "C9": "7:C9, 7:X2", "C10": "7:C10",
    "D1": "7:D1", "D3": "7:D3", "D4": "7:D4", "D5": "7:D5", "D6": "7:D6",
    "F1": "7:F1", "F3": "7:F3, 7:X6", "F4": "7:F4", "F5": "7:F5",
    "P1": "7:P1", "P2": "7:P2",
}

BLOCK = {"A": "the inputs carried",
         "B": "the register and the shell",
         "C": "the forms, the cone and the fibration",
         "D": "time and the antipode",
         "F": "the arrow",
         "P": "the predictions"}

# the deciding check of each witnessed predicate
PREDICATES = {
    "7:A4": "A4", "7:A6": "A6", "7:A10": "A6", "7:A8": "A8", "7:A9": "A8", "7:A11": "A11", "7:A12": "A11", "7:A13": "A13",
    "7:A14": "A13", "7:A15": "A15", "7:A16": "A16", "7:A21": "A21", "7:A24": "A21", "7:A25": "A21", "7:A23": "A23", "7:A26": "A26",
    "7:A28": "A28", "7:A17": "A17", "7:A31": "A31", "7:A32": "A32", "7:A33": "A33",
    "7:B1": "B1", "7:B4": "B4", "7:B5": "B5", "7:B6": "B6",
    "7:C1": "C1", "7:C2": "C2", "7:X4": "C2", "7:C3": "C3", "7:C4": "C3", "7:C5": "C5", "7:X1": "C5", "7:C6": "C6",
    "7:X5": "C6", "7:C7": "C7", "7:C8": "C8", "7:C9": "C9", "7:X2": "C9", "7:C10": "C10",
    "7:D1": "D1", "7:D3": "D3", "7:D4": "D4", "7:D5": "D5", "7:D6": "D6",
    "7:F1": "F1", "7:F3": "F3", "7:X6": "F3", "7:F4": "F4", "7:F5": "F5",
    "7:P1": "P1", "7:P2": "P2",
}

R = Registry("7", "spacetime", LEDGER, PREDICATES, sources=[__file__])
Fr = Fraction
_IMAGE = {}                                   # the one enumeration of SL₂(𝔽_{p²}) per shell, shared by C2, D1 and F2


def image(p, nu):
    if p not in _IMAGE: _IMAGE[p] = PJ.congruence_image(p, nu)
    return _IMAGE[p]


def norm_one_order(nu, p):
    """|{(t, x) : −ν t² + x² = 1}|: the norm-one group of the plane form, C_{p+1} for ν a nonsquare, C_{p−1} for a square."""
    return sum(1 for t in range(p) for x in range(p) if (-nu * t * t + x * x) % p == 1)


# ---- block A: the inputs carried (7:A4, A6, A8–A17, A21, A23–A26, A28, A31–A33) -------------------------------------------
@R.block("A", BLOCK["A"])
def block_A():
    ok, det = True, []
    for p, g in SHELLS:
        k, _, pi, _ = SB.frame(p); i = (-pow(g, k, p)) % p
        ok &= p == 4 * k + 1 and pi == 2 * k and arith.is_primitive_root(g, p) and not SH.is_square(g, p)
        ok &= pow(i, 2, p) == p - 1 and (-pow(g, k, p)) % p == pow(g, 3 * k, p)
        det.append(f"p={p}: κ={k}, π={pi}, g={g} generator and nonsquare, i=−g^κ={(-pow(g, k, p)) % p} with i²=−1")
    # 7:A4 (p00021)
    R.check("A4", "the frame, Subject-only: on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉ the drive g = 2 is a generator of 𝔽_p^× and a nonsquare, the shell is p = 4κ + 1 with π = 2κ, and the quarter-turn i = −g^κ = g^{3κ} squares to −1", ok, "; ".join(det))
    ok, det = True, []
    for p, g in SHELLS:
        ns = norm_one_order(g, p); sq = norm_one_order(g * g % p, p)
        ok &= ns == p + 1 and sq == p - 1
        det.append(f"p={p}: |N¹(−g t² + x²)| = {ns}, |N¹(−g² t² + x²)| = {sq}")
    for p, g in ENUM:
        ok &= all(norm_one_order(nu, p) == (p - 1 if SH.is_square(nu, p) else p + 1) for nu in range(1, p))
    # 7:A6 (p00150), 7:A10 (p03013)
    R.check("A6", "the signature is the square class of the temporal coefficient: the norm-one group of −ν t² + x² has order p + 1 (the non-split torus C_{p+1}) for ν the drive, a nonsquare, and p − 1 (the split torus C_{p−1}) for its square, on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉; for every ν of 𝔽₁₃^×", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        hyp = SH.isotropic_count((1, 1, 1, (-g * g) % p), p); ell = SH.isotropic_count((1, 1, 1, (-g) % p), p)
        ok &= hyp == p ** 3 + p * p - p and ell == p ** 3 - p * p + p
        vc = SH.value_counts((1, 1, 1, (-g) % p), p)
        sqv = sum(n for v, n in enumerate(vc) if v and SH.is_square(v, p)); nsv = sum(n for v, n in enumerate(vc) if v and not SH.is_square(v, p))
        ok &= sqv == nsv == (p - 1) * (p ** 3 + p) // 2
        # rescaling by a nonsquare exchanges the two classes, by a square fixes them: the classes are unions of value fibres
        ok &= all(vc[v] == vc[v * g * g % p] for v in range(1, p))
        det.append(f"p={p}: null {hyp} (hyperbolic), {ell} (elliptic); the non-null classes {sqv} = {nsv}")
    for p, g in SHELLS:
        nulls, _ = PJ.null_count_by_fibres(p, g)
        ok &= nulls == p ** 3 - p * p + p
        det.append(f"p={p}: elliptic null count by the binary fibres {nulls} = p³ − p² + p")
    # 7:A8 (p03008), 7:A9 (p03011)
    R.check("A8", "the earlier classification carried: the null vectors of Q_ν = −ν t² + x² + y² + z² number p³ + p² − p for ν a square and p³ − p² + p for a nonsquare, and the two non-null classes of the elliptic form are equal, (p − 1)(p³ + p)/2 each, and invariant under rescaling by a square, enumerated on 𝔽₁₃; the elliptic count by the binary fibres on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        G_ = PJ.pgl2(p); nu = g
        facts = all(tuple(N * x % p for x in M) == PJ.mul(PJ.borel(*bor, p), PJ.boost(nu, *bst, p), p) for M in G_ for N, bor, bst in [PJ.factor(M, nu, p)])
        n, dirs, bors, bij = PJ.frame_triple(p, nu)
        ok &= facts and len(G_) == (p - 1) * p * (p + 1) and bij and n == (p + 1) * p * (p - 1)
        det.append(f"p={p}: |G| = {len(G_)} = (p+1)p(p−1), every class borel × boost, the frame triple bijective ({dirs} directions × {bors} Borel classes)")
    # 7:A11 (p00190), 7:A12 (p38050)
    R.check("A11", "the Hopf section and the frame triple: every class of PGL₂(𝔽_p) is a Borel class times a boost, G = B · T, and one direction of ℙ¹(𝔽_p) × one Borel class, (p + 1)·p(p − 1) exactly, enumerated on 𝔽₁₃", ok, "; ".join(det))
    r13 = PJ.unit(13)[0]
    so = PJ.so3(13); inv = PJ.involutions(13)
    ok = so[0] == so[1] == 2184 and so[2] == {1} and so[3] and so[4] == 2 * 2184 and inv == (1, 169)
    hw = PJ.hermitian_wJ(13, 2)[1]; sam = PJ.su2_is_sl2(13, 2)
    img = image(13, 2)
    ok &= hw and sam[0] and sam[3] == 0 and img["stabiliser"] == img["stabiliser_rational"] == img["sl2p"] == 2184
    # 7:A13 (p00152), 7:A14 (p00183)
    R.check("A13", "the frame group: PGL₂(𝔽₁₃) → SO₃(𝔽₁₃) by the adjoint action is injective with image of order 2184 = |SO₃| (|O₃| = 4368 by frames), SL₂ has one involution against PGL₂'s 169; and SU₂(𝔽₁₆₉/𝔽₁₃) = SL₂(𝔽₁₃) for the Hermitian form ηJ: every rational unimodular matrix is unitary, no non-rational sample is, and over all of SL₂(𝔽₁₆₉) the unitary matrices are exactly the 2184 rational ones", ok,
            f"so3 {so[:2]}, dets {so[2]}, |O₃| {so[4]}; sample {sam}; stabiliser {img['stabiliser']}")
    ok, det = True, []
    for p, g in SHELLS:
        K = Ext(p, g); k = (p - 1) // 4
        pts = {PJ.normal(z, p) for z in K.elements() if z != (0, 0)}
        seam = (2 * k + 1) * 2 % p == 1
        ok &= len(pts) == p + 1 and (1, 0) in pts and all(PJ.normal((x, 1), p) != (1, 0) for x in range(p)) and seam
        det.append(f"p={p}: ℙ¹ has {len(pts)} points, the antipode [1:0] no residue, 2⁻¹ = {2 * k + 1}")
    # 7:A15 (p00139)
    R.check("A15", "origin and antipode: the classes of 𝔽_{p²}^× modulo 𝔽_p^× are the p + 1 points of ℙ¹(𝔽_p), the antipode [1 : 0] among them and no residue [x : 1]; the seam 2⁻¹ = 2κ + 1, on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))
    ok = all(SH.is_square(pow(g, j, p), p) == (j % 2 == 0) for p, g in SHELLS for j in range(p - 1))
    # 7:A16 (p00028)
    R.check("A16", "the squares are the even drive steps: g^j is a square exactly when j is even, so registered transport (two chronons) is even and the one-way multiplier g odd, on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "")
    ok, det = True, []
    for p, Om in PAIRS:
        k, S_ = (p - 1) // 4, (Om - 1) // 4
        ang, per, om1, _ = SB.leak_rate(p, Om)
        L, half, _, _ = SB.joint_cycle(p, Om)
        ok &= ang == Fr(k, S_) and per == om1 == Fr(1, Om - 1) and L == 4 * k * S_ // gcd(k, S_) and half == L // 2
        ok &= SB.apsidal_bound(p, Om) == (True, True) and D.nesting_bound(p, Om)[:2] == (True, True)
        det.append(f"({p}, {Om}): κ/S = {ang}, per chronon {per}, joint cycle {L}")
    ok &= all(SB.leak_rate(p, Om)[1] == Fr(1, Om - 1) for p, Om in ADMISSIBLE)
    ok &= all(SB.joint_cycle(p, Om)[0] == SB.least_return(p, Om) for p, Om in ADMISSIBLE[:40])
    ok &= all(SB.apsidal_bound(p, Om) == (True, True) for p, Om in ADMISSIBLE) and all(SB.apsidal_bound(p, Om) == (False, False) for p, Om in ((53, 157), (13, 157), (173, 233)))
    # 7:A21 (p38053), 7:A24 (p38044), 7:A25 (p38054)
    R.check("A21", f"the pair's arithmetic carried: the per-chronon drift rate is 1/(Ω − 1) on every admissible pair below (200, 3000) ({len(ADMISSIBLE)} of them) and on the three laboratory pairs, 1/232, 1/30088 and 1/2408560, with κ/S = 3/58, 43/7522 and 387/602140 per revolution; the joint cycle is lcm(p − 1, Ω − 1): 696, 1 293 784 and 932 112 720; and the apsidal bound κ/S < 1/(√Ω + 1) holds exactly on the nested pairs p² < Ω and fails on (53, 157), (13, 157), (173, 233)", ok,
            "; ".join(det))
    bad = [q for q in range(2, 260) if FO.is_complete(q) != arith.is_prime(q)]
    ok = not bad and FO.is_complete(233) and not FO.zero_divisors(233) and FO.zero_divisors(234) and not FO.is_complete(234)
    ok &= all(arith.is_prime(p) and arith.is_prime(Om) and p * p < Om and (p - 1) % 4 == 0 and (Om - 1) % 4 == 0 for p, Om in PAIRS)
    # 7:A23 (p00162)
    R.check("A23", "completeness is primality: for every count 2 ≤ q < 260 the residues of q have no proper nonzero ideal (every nonzero residue invertible) exactly when q is prime; 𝔽₂₃₃ is a field with no zero divisors, ℤ₂₃₄ is not; the three laboratory pairs are prime Subjects nested in prime Carriers, p² < Ω, both of the form 4n + 1", ok, f"exceptions {bad}")
    ok = all(CV.tick(232, k, k) == 0 and CV.tick(232, k, 116 + k) == 116 for k in range(232))
    ok &= all((CV.tick(232, k, b) + b) % 232 == k for b in range(232) for k in range(13))
    ok &= all(CV.tick(n, k, b) == (k - b) % n for n in (12, 24, 232, 464) for k in range(n) for b in range(n))
    # 7:A26 (p38016)
    R.check("A26", "one retarded flow law, carried from the laboratory: the row k at clock b stands at (k − b) mod 232 on the Carrier cycle C₂₃₂, the same count on C₁₂, C₂₄, C₂₃₂ and C₄₆₄, and the count returns the row at every clock state", ok, "")
    arrows = [D.single_arrow(p, g) for p, g in MID]
    ok = all(a[0] for a in arrows) and all(a[1] == p + 1 for a, (p, _) in zip(arrows, MID))
    # 7:A28 (p21018)
    R.check("A28", "the drive has a single arrow: on 𝔽₁₆₉ and 𝔽_{173²} the Frobenius is the conjugation on every element, on the norm-one circle the conjugate is the inverse and the drive generator's conjugate orbit is its orbit reversed, and the conjugation fixes ±1 alone — a time-reversed clock is the Frobenius branch, not a step of the drive", ok,
            "; ".join(f"p={p}: circle of order {a[1]}, fixed {a[2]}" for a, (p, _) in zip(arrows, MID)))
    # time is the drive (00:D1, a theorem on the author's word of 1 November 2026): the drive x ↦ gx is transitive on 𝔽_p^× (one orbit, so the
    # register alone registers no duration), the register returns after 4κ chronons, and the pair's chart count is injective on the registrable
    # depth p² < Ω − 1 (frc/subject.py's drift_depth), so a registered duration is the count of drive steps
    ok, det = True, []
    for p, g in SHELLS:
        orbit = set(); x = 1
        for _ in range(p - 1): orbit.add(x); x = (x * g) % p
        ok &= orbit == set(range(1, p)) and x == 1 and pow(g, (p - 1) // 2, p) == p - 1
    for p, Om in PAIRS + [(13, 181)]:
        below, inj, d, cyc = SB.drift_depth(p, Om)
        ok &= below and inj and d % 2 == 1 and cyc % 2 == 0 and d <= cyc - 1
        det.append(f"({p}, {Om}): p²={d} < Ω−1={cyc}, the counts 0..{d} distinct")
    ok &= all(SB.drift_depth(p, Om)[0] and SB.drift_depth(p, Om)[1] for p, Om in ADMISSIBLE)
    # the Carrier register (00:B7): on the three Carriers Ω = 4S + 1 the register {S, Ω, c, ħ, G, k_B} of frc/carrier.py is generator-free
    # in S, with G = 2S = −c², 2c² ≡ 1, ħ² ≡ −1, k_B² ≡ −2 and k_B c ≡ ħ (|k_B| = ħ/c); G exact, the rest up to sign
    ok, det = True, []
    for p, Om in PAIRS:
        r = CA.register((Om - 1) // 4); S, c, hbar, kB, G = r["S"], r["c"], r["hbar"], r["kB"], r["G"]
        ok &= Om == 4 * S + 1 and G == 2 * S and (G + c * c) % Om == 0 and 2 * c * c % Om == 1 and hbar * hbar % Om == Om - 1
        ok &= kB * kB % Om == Om - 2 and kB * c % Om == hbar and (Om - kB) * c % Om == Om - hbar
        det.append(f"Ω={Om}: S={S}, G={G}=−c², c={c}, ħ={hbar}, k_B={kB}, k_B c ≡ ħ")
    # 7:A33 (p00165)
    R.check("A33", "the Carrier register is generator-free in the capacity, carried from the master: on 𝔽₂₃₃, 𝔽₃₀₀₈₉ and 𝔽₂₄₀₈₅₆₁ the register {S, Ω, c, ħ, G, k_B} satisfies G = 2S = −c², 2c² ≡ 1, ħ² ≡ −1, k_B² ≡ −2 and k_B c ≡ ħ, so |k_B| = ħ/c; G is exact and the rest hold up to sign", ok, "; ".join(det))
    # the domain of temperature (00:C12, 10-dimensions): in the domain lattice of frc/shell.py, [Θ] = [E][k_B]⁻¹ = [L][T]⁻², flag-free; the
    # Unruh combination ħa/(2π c k_B) has the temperature domain; the classical M-L-T-Θ exponents of every listed quantity lift to its domain
    ok = SH.TEMP == SH.ACCEL == SH.dom(SH.L, (SH.T, -2)) and SH.TEMP[2] == 0 and SH.KB == SH.dom(SH.HBAR, (SH.SPEED, -1))
    ok &= SH.dom(SH.HBAR, SH.ACCEL, (SH.SPEED, -1), (SH.KB, -1)) == SH.TEMP and SH.dom(SH.ENERGY, (SH.KB, -1)) == SH.TEMP
    ok &= all(SH.classical(*SH.CLASSICAL[q]) == SH.DOMAINS[q] for q in SH.CLASSICAL) and SH.classical(0, 0, 0, 1) == SH.ACCEL and SH.classical(1, 0, 0, 0) == SH.MASS
    # 7:A32 (p00032)
    R.check("A32", "temperature carries the acceleration domain, carried from the master: in the lifted domain lattice [Θ] = [E][k_B]⁻¹ = [L][T]⁻² with no flag, the Unruh combination ħa/(2π c k_B) has the temperature domain, and the classical M-L-T-Θ exponents of the thirteen listed quantities lift to their domains, with Θ ↦ L T⁻² and M ↦ Iq L⁻² T; neither mass nor temperature is primitive", ok,
            f"[Θ] = {SH.TEMP} = [a]; [k_B] = {SH.KB}; {len(SH.CLASSICAL)} quantities recovered")
    # the weak-acceleration floor (21:P3): a₀ = c/T_H = cH₀/τ with T_H = τ/H₀ the drive period and τ the full cycle, an identity of exact
    # rationals in every value of the symbols; the SI value at H₀ = 67.4 km s⁻¹ Mpc⁻¹ and the fitted 1.20 ± 0.24 are the detail [chart]
    ok = True
    for c, H, tau in ((Fr(29979, 100), Fr(218, 100), Fr(628, 100)), (Fr(1), Fr(1), Fr(1)), (Fr(7, 3), Fr(5, 11), Fr(44, 7))):
        TH = tau / H; ok &= c / TH == c * H / tau and (c / TH) * TH == c
    a0 = CH.floor()                                                     # the SI reading through the chart theme (gate G09: no float literal in this tier)
    # 7:A31 (p21052)
    R.check("A31", "the weak-acceleration floor of registration against the drift, carried from the gravitational paper: a₀ = c/T_H = cH₀/2π with T_H = 2π/H₀ the drive period by the angle–count dictionary, an identity of exact rationals in every value of the symbols; at H₀ = 67.4 km s⁻¹ Mpc⁻¹ the floor is 1.04 × 10⁻¹⁰ m s⁻², against the fitted 1.20 ± 0.24 × 10⁻¹⁰ [chart]", ok,
            f"a₀ = {a0:.3e} m s⁻² at H₀ = 67.4 km s⁻¹ Mpc⁻¹; fitted (1.20 ± 0.24) × 10⁻¹⁰ (21:P3, chart)")
    # 7:A17 (p00042)
    R.check("A17", "time is the drive: on the three Subjects the drive g generates 𝔽_p^× (one orbit on the nonzero cells, the register back after 4κ steps, so the register alone registers no duration), and on the three laboratory pairs, on (13, 181) and on every admissible pair the registrable depth p² is odd and below the even cycle Ω − 1, so the chart count n mod (Ω − 1) is injective on every registered duration: a registered duration is the count of drive steps", ok, "; ".join(det))


# ---- block B: the register and the shell (7:B1, B4) -------------------------------------------------------------------------
@R.block("B", BLOCK["B"])
def block_B():
    # the register (7:B6): the translations [x:y] ↦ [x + by : y] of the frame's line are the unipotent moves; for b ≠ 0 each fixes
    # exactly the antipode [1:0], and on the cells the translations are one orbit of order p, the additive cycle C_p
    ok, det = True, []
    for p, g in SHELLS:
        pts = [(x, 1) for x in range(p)] + [(1, 0)]                                  # ℙ¹(𝔽_p): the residues [x:1] and the antipode [1:0]
        fixed = [{(x, y) for (x, y) in pts if ((x + b * y) % p, y) == (x, y)} for b in range(1, p)]
        orbit = {frozenset((x + b) % p for b in range(p)) for x in range(p)}
        ok &= len(pts) == p + 1 and all(f == {(1, 0)} for f in fixed) and orbit == {frozenset(range(p))}
        det.append(f"p={p}: {p - 1} nontrivial translations, each fixing [1:0] alone among {p + 1} directions; the cells one orbit of order {p}")
    # 7:B6 (p07050)
    R.check("B6", "the register: the translations [x:y] ↦ [x + by : y] of the frame's line are the unipotent moves, and for b ≠ 0 each fixes exactly one of the p + 1 directions, the antipode [1:0]; on the cells the translations form the additive cycle C_p, one orbit of order p, on the three Subjects", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        k = (p - 1) // 4
        divides, counts, partition, eq = PJ.class_equation(p)
        hf = PJ.hopf_fibration(p, g)
        ok &= divides and partition and eq and counts == {p - 1: p * (p + 1) // 2, p: p + 1, p + 1: p * (p - 1) // 2}
        ok &= hf["borel_section"] and hf["lift_meets_torus_in_pm_I"]
        det.append(f"p={p}: maximal cyclic subgroups {counts}; the Borel lift meets the torus lift in ±I")
    for p, g in SHELLS:
        k = (p - 1) // 4
        ok &= (p - 1, p, p + 1) == (4 * k, 4 * k + 1, 4 * k + 2) and 1 + (p * p - 1) + p * (p + 1) * (p - 2) // 2 + p * p * (p - 1) // 2 == (p - 1) * p * (p + 1)
        det.append(f"p={p}: cycles of orders {4 * k}, {4 * k + 1}, {4 * k + 2}, the class equation summing to {(p - 1) * p * (p + 1)}")
    # 7:B1 (p07003)
    R.check("B1", "every frame move factors uniquely as a Borel move times a boost (G = B · T, the Borel simply transitive on the causal rays) and on the spin cover the Borel lift meets the torus lift in ±I, the obstruction to a section, enumerated on 𝔽₁₃; the three cycles have the consecutive orders 4κ, 4κ + 1, 4κ + 2 and the class equation sums to |G| on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))
    ok, det = True, []
    for p, g in SHELLS:
        ok &= not SH.is_square(g, p) and norm_one_order(g, p) == p + 1 and norm_one_order(g * g % p, p) == p - 1
        ok &= SH.isotropic_count((1, (-g) % p), p) == 1 and SH.isotropic_count((1, (-g * g) % p), p) == 2 * p - 1
        nulls, lines = PJ.null_count_by_fibres(p, g)
        ok &= lines == p * p + 1
        det.append(f"p={p}: g={g} nonsquare; −g t² + x² anisotropic with |N¹| = {p + 1}; the square coefficient splits with |N¹| = {p - 1}; register null lines {lines}")
    for p, g in ENUM:
        eh = PJ.elliptic_hyperbolic(p, g)
        ok &= eh["register_null"] == p * p + 1 and not eh["register_plane"] and eh["frame_null"] == (p + 1) ** 2 and eh["frame_plane"]
        det.append(f"p={p}: no totally isotropic plane in the register square, one in the frame quadric")
    # 7:B4 (p07042)
    R.check("B4", "the necessity chain: the drive's generator g is a nonsquare, the temporal plane −g t² + x² is anisotropic (its only null vector is zero) with norm-one group of order p + 1, the third cycle, and the register square is elliptic with p² + 1 null lines; a square coefficient gives the split plane (2p − 1 null vectors) and the cycle C_{p−1} again, on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉; no totally isotropic plane in the register square and one in the frame quadric, enumerated on 𝔽₁₃", ok, "; ".join(det))
    # the registrable depth (7:B5): the Subject's register pair takes p² values, registration distinguishes states only, so a
    # sequence of distinct registrations has at most p² entries (frc/subject.py's drift_depth gives the depth against the Carrier's cycle)
    ok, det = True, []
    for p, g in SHELLS:
        states = {(x, y) for x in range(p) for y in range(p)}                      # the register pair, a state per pair of cells
        run = sorted(states)                                                        # a sequence of distinct states: p² entries, and no longer one exists
        ok &= len(states) == p * p and len(run) == p * p and len(set(run)) == len(run) and all(len(set(run[:k])) == k for k in (1, p, p * p))
        det.append(f"p={p}: {p * p} states of the register pair, a run of distinct registrations has at most {p * p} entries")
    for p, Om in PAIRS + [(13, 181)]:
        below, inj, d, cyc = SB.drift_depth(p, Om)
        ok &= below and d == p * p
        det.append(f"({p}, {Om}): depth {d} < cycle {cyc}")
    # 7:B5 (p07049)
    R.check("B5", "the registrable depth: on the three Subjects the register pair takes p² values and a sequence of distinct registrations has at most p² entries (the full run of p² distinct states exists and none longer), and on the three laboratory pairs and (13, 181) the depth p² lies below the Carrier's cycle Ω − 1", ok, "; ".join(det))


# ---- block C: the forms, the cone and the fibration (7:C1–C9, X1, X2, X5) ----------------------------------------------------
@R.block("C", BLOCK["C"])
def block_C():
    ok, det = True, []
    for p, g in ENUM:
        ident, nulls, lines = PJ.register_square(p, g)
        ok &= ident and nulls == p ** 3 - p * p + p and lines == p * p + 1
        det.append(f"p={p}: det X(x) = Q(x) on all {p ** 4} vectors; null vectors {nulls}, null lines {lines}")
    for p, g in SHELLS:
        nulls, lines = PJ.null_count_by_fibres(p, g)
        ok &= nulls == p ** 3 - p * p + p and lines == p * p + 1
        det.append(f"p={p}: null vectors {nulls}, null lines {lines} by the binary fibres")
    # 7:C1 (p07005)
    R.check("C1", "the register square: X(x) = [[x₀ + x₃, x₁ + ηx₂], [x₁ − ηx₂, x₀ − x₃]] is Hermitian with det X(x) = x₀² − x₁² − x₃² + g x₂² on every x ∈ 𝔽₁₃⁴, the coordinates recovered from the matrix; the null count is the elliptic one, p³ − p² + p vectors and p² + 1 lines, on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))
    im = image(P, G)
    ok = (im["sl2K"] == im["sl2K_formula"] and im["kernel"] == 2 and im["image"] == im["image_formula"] and im["index"] == 4
          and im["o_minus_4"] == SH.o_minus_4(P))
    # 7:C2 (p07006), 7:X4 (p07023)
    R.check("C2", "the congruence X ↦ A X A† of SL₂(𝔽₁₆₉) on the register square, enumerated over all 4 826 640 matrices: the kernel is ±I (two matrices fix the four basis vectors), so the image has order 13²(13⁴ − 1)/2 = 2 413 320, one quarter of |O₄⁻(13)| = 9 653 280 — the finite Lorentz group PSL₂(𝔽₁₆₉), the spinor kernel of X4", ok,
            f"|SL₂(K)| = {im['sl2K']}, kernel {im['kernel']}, image {im['image']}, index {im['index']}")
    ok, det = True, []
    for p, g in ENUM:
        bij, n, lines, sym, tim = PJ.cone_bijection(p, g)
        ok &= bij and n == lines == p * p + 1 and sym == p + 1 and tim == p * (p - 1)
        det.append(f"p={p}: {n} directions ↔ {lines} null lines, {sym} symmetric (in space), {tim} with a time component")
    for p, g in SHELLS:
        ok &= p + 1 + p * (p - 1) == p * p + 1
        det.append(f"p={p}: {p + 1} + {p * (p - 1)} = {p * p + 1}")
    # 7:C3 (p07007), 7:C4 (p07008)
    R.check("C3", "the cone is ℙ¹(K): [v] ↦ [v v†] is a bijection onto the null lines of the register square, p² + 1 directions, enumerated on 𝔽₁₃; the p + 1 points of ℙ¹(𝔽_p) give the symmetric null matrices (x₂ = 0), the null directions inside space, and the p(p − 1) others carry a time component (x₂ ≠ 0), the causal rays — the count p + 1 + p(p − 1) = p² + 1 on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        eh = PJ.elliptic_hyperbolic(p, g)
        ok &= eh["frame_null"] == (p + 1) ** 2 and eh["frame_plane"] and eh["register_null"] == p * p + 1 and not eh["register_plane"]
        ok &= eh["s4_null"] == eh["s31_null"] == (p + 1) ** 2
        det.append(f"p={p}: frame quadric {eh['frame_null']} null lines with an isotropic plane; register square {eh['register_null']} without; ⟨1,1,1,1⟩ and ⟨1,1,1,−1⟩ both {eh['s4_null']}")
    for p, g in SHELLS:
        ok &= SH.is_square(p - 1, p)
        det.append(f"p={p}: −1 a square")
    # 7:C5 (p07009), 7:X1 (p07020)
    R.check("C5", "exactly two four-dimensional classes: the frame quadric (M₂(𝔽_p), det) is hyperbolic — (p + 1)² null lines and a totally isotropic plane — and the register square elliptic — p² + 1 null lines and no totally isotropic plane; ⟨1,1,1,1⟩ and ⟨1,1,1,−1⟩ have the same null count, enumerated on 𝔽₁₃; −1 is a square on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉, so the sign pattern is not the invariant, the Witt index is (the elliptic class is Lorentzian by the index chart)", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        s_ = PJ.similitude(p, g, g)
        ok &= s_["multiplies"] and s_["exchanges"] and s_["equal_classes"] and s_["bijective"]
        det.append(f"p={p}: c={s_['c']}, (a, b)={s_['ab']}, Q(Sx) = g Q(x), the two non-null classes exchanged")
    # 7:C6 (p07010), 7:X5 (p07024)
    R.check("C6", "no inertia: with a² + b² = g and c² = −1 the similitude (t, x, y, z) ↦ (cz, ax − by, bx + ay, cgt) multiplies Q_g by g, so it is an isometry ⟨1,1,1,g⟩ ≅ ⟨1,g,g,g⟩ exchanging the two non-null classes (equal in size) and fixing the null cone: a change of unit exchanges the label, the cone is the invariant, enumerated on 𝔽₁₃", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        hf = PJ.hopf_fibration(p, g)
        ok &= hf["rays"] == p * (p - 1) and hf["transitive"] and hf["stabiliser"] == p + 1 and hf["torus"] and hf["count"]
        ok &= hf["borel_section"] and hf["borel_lift_orbits"] == [p * (p - 1) // 2] * 2 and hf["lift_meets_torus_in_pm_I"]
        det.append(f"p={p}: {hf['rays']} rays, stabiliser the norm-one torus of order {hf['stabiliser']}, |SL₂| = rays × fibre; Borel lift orbits {hf['borel_lift_orbits']}")
    for p, g in SHELLS:
        ok &= p * (p - 1) * (p + 1) == (p - 1) * p * (p + 1)
    # 7:C7 (p07031)
    R.check("C7", "the fibration is exact: SL₂(𝔽_p) acts transitively on the p(p − 1) causal rays with stabiliser the norm-one torus C_{p+1}, |SL₂| = p(p − 1)·(p + 1); the Borel of G is simply transitive on the rays, a section; on the spin cover the Borel lift has two orbits of p(p − 1)/2 and meets the torus lift in ±I, so no subgroup section, enumerated on 𝔽₁₃", ok, "; ".join(det))
    ok, det = True, []
    for p, g in MID:
        null, internal, external = PJ.direction_classes(p, g)
        ok &= (null, internal, external) == (p + 1, p * (p - 1) // 2, p * (p + 1) // 2) and null + internal + external == p * p + p + 1
        det.append(f"p={p}: null {null}, internal (nonsquare axes, the Hopf base) {internal}, external {external}")
    for p, g in ENUM:
        ok &= PJ.hopf_fibration(p, g)["axes_nonsquare"]
        det.append(f"p={p}: every ray's axis t² − tr(z)t + N(z) has nonsquare discriminant")
    # 7:C8 (p07032)
    R.check("C8", "the Hopf base: the stabiliser of a causal ray z fixes the binary form with roots {z, z̄}, of discriminant 4g(Im z)², a nonsquare, so the causal rays are the oriented nonsquare axes, two per axis (every ray's axis checked on 𝔽₁₃); the p² + p + 1 directions of space are root pairs: p + 1 double, p(p + 1)/2 split, p(p − 1)/2 conjugate (the internal points of the conic), on 𝔽₁₃ and 𝔽₁₇₃", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        divides, counts, partition, eq = PJ.class_equation(p)
        ok &= divides and partition and eq and counts == {p - 1: p * (p + 1) // 2, p: p + 1, p + 1: p * (p - 1) // 2}
        det.append(f"p={p}: orders divide p−1, p, p+1; maximal cyclic subgroups {counts}")
    for p, g in SHELLS:
        ok &= 1 + (p * p - 1) + p * (p + 1) * (p - 2) // 2 + p * p * (p - 1) // 2 == (p - 1) * p * (p + 1)
        det.append(f"p={p}: 1 + (p² − 1) + p(p+1)(p−2)/2 + p²(p−1)/2 = {(p - 1) * p * (p + 1)}")
    # 7:C9 (p07040), 7:X2 (p07021)
    R.check("C9", "the class equation of PGL₂(𝔽_p): every element has order dividing p − 1, p or p + 1; the maximal cyclic subgroups are the p(p + 1)/2 split tori, the p + 1 unipotent groups and the p(p − 1)/2 non-split tori, partitioning G ∖ {1}, enumerated on 𝔽₁₃; 1 + (p² − 1) + p(p + 1)(p − 2)/2 + p²(p − 1)/2 = (p − 1)p(p + 1) on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))
    # the fixed points (7:C10): a Möbius move fixes the roots of its characteristic form on ℙ¹(𝔽_p), two, one or none as the
    # discriminant is a nonzero square, zero or a nonsquare; the three kinds of maximal cyclic subgroup match the three kinds of direction
    ok, det = True, []
    for p, g in ENUM:
        def nz(u, v): return ((u * pow(v, -1, p)) % p, 1) if v % p else (1, 0)
        pts = [(x, 1) for x in range(p)] + [(1, 0)]
        tally, consistent = {0: 0, 1: 0, 2: 0}, True
        for a, b, c, d in PJ.pgl2(p):
            if (a, b, c, d) == (1, 0, 0, 1): continue
            fx = sum(1 for (x, y) in pts if nz((a * x + b * y) % p, (c * x + d * y) % p) == (x, y))
            disc = ((a + d) ** 2 - 4 * (a * d - b * c)) % p
            consistent &= fx == (1 if disc == 0 else 2 if SH.is_square(disc, p) else 0); tally[fx] += 1
        _, counts, _, _ = PJ.class_equation(p); null, internal, external = PJ.direction_classes(p, g)
        ok &= consistent and tally == {2: p * (p + 1) * (p - 2) // 2, 1: p * p - 1, 0: p * p * (p - 1) // 2}
        ok &= (counts[p - 1], counts[p], counts[p + 1]) == (external, null, internal)
        det.append(f"p={p}: fixed points two/one/none by the discriminant class on all {(p - 1) * p * (p + 1) - 1} non-identity moves {tally}; split tori {counts[p - 1]} = square axes {external}, unipotent groups {counts[p]} = null directions {null}, non-split tori {counts[p + 1]} = nonsquare axes {internal}")
    # 7:C10 (p07051)
    R.check("C10", "the fixed points: on ℙ¹(𝔽₁₃) every non-identity move fixes two, one or no direction as the discriminant of its characteristic form is a nonzero square, zero or a nonsquare (all 2183 moves); the three kinds of cycle are the three kinds of direction of space, the p(p + 1)/2 split tori matching the square axes, the p + 1 unipotent groups the null directions and the p(p − 1)/2 non-split tori the nonsquare axes", ok, "; ".join(det))


# ---- block D: time and the antipode (7:D1, D3–D6, X4) --------------------------------------------------------------------------
@R.block("D", BLOCK["D"])
def block_D():
    im = image(P, G)
    so = PJ.so3(P); dr = PJ.drive_on_square(P, G, G)
    ok = im["stabiliser"] == im["stabiliser_rational"] == P * (P * P - 1) and so[0] == so[1] and so[3] and dr["time_scaled_by_g"] and dr["g_nonsquare"]
    # 7:D1 (p07011)
    R.check("D1", "the stabiliser of the time vector ηJ in SL₂(𝔽₁₆₉), over all 4 826 640 matrices, is exactly the 2184 matrices with entries in 𝔽₁₃ — the spin cover SL₂(𝔽₁₃) — which acts on Sym²(V) through the adjoint action PGL₂ → SO₃ (injective, orthogonal); the one-chronon move diag(g, 1), of nonsquare determinant, fixes the time line and scales the vector by g", ok,
            f"stabiliser {im['stabiliser']} = |SL₂(𝔽₁₃)|, all rational; so3 injective {so[0] == so[1]}")
    ok, det = True, []
    for p, g in MID:
        dr = PJ.drive_on_square(p, g, g)
        ok &= all(dr.values())
        det.append(f"p={p}: {dr}")
    # 7:D3 (p07013)
    R.check("D3", "the drive on the square: diag(g, 1) carries every ray [z : 1] to [gz : 1] and ηJ to g·ηJ (two chronons scale by the square g²); its unimodular lift D = diag(η, η⁻¹) has det 1, D† = −D and carries ηJ to −ηJ; the even transport diag(g, g⁻¹) ∈ SL₂(𝔽_p) fixes ηJ and σ_x and dilates E₂₂ by g⁻², E₁₁ by g², on 𝔽₁₃ and 𝔽₁₇₃", ok, "; ".join(det))
    ok, det = True, []
    for p, g in SHELLS:
        tc = PJ.two_circuits(p, g)
        ok &= tc["order"] == p + 1 and tc["contains_minus_I"] and tc["image_order"] == (p + 1) // 2 and tc["conjugate_to_torus"]
        det.append(f"p={p}: |N¹| = {tc['order']}, image on the square of order {tc['image_order']}, conjugate to the torus lift through P")
    # 7:D4 (p07014)
    R.check("D4", "two circuits: N¹ = {diag(λ, λ̄) : N(λ) = 1} has order p + 1 and contains −I, its image on the register square has order (p + 1)/2 (−I acts trivially), and P diag(λ, λ̄) P⁻¹, P = [[η, −η], [1, 1]], is the multiplication by λ in the basis (1, η): N¹ and the torus lift are conjugate in SL₂(K), on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))
    ok, det = True, []
    for p, g in ENUM:
        iso, n = PJ.no_definite_space(p, g)
        ok &= iso and n == p ** 3 + p * p + p + 1
        det.append(f"p={p}: all {n} three-dimensional subspaces carry a null vector")
    # 7:D5 (p07015)
    R.check("D5", "no definite space: every three-dimensional subspace of the register square (every hyperplane, p³ + p² + p + 1 of them) contains a nonzero null vector of the determinant form, by search on 𝔽₁₃ (Chevalley–Warning on every shell, the Lean witness)", ok, "; ".join(det))
    ok, det = True, []
    for p, g in MID:
        k = (p - 1) // 4
        hh = PJ.antipode_half_step(p, g)
        ok &= hh["regular"] and hh["order_two_classes"] == {(1, 0)} and hh["first_step"] == {2 * k + 1} and hh["half"] == 2 * k + 1 and hh["half_odd"] and hh["even_never"]
        det.append(f"p={p}: {hh['generators']} generators, each reaching the antipode first at step {2 * k + 1}; the even steps never")
    for p, g in SHELLS:
        k = (p - 1) // 4
        ok &= (p + 1) // 2 == 2 * k + 1 and (2 * k + 1) % 2 == 1
    # 7:D6 (p07033)
    R.check("D6", "the antipode: K^×/𝔽_p^× (cyclic of order p + 1) acts regularly on ℙ¹(𝔽_p); the antipode [1 : 0] is its unique element of order two, reached from the origin [0 : 1] by every generator first at the half step (p + 1)/2 = 2κ + 1, which is odd; the unimodular torus, the even steps, never reaches it, on 𝔽₁₃ and 𝔽₁₇₃; the half step odd on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉", ok, "; ".join(det))


# ---- block F: the arrow (7:F1, F3, F4, X6) ---------------------------------------------------------------------------------------
@R.block("F", BLOCK["F"])
def block_F():
    ok = all(SB.leak_rate(p, Om)[1] == Fr(1, Om - 1) and SB.leak_rate(p, Om)[0] == Fr((p - 1) // 4, (Om - 1) // 4) for p, Om in ADMISSIBLE + PAIRS)
    ok &= all(SB.apsidal_bound(p, Om) == (p * p < Om, p * p < Om) for p in range(5, 60, 4) if arith.is_prime(p) for Om in range(p + 1, 2000) if arith.is_prime(Om) and Om % 4 == 1)
    ok &= [SB.leak_rate(p, Om)[1] for p, Om in PAIRS] == [Fr(1, 232), Fr(1, 30088), Fr(1, 2408560)]
    # 7:F1 (p07044)
    R.check("F1", f"one rate for every observer: on every admissible pair below (200, 3000) ({len(ADMISSIBLE)}) and on the three laboratory pairs an embedded shell drifts by 1/(Ω − 1) of the Carrier cycle per chronon and κ/S per revolution, 1/232, 1/30088 and 1/2408560; and the rate lies below 1/(√Ω + 1) exactly when p² < Ω, on every prime pair p ≡ 1 (4) below (60, 2000)", ok, "")
    im = image(P, G)
    ok = im["T_hits"] == im["P_hits"] == im["PT_hits"] == 0 and im["index"] == 4
    # the determinants of the three maps on the four coordinates, and the Frobenius as x₂ ↦ −x₂
    K = Ext(P, G)
    frob = all(tuple(K.conj(v) for v in PJ.herm(K, x)) == PJ.herm(K, (x[0], x[1], (-x[2]) % P, x[3])) for x in ((a, b, c, d) for a in range(P) for b in range(P) for c in range(0, P, 3) for d in range(0, P, 4)))
    ok &= frob
    # 7:F3 (p07046), 7:X6 (p07048)
    R.check("F3", "the time reversal is not a Lorentz move: over all of SL₂(𝔽₁₆₉) no congruence realises the time reversal (the Frobenius σ of K, which acts on X(x) as x₂ ↦ −x₂), the spatial reflection x₁ ↦ −x₁ or the total inversion X ↦ −X; the image is one coset of four in O₄⁻(13), the three others are those maps", ok,
            f"hits T {im['T_hits']}, P {im['P_hits']}, −I {im['PT_hits']}; index {im['index']}")
    lo = {pair: SB.drift_order(*pair) for pair in PAIRS}
    ok = all(v[0] == 1 and v[1] == 4 * ((p - 1) // 4) * ((Om - 1) // 4) and v[2] and v[3] and v[4] for (p, Om), v in lo.items())
    ok &= [v[1] for v in lo.values()] == [696, 1293784, 932112720]
    ok &= all(SB.drift_order(p, Om)[1] == SB.joint_cycle(p, Om)[0] for p, Om in ADMISSIBLE[:60])
    # the general pair: gcd(κ, S) > 1 on the nested pairs (13, 181), (13, 193), (13, 229), (13, 241) — gcd 3, the joint period 4κS/3,
    # the chart counts distinct on the first S/3 revolutions and repeating at S/3
    gl = {pair: SB.drift_order(*pair) for pair in ((13, 181), (13, 193), (13, 229), (13, 241))}
    ok &= all(arith.is_prime(Om) and 13 * 13 < Om and v[0] == 3 and v[1] == 4 * 3 * ((Om - 1) // 4) // 3 and (not v[2]) and v[3] and v[4] for (p, Om), v in gl.items())
    ok &= gl[(13, 181)][1] == 180
    # the physical pair: the registrable depth p² below the cycle Ω − 1, the chart count injective on it, and the hosted period above it
    dd = {pair: SB.drift_depth(*pair) for pair in PAIRS + [(13, 181)]}
    ok &= all(v[0] and v[1] for v in dd.values()) and all(dd[pair][2] < (lo | gl)[pair][1] for pair in dd)
    # 7:F4 (p07047)
    R.check("F4", "the drift is one-directional: on the three laboratory pairs and on (13, 181) the registrable depth p² (169, 29 929, 2 399 401, 169) lies below the Carrier's cycle Ω − 1 (232, 30 088, 2 408 560, 180), so the chart count n mod (Ω − 1) is injective on every registered duration and no recurrence is registrable; on a hosted Carrier run through its cycle the joint period is lcm(4κ, 4S) = 4κS — 696, 1 293 784, 932 112 720 — above the registrable depth, the chart counts 4κn mod 4S of the first S revolutions distinct and repeating at S, and on (13, 181), (13, 193), (13, 229), (13, 241) with gcd(κ, S) = 3 the period 4κS/3 (180 at (13, 181)); the joint period agrees with the joint cycle on the admissible pairs", ok,
            "; ".join(f"({p}, {Om}): depth {v[2]} < cycle {v[3]}" for (p, Om), v in dd.items()) + "; " + "; ".join(f"({p}, {Om}): {v}" for (p, Om), v in list(lo.items()) + list(gl.items())))
    # the record (the state face): the chart counts n mod (Ω − 1) of the n ≤ p² registered chronons are 0, …, n themselves, strictly
    # increasing, so a record gains one entry per chronon and none recurs; the first return of the count is at Ω − 1, above the depth p²;
    # the record's bound p² is the capacity of the register pair, 4κ(p + 1) + 1: the quarter-turn group Q₄ = {±1, ±i}, i = −g^κ of order
    # four, acts freely by scalars on the p² − 1 nonzero pair states, in κ(p + 1) orbits of four, the channel count of the first law (00:D15)
    rec = {}
    for p, Om in PAIRS:
        d, cyc, kap = p * p, Om - 1, (p - 1) // 4
        counts = [n % cyc for n in range(d + 1)]
        rec[(p, Om)] = (counts == list(range(d + 1)), all(counts[i] < counts[i + 1] for i in range(d)),
                        all(n % cyc for n in range(1, cyc)) and cyc % cyc == 0 and d < cyc, d == 4 * kap * (p + 1) + 1, kap * (p + 1) == (d - 1) // 4)
    ok = all(all(v) for v in rec.values())
    orb = {}
    for p, g in SHELLS:
        kap = (p - 1) // 4; i = (-pow(g, kap, p)) % p
        free = pow(i, 2, p) == p - 1 and pow(i, 4, p) == 1 and all((a * i - a) % p or (b * i - b) % p for a in range(p) for b in range(p) if (a, b) != (0, 0))
        reps_ = sum(1 for a in range(p) for b in range(p) if (a, b) != (0, 0) and (a, b) == min(((a * pow(i, k, p)) % p, (b * pow(i, k, p)) % p) for k in range(4)))
        orb[p] = (free, reps_ == kap * (p + 1) == (p * p - 1) // 4)
        ok &= free and orb[p][1]
    # 7:F5 (p07052)
    R.check("F5", "the second law of the record: on the three laboratory pairs the record of n ≤ p² registered chronons, the chart counts n mod (Ω − 1), is the counts 0, …, n themselves, strictly increasing and never repeating, so the record gains one entry per chronon with its entries distinct, and an entropy of one k_B per registration never decreases on a registrable duration; the first return of the count is at n = Ω − 1 (232, 30 088, 2 408 560), above the depth p² (169, 29 929, 2 399 401); the record holds at most p² = 4κ(p + 1) + 1 entries, the capacity of the register pair (169 = 4 · 42 + 1, 29 929 = 4 · 7 482 + 1, 2 399 401 = 4 · 599 850 + 1): the quarter-turn group {±1, ±i} acts freely on the nonzero pair states of the three Subjects, in κ(p + 1) orbits of four, the channel count of the first law, plus the origin", ok,
            "; ".join(f"({p}, {Om}): record 0..{p * p} = counts, first return at {Om - 1}, p² − 1 = 4 · {((p - 1) // 4) * (p + 1)}" for p, Om in PAIRS) + "; " + "; ".join(f"p={p}: Q₄ free on the nonzero pairs, {((p - 1) // 4) * (p + 1)} orbits of four" for p, _ in SHELLS))


# ---- block P: the predictions (7:P1, 7:P2) --------------------------------------------------------------------------------------------
@R.block("P", BLOCK["P"])
def block_P():
    ok, det = True, []
    for p, g in MID:
        null, internal, external = PJ.direction_classes(p, g)
        ok &= null + internal + external == p * p + p + 1
        det.append(f"p={p}: {p * p + p + 1} directions of the three-dimensional space in three classes")
    for p, g in ENUM:
        divides, counts, partition, eq = PJ.class_equation(p)
        ok &= len(counts) == 3 and partition
        det.append(f"p={p}: three kinds of maximal cyclic subgroup, three cycles")
    for p, g in SHELLS:
        ok &= (p + 1) + p * (p - 1) // 2 + p * (p + 1) // 2 == p * p + p + 1
    # 7:P1 (p07026)
    R.check("P1", "three spatial dimensions, staked: space is Sym²(V), of dimension three (its p² + p + 1 directions fall in the three classes of the three cycles — counted on 𝔽₁₃ and 𝔽₁₇₃, summed on 𝔽₁₃, 𝔽₁₇₃ and 𝔽₁₅₄₉ — and the frame moves have no fourth cycle), at every registrable scale through the declared metric chart; falsifier a short-range departure from the inverse-square law of the extra-dimension form; confrontation: the law holds to 52 μm (Lee et al. 2020) [data]", ok, "; ".join(det))
    # the floor and the temperature: with T_dS = ħH/(τ k_B) (Gibbons–Hawking, τ the full cycle 2π of the dictionary), a₀ = cH/τ (21:P3)
    # and the chart's unit |k_B| = ħ/c (00:B7), k_B T_dS = (ħ/c) a₀ and T_dS = a₀, as an identity of rationals in every value of the
    # symbols; on the three Carriers the residues of frc/carrier.py satisfy k_B c ≡ ħ, ħ² ≡ −1 and k_B² ≡ −2; the SI numbers are the detail
    ok, det = True, []
    for hbar, c, H, tau in ((Fr(3, 7), Fr(5, 2), Fr(11, 13), Fr(44, 7)), (Fr(1), Fr(1), Fr(1), Fr(1)), (Fr(105, 1000), Fr(29979, 100), Fr(218, 100), Fr(628, 100))):
        kB = hbar / c
        T, a0 = hbar * H / (tau * kB), c * H / tau
        ok &= kB * T == (hbar / c) * a0 and T == a0
    for p, Om in PAIRS:
        r = CA.register((Om - 1) // 4)
        ok &= r["kB"] * r["c"] % Om == r["hbar"] and r["hbar"] ** 2 % Om == Om - 1 and r["kB"] ** 2 % Om == Om - 2
        det.append(f"Ω={Om}: k_B c = {r['kB']} · {r['c']} ≡ {r['hbar']} = ħ, ħ² ≡ −1, k_B² ≡ −2")
    T, a0, unit = CH.de_sitter_temperature(), CH.floor(), CH.HBAR / (CH.C_LIGHT * CH.K_BOLTZMANN)   # the SI readings through the chart theme (gate G09)
    det.append(f"SI at H₀ = 67.4 km s⁻¹ Mpc⁻¹: T_dS = {T:.3e} K, a₀ = {a0:.3e} m s⁻², ħ/(c k_B) = {CH.show(unit, '.3e')} K s² m⁻¹, T_dS/(a₀ ħ/(c k_B)) = {T / (a0 * unit):.6f}")
    # 7:P2 (p07054)
    R.check("P2", "the floor is the Carrier's temperature: with the de Sitter temperature T_dS = ħH/(2π k_B), the floor a₀ = cH/2π and the chart's unit |k_B| = ħ/c, the identity k_B T_dS = (ħ/c) a₀ and T_dS = a₀ hold in every value of the symbols (exact rationals), and on the three Carriers 𝔽₂₃₃, 𝔽₃₀₀₈₉, 𝔽₂₄₀₈₅₆₁ the register's residues satisfy k_B c ≡ ħ, ħ² ≡ −1 and k_B² ≡ −2; in SI the two read 2.66 × 10⁻³⁰ K and 1.04 × 10⁻¹⁰ m s⁻² at H₀ = 67.4 km s⁻¹ Mpc⁻¹ [chart]; falsifier a measured weak-acceleration floor that departs from cH₀/2π", ok, "; ".join(det))


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