The ledger file py/spacetime.py of Emergent Lorentzian Space-Time over Finite Holographic Substrate, rendered with an anchor per line: the marked lines (# 7:C2 (p7010): a predicate and its accession key) are the checks that decide the predicates of the paper's predicate ledger — 39 of 39 checks passing; the predicates' theorems are the declarations of Spacetime in the core. ▶ run the predicates on Google Colab.
1"""p07_spacetime — the ledger file of 7-spacetime (the verification package of 31 October 2026).23"Emergent Lorentzian Space-Time over Finite Holographic Substrate" (Akhtman, 2026). The paper's predicate ledger is4docs/7-spacetime/7-spacetime-ledger.json. This file binds its predicates to the framework: the table of keys (generated5from the ledger by ci/make_ledgers.py) and the checks of six blocks. Each check names the predicate(s) it witnesses6(LEDGER) under a `# 7:XN (<key>)` marker on the check that decides it (PREDICATES). The carried rows of block A keep7their origin keys (the master's 00:, 3-causality's 3:, 38-s13's 38:, 21-gravity's 21:) and are decided here again on8the themes: the frame and the signature (frc/subject.py), the quadratic forms and their counts (frc/shell.py), the9Hopf section, the frame triple, the frame group and its one form (frc/projective.py), the pair's drift and joint cycle10(frc/subject.py), completeness as primality (frc/foundation.py), the retarded flow (frc/covering.py), the single11arrow (frc/drift.py), the Carrier register's residues (frc/carrier.py), the domain of temperature (frc/shell.py's domain12lattice) and the weak-acceleration floor (an identity of exact rationals; the confrontation with the fitted value is1321-gravity's chart check). Since 6 November 2026 the three last rows cite their origin's Lean declarations (the paper's14reports/lean-a31-20261106/): the register (Keys/Carrier), the domain identities (the domain theme's Keys/Domain) and the15floor'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 of16frc/projective.py (7-spacetime's section): the determinant of the Hermitian matrix, the congruence of SL₂(𝔽_{p²}) with17its kernel ±I and its image of index four, the cone, the two four-dimensional classes, the similitude, the fibration,18the class equation, the drive and the lift, the antipode at the half step, the three exclusions of the arrow, the19one-directional drift, the record's second law and, with the Carrier register of frc/carrier.py, the floor as the Carrier's20temperature. Everything is exact (gate G09); the SI readings in the details of A31 and P2 come through the chart theme21(frc/chart.py: floor, de_sitter_temperature). The Lean side is lean/FrcCore/Theme/Lorentz.lean (the projective theme)22with Theme/Spin.lean, Theme/Projective.lean, Theme/Hopf.lean, Theme/Pair.lean and Theme/Register.lean behind it, and lean/FrcMathlib/Theme/23Lorentz.lean for the isotropy of every three-dimensional subspace (Chevalley–Warning, D5), with Theme/Carrier.lean,24Theme/Domain.lean and Theme/Drift.lean behind the carried A33, A32 and A31 and lean/FrcMathlib/Theme/Chart.lean behind A31's25number; the paper modules are26lean/FrcCore/Spacetime.lean and lean/FrcMathlib/Spacetime.lean, the certificates lean/FrcCore/Ledgers/P07Spacetime.lean27and lean/FrcMathlib/Ledgers/P07Spacetime.lean.2829 python3 -m frc.ledgers.p07_spacetime every block, the census; exit 1 if a check fails (≈ 90 s: the one30 enumeration of SL₂(𝔽₁₆₉), 4 826 640 matrices, decides C2, D1 and F3)31 python3 -m frc.ledgers.p07_spacetime C one block (A to F)32 from frc.ledgers.p07_spacetime import R; R.predicate("7:C2") one predicate: its blocks run once per session3334Blocks: 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)35 B the register and the shell EXACT (7:B1, B4, B5, B6)36 C the forms, the cone and the fibration EXACT (7:C1, C2, C3, C4, C5, C6, C7, C8, C9, C10, X1, X2, X5)37 D time and the antipode EXACT (7:D1, D3, D4, D5, D6, X4)38 F the arrow EXACT (7:F1, F3, F4, F5, X6)39 P the predictions EXACT (7:P1, P2)4041The instances are the corpus's three laboratory pairs: the Subjects 𝔽₁₃ (κ = 3), 𝔽₁₇₃ (κ = 43) and 𝔽₁₅₄₉ (κ = 387),42each with the drive g = 2 (a generator and a nonsquare, p ≡ 5 mod 8) and its quadratic extension, inside the Carriers43𝔽₂₃₃, 𝔽₃₀₀₈₉ and 𝔽₂₄₀₈₅₆₁ (38-s13, 39-s173, 37-sim). The identities, the counts by formula and the drift run on all three44(SHELLS, PAIRS); the O(p²) searches on 𝔽₁₃ and 𝔽₁₇₃ (MID); the complete enumerations of SL₂(𝔽_{p²}), PGL₂(𝔽_p) and 𝔽_p⁴45on 𝔽₁₃ alone (ENUM). The notebook frc/ledgers/p07_spacetime.ipynb runs one predicate per cell, the cell's id its key46(gate G13).47"""48import sys49from fractions import Fraction50from math import gcd5152from frc import arith53from frc import carrier as CA54from frc import chart as CH55from frc import covering as CV56from frc import drift as D57from frc import foundation as FO58from frc import projective as PJ59from frc import shell as SH60from frc import subject as SB61from frc.extension import Ext62from frc.registry import Registry6364# ---- generated by ci/make_ledgers.py from docs/7-spacetime/7-spacetime-ledger.json; edit the ledger, not this table ----65PAPER = "7-spacetime"66KEYS = {"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 key67LEAN = {"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 them68# ---- end of the generated table ----6970LEAN_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)7172SHELLS = [(13, 2), (173, 2), (1549, 2)] # (p, g): the three Subjects with the drive g = 2, a generator and a nonsquare; ν = g73MID = SHELLS[:2] # the O(p²) searches: 𝔽₁₃ and 𝔽₁₇₃74ENUM = SHELLS[:1] # the complete enumerations (p³ and p⁴): 𝔽₁₃75PAIRS = [(13, 233), (173, 30089), (1549, 2408561)] # the laboratory pairs (Subject, Carrier) of 38-s13, 39-s173 and 37-sim76P, G, OM = 13, 2, 23377ADMISSIBLE = [(p, Om) for p in range(5, 200) for Om in range(p * p + 1, 3000)78 if SB.admissible(p, Om)["p_prime"] and Om % 48 == 41 and arith.is_prime(Om) and all(SB.admissible(p, Om).values())]7980# The paper's predicate ledger (its appendix, predicates cited as 7:XN): the predicate(s) each check witnesses.81LEDGER = {82 "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",83 "A16": "7:A16", "A17": "7:A17", "A21": "7:A21, 7:A24, 7:A25", "A23": "7:A23", "A26": "7:A26", "A28": "7:A28",84 "A31": "7:A31", "A32": "7:A32", "A33": "7:A33",85 "B1": "7:B1", "B4": "7:B4", "B5": "7:B5", "B6": "7:B6",86 "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",87 "C8": "7:C8", "C9": "7:C9, 7:X2", "C10": "7:C10",88 "D1": "7:D1", "D3": "7:D3", "D4": "7:D4", "D5": "7:D5", "D6": "7:D6",89 "F1": "7:F1", "F3": "7:F3, 7:X6", "F4": "7:F4", "F5": "7:F5",90 "P1": "7:P1", "P2": "7:P2",91}9293BLOCK = {"A": "the inputs carried",94 "B": "the register and the shell",95 "C": "the forms, the cone and the fibration",96 "D": "time and the antipode",97 "F": "the arrow",98 "P": "the predictions"}99100# the deciding check of each witnessed predicate101PREDICATES = {102 "7:A4": "A4", "7:A6": "A6", "7:A10": "A6", "7:A8": "A8", "7:A9": "A8", "7:A11": "A11", "7:A12": "A11", "7:A13": "A13",103 "7:A14": "A13", "7:A15": "A15", "7:A16": "A16", "7:A21": "A21", "7:A24": "A21", "7:A25": "A21", "7:A23": "A23", "7:A26": "A26",104 "7:A28": "A28", "7:A17": "A17", "7:A31": "A31", "7:A32": "A32", "7:A33": "A33",105 "7:B1": "B1", "7:B4": "B4", "7:B5": "B5", "7:B6": "B6",106 "7:C1": "C1", "7:C2": "C2", "7:X4": "C2", "7:C3": "C3", "7:C4": "C3", "7:C5": "C5", "7:X1": "C5", "7:C6": "C6",107 "7:X5": "C6", "7:C7": "C7", "7:C8": "C8", "7:C9": "C9", "7:X2": "C9", "7:C10": "C10",108 "7:D1": "D1", "7:D3": "D3", "7:D4": "D4", "7:D5": "D5", "7:D6": "D6",109 "7:F1": "F1", "7:F3": "F3", "7:X6": "F3", "7:F4": "F4", "7:F5": "F5",110 "7:P1": "P1", "7:P2": "P2",111}112113R = Registry("7", "spacetime", LEDGER, PREDICATES, sources=[__file__])114Fr = Fraction115_IMAGE = {} # the one enumeration of SL₂(𝔽_{p²}) per shell, shared by C2, D1 and F2116117118def image(p, nu):119 if p not in _IMAGE: _IMAGE[p] = PJ.congruence_image(p, nu)120 return _IMAGE[p]121122123def norm_one_order(nu, p):124 """|{(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."""125 return sum(1 for t in range(p) for x in range(p) if (-nu * t * t + x * x) % p == 1)126127128# ---- block A: the inputs carried (7:A4, A6, A8–A17, A21, A23–A26, A28, A31–A33) -------------------------------------------129@R.block("A", BLOCK["A"])130def block_A():131 ok, det = True, []132 for p, g in SHELLS:133 k, _, pi, _ = SB.frame(p); i = (-pow(g, k, p)) % p134 ok &= p == 4 * k + 1 and pi == 2 * k and arith.is_primitive_root(g, p) and not SH.is_square(g, p)135 ok &= pow(i, 2, p) == p - 1 and (-pow(g, k, p)) % p == pow(g, 3 * k, p)136 det.append(f"p={p}: κ={k}, π={pi}, g={g} generator and nonsquare, i=−g^κ={(-pow(g, k, p)) % p} with i²=−1")137 # 7:A4 (p00021)138 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))139 ok, det = True, []140 for p, g in SHELLS:141 ns = norm_one_order(g, p); sq = norm_one_order(g * g % p, p)142 ok &= ns == p + 1 and sq == p - 1143 det.append(f"p={p}: |N¹(−g t² + x²)| = {ns}, |N¹(−g² t² + x²)| = {sq}")144 for p, g in ENUM:145 ok &= all(norm_one_order(nu, p) == (p - 1 if SH.is_square(nu, p) else p + 1) for nu in range(1, p))146 # 7:A6 (p00150), 7:A10 (p03013)147 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))148 ok, det = True, []149 for p, g in ENUM:150 hyp = SH.isotropic_count((1, 1, 1, (-g * g) % p), p); ell = SH.isotropic_count((1, 1, 1, (-g) % p), p)151 ok &= hyp == p ** 3 + p * p - p and ell == p ** 3 - p * p + p152 vc = SH.value_counts((1, 1, 1, (-g) % p), p)153 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))154 ok &= sqv == nsv == (p - 1) * (p ** 3 + p) // 2155 # rescaling by a nonsquare exchanges the two classes, by a square fixes them: the classes are unions of value fibres156 ok &= all(vc[v] == vc[v * g * g % p] for v in range(1, p))157 det.append(f"p={p}: null {hyp} (hyperbolic), {ell} (elliptic); the non-null classes {sqv} = {nsv}")158 for p, g in SHELLS:159 nulls, _ = PJ.null_count_by_fibres(p, g)160 ok &= nulls == p ** 3 - p * p + p161 det.append(f"p={p}: elliptic null count by the binary fibres {nulls} = p³ − p² + p")162 # 7:A8 (p03008), 7:A9 (p03011)163 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))164 ok, det = True, []165 for p, g in ENUM:166 G_ = PJ.pgl2(p); nu = g167 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)])168 n, dirs, bors, bij = PJ.frame_triple(p, nu)169 ok &= facts and len(G_) == (p - 1) * p * (p + 1) and bij and n == (p + 1) * p * (p - 1)170 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)")171 # 7:A11 (p00190), 7:A12 (p38050)172 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))173 r13 = PJ.unit(13)[0]174 so = PJ.so3(13); inv = PJ.involutions(13)175 ok = so[0] == so[1] == 2184 and so[2] == {1} and so[3] and so[4] == 2 * 2184 and inv == (1, 169)176 hw = PJ.hermitian_wJ(13, 2)[1]; sam = PJ.su2_is_sl2(13, 2)177 img = image(13, 2)178 ok &= hw and sam[0] and sam[3] == 0 and img["stabiliser"] == img["stabiliser_rational"] == img["sl2p"] == 2184179 # 7:A13 (p00152), 7:A14 (p00183)180 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,181 f"so3 {so[:2]}, dets {so[2]}, |O₃| {so[4]}; sample {sam}; stabiliser {img['stabiliser']}")182 ok, det = True, []183 for p, g in SHELLS:184 K = Ext(p, g); k = (p - 1) // 4185 pts = {PJ.normal(z, p) for z in K.elements() if z != (0, 0)}186 seam = (2 * k + 1) * 2 % p == 1187 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 seam188 det.append(f"p={p}: ℙ¹ has {len(pts)} points, the antipode [1:0] no residue, 2⁻¹ = {2 * k + 1}")189 # 7:A15 (p00139)190 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))191 ok = all(SH.is_square(pow(g, j, p), p) == (j % 2 == 0) for p, g in SHELLS for j in range(p - 1))192 # 7:A16 (p00028)193 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, "")194 ok, det = True, []195 for p, Om in PAIRS:196 k, S_ = (p - 1) // 4, (Om - 1) // 4197 ang, per, om1, _ = SB.leak_rate(p, Om)198 L, half, _, _ = SB.joint_cycle(p, Om)199 ok &= ang == Fr(k, S_) and per == om1 == Fr(1, Om - 1) and L == 4 * k * S_ // gcd(k, S_) and half == L // 2200 ok &= SB.apsidal_bound(p, Om) == (True, True) and D.nesting_bound(p, Om)[:2] == (True, True)201 det.append(f"({p}, {Om}): κ/S = {ang}, per chronon {per}, joint cycle {L}")202 ok &= all(SB.leak_rate(p, Om)[1] == Fr(1, Om - 1) for p, Om in ADMISSIBLE)203 ok &= all(SB.joint_cycle(p, Om)[0] == SB.least_return(p, Om) for p, Om in ADMISSIBLE[:40])204 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)))205 # 7:A21 (p38053), 7:A24 (p38044), 7:A25 (p38054)206 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,207 "; ".join(det))208 bad = [q for q in range(2, 260) if FO.is_complete(q) != arith.is_prime(q)]209 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)210 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)211 # 7:A23 (p00162)212 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}")213 ok = all(CV.tick(232, k, k) == 0 and CV.tick(232, k, 116 + k) == 116 for k in range(232))214 ok &= all((CV.tick(232, k, b) + b) % 232 == k for b in range(232) for k in range(13))215 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))216 # 7:A26 (p38016)217 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, "")218 arrows = [D.single_arrow(p, g) for p, g in MID]219 ok = all(a[0] for a in arrows) and all(a[1] == p + 1 for a, (p, _) in zip(arrows, MID))220 # 7:A28 (p21018)221 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,222 "; ".join(f"p={p}: circle of order {a[1]}, fixed {a[2]}" for a, (p, _) in zip(arrows, MID)))223 # 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 the224 # register alone registers no duration), the register returns after 4κ chronons, and the pair's chart count is injective on the registrable225 # depth p² < Ω − 1 (frc/subject.py's drift_depth), so a registered duration is the count of drive steps226 ok, det = True, []227 for p, g in SHELLS:228 orbit = set(); x = 1229 for _ in range(p - 1): orbit.add(x); x = (x * g) % p230 ok &= orbit == set(range(1, p)) and x == 1 and pow(g, (p - 1) // 2, p) == p - 1231 for p, Om in PAIRS + [(13, 181)]:232 below, inj, d, cyc = SB.drift_depth(p, Om)233 ok &= below and inj and d % 2 == 1 and cyc % 2 == 0 and d <= cyc - 1234 det.append(f"({p}, {Om}): p²={d} < Ω−1={cyc}, the counts 0..{d} distinct")235 ok &= all(SB.drift_depth(p, Om)[0] and SB.drift_depth(p, Om)[1] for p, Om in ADMISSIBLE)236 # the Carrier register (00:B7): on the three Carriers Ω = 4S + 1 the register {S, Ω, c, ħ, G, k_B} of frc/carrier.py is generator-free237 # 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 sign238 ok, det = True, []239 for p, Om in PAIRS:240 r = CA.register((Om - 1) // 4); S, c, hbar, kB, G = r["S"], r["c"], r["hbar"], r["kB"], r["G"]241 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 - 1242 ok &= kB * kB % Om == Om - 2 and kB * c % Om == hbar and (Om - kB) * c % Om == Om - hbar243 det.append(f"Ω={Om}: S={S}, G={G}=−c², c={c}, ħ={hbar}, k_B={kB}, k_B c ≡ ħ")244 # 7:A33 (p00165)245 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))246 # the domain of temperature (00:C12, 10-dimensions): in the domain lattice of frc/shell.py, [Θ] = [E][k_B]⁻¹ = [L][T]⁻², flag-free; the247 # Unruh combination ħa/(2π c k_B) has the temperature domain; the classical M-L-T-Θ exponents of every listed quantity lift to its domain248 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))249 ok &= SH.dom(SH.HBAR, SH.ACCEL, (SH.SPEED, -1), (SH.KB, -1)) == SH.TEMP and SH.dom(SH.ENERGY, (SH.KB, -1)) == SH.TEMP250 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.MASS251 # 7:A32 (p00032)252 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,253 f"[Θ] = {SH.TEMP} = [a]; [k_B] = {SH.KB}; {len(SH.CLASSICAL)} quantities recovered")254 # 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 exact255 # 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]256 ok = True257 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))):258 TH = tau / H; ok &= c / TH == c * H / tau and (c / TH) * TH == c259 a0 = CH.floor() # the SI reading through the chart theme (gate G09: no float literal in this tier)260 # 7:A31 (p21052)261 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,262 f"a₀ = {a0:.3e} m s⁻² at H₀ = 67.4 km s⁻¹ Mpc⁻¹; fitted (1.20 ± 0.24) × 10⁻¹⁰ (21:P3, chart)")263 # 7:A17 (p00042)264 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))265266267# ---- block B: the register and the shell (7:B1, B4) -------------------------------------------------------------------------268@R.block("B", BLOCK["B"])269def block_B():270 # the register (7:B6): the translations [x:y] ↦ [x + by : y] of the frame's line are the unipotent moves; for b ≠ 0 each fixes271 # exactly the antipode [1:0], and on the cells the translations are one orbit of order p, the additive cycle C_p272 ok, det = True, []273 for p, g in SHELLS:274 pts = [(x, 1) for x in range(p)] + [(1, 0)] # ℙ¹(𝔽_p): the residues [x:1] and the antipode [1:0]275 fixed = [{(x, y) for (x, y) in pts if ((x + b * y) % p, y) == (x, y)} for b in range(1, p)]276 orbit = {frozenset((x + b) % p for b in range(p)) for x in range(p)}277 ok &= len(pts) == p + 1 and all(f == {(1, 0)} for f in fixed) and orbit == {frozenset(range(p))}278 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}")279 # 7:B6 (p07050)280 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))281 ok, det = True, []282 for p, g in ENUM:283 k = (p - 1) // 4284 divides, counts, partition, eq = PJ.class_equation(p)285 hf = PJ.hopf_fibration(p, g)286 ok &= divides and partition and eq and counts == {p - 1: p * (p + 1) // 2, p: p + 1, p + 1: p * (p - 1) // 2}287 ok &= hf["borel_section"] and hf["lift_meets_torus_in_pm_I"]288 det.append(f"p={p}: maximal cyclic subgroups {counts}; the Borel lift meets the torus lift in ±I")289 for p, g in SHELLS:290 k = (p - 1) // 4291 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)292 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)}")293 # 7:B1 (p07003)294 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))295 ok, det = True, []296 for p, g in SHELLS:297 ok &= not SH.is_square(g, p) and norm_one_order(g, p) == p + 1 and norm_one_order(g * g % p, p) == p - 1298 ok &= SH.isotropic_count((1, (-g) % p), p) == 1 and SH.isotropic_count((1, (-g * g) % p), p) == 2 * p - 1299 nulls, lines = PJ.null_count_by_fibres(p, g)300 ok &= lines == p * p + 1301 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}")302 for p, g in ENUM:303 eh = PJ.elliptic_hyperbolic(p, g)304 ok &= eh["register_null"] == p * p + 1 and not eh["register_plane"] and eh["frame_null"] == (p + 1) ** 2 and eh["frame_plane"]305 det.append(f"p={p}: no totally isotropic plane in the register square, one in the frame quadric")306 # 7:B4 (p07042)307 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))308 # the registrable depth (7:B5): the Subject's register pair takes p² values, registration distinguishes states only, so a309 # sequence of distinct registrations has at most p² entries (frc/subject.py's drift_depth gives the depth against the Carrier's cycle)310 ok, det = True, []311 for p, g in SHELLS:312 states = {(x, y) for x in range(p) for y in range(p)} # the register pair, a state per pair of cells313 run = sorted(states) # a sequence of distinct states: p² entries, and no longer one exists314 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))315 det.append(f"p={p}: {p * p} states of the register pair, a run of distinct registrations has at most {p * p} entries")316 for p, Om in PAIRS + [(13, 181)]:317 below, inj, d, cyc = SB.drift_depth(p, Om)318 ok &= below and d == p * p319 det.append(f"({p}, {Om}): depth {d} < cycle {cyc}")320 # 7:B5 (p07049)321 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))322323324# ---- block C: the forms, the cone and the fibration (7:C1–C9, X1, X2, X5) ----------------------------------------------------325@R.block("C", BLOCK["C"])326def block_C():327 ok, det = True, []328 for p, g in ENUM:329 ident, nulls, lines = PJ.register_square(p, g)330 ok &= ident and nulls == p ** 3 - p * p + p and lines == p * p + 1331 det.append(f"p={p}: det X(x) = Q(x) on all {p ** 4} vectors; null vectors {nulls}, null lines {lines}")332 for p, g in SHELLS:333 nulls, lines = PJ.null_count_by_fibres(p, g)334 ok &= nulls == p ** 3 - p * p + p and lines == p * p + 1335 det.append(f"p={p}: null vectors {nulls}, null lines {lines} by the binary fibres")336 # 7:C1 (p07005)337 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))338 im = image(P, G)339 ok = (im["sl2K"] == im["sl2K_formula"] and im["kernel"] == 2 and im["image"] == im["image_formula"] and im["index"] == 4340 and im["o_minus_4"] == SH.o_minus_4(P))341 # 7:C2 (p07006), 7:X4 (p07023)342 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,343 f"|SL₂(K)| = {im['sl2K']}, kernel {im['kernel']}, image {im['image']}, index {im['index']}")344 ok, det = True, []345 for p, g in ENUM:346 bij, n, lines, sym, tim = PJ.cone_bijection(p, g)347 ok &= bij and n == lines == p * p + 1 and sym == p + 1 and tim == p * (p - 1)348 det.append(f"p={p}: {n} directions ↔ {lines} null lines, {sym} symmetric (in space), {tim} with a time component")349 for p, g in SHELLS:350 ok &= p + 1 + p * (p - 1) == p * p + 1351 det.append(f"p={p}: {p + 1} + {p * (p - 1)} = {p * p + 1}")352 # 7:C3 (p07007), 7:C4 (p07008)353 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))354 ok, det = True, []355 for p, g in ENUM:356 eh = PJ.elliptic_hyperbolic(p, g)357 ok &= eh["frame_null"] == (p + 1) ** 2 and eh["frame_plane"] and eh["register_null"] == p * p + 1 and not eh["register_plane"]358 ok &= eh["s4_null"] == eh["s31_null"] == (p + 1) ** 2359 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']}")360 for p, g in SHELLS:361 ok &= SH.is_square(p - 1, p)362 det.append(f"p={p}: −1 a square")363 # 7:C5 (p07009), 7:X1 (p07020)364 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))365 ok, det = True, []366 for p, g in ENUM:367 s_ = PJ.similitude(p, g, g)368 ok &= s_["multiplies"] and s_["exchanges"] and s_["equal_classes"] and s_["bijective"]369 det.append(f"p={p}: c={s_['c']}, (a, b)={s_['ab']}, Q(Sx) = g Q(x), the two non-null classes exchanged")370 # 7:C6 (p07010), 7:X5 (p07024)371 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))372 ok, det = True, []373 for p, g in ENUM:374 hf = PJ.hopf_fibration(p, g)375 ok &= hf["rays"] == p * (p - 1) and hf["transitive"] and hf["stabiliser"] == p + 1 and hf["torus"] and hf["count"]376 ok &= hf["borel_section"] and hf["borel_lift_orbits"] == [p * (p - 1) // 2] * 2 and hf["lift_meets_torus_in_pm_I"]377 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']}")378 for p, g in SHELLS:379 ok &= p * (p - 1) * (p + 1) == (p - 1) * p * (p + 1)380 # 7:C7 (p07031)381 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))382 ok, det = True, []383 for p, g in MID:384 null, internal, external = PJ.direction_classes(p, g)385 ok &= (null, internal, external) == (p + 1, p * (p - 1) // 2, p * (p + 1) // 2) and null + internal + external == p * p + p + 1386 det.append(f"p={p}: null {null}, internal (nonsquare axes, the Hopf base) {internal}, external {external}")387 for p, g in ENUM:388 ok &= PJ.hopf_fibration(p, g)["axes_nonsquare"]389 det.append(f"p={p}: every ray's axis t² − tr(z)t + N(z) has nonsquare discriminant")390 # 7:C8 (p07032)391 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))392 ok, det = True, []393 for p, g in ENUM:394 divides, counts, partition, eq = PJ.class_equation(p)395 ok &= divides and partition and eq and counts == {p - 1: p * (p + 1) // 2, p: p + 1, p + 1: p * (p - 1) // 2}396 det.append(f"p={p}: orders divide p−1, p, p+1; maximal cyclic subgroups {counts}")397 for p, g in SHELLS:398 ok &= 1 + (p * p - 1) + p * (p + 1) * (p - 2) // 2 + p * p * (p - 1) // 2 == (p - 1) * p * (p + 1)399 det.append(f"p={p}: 1 + (p² − 1) + p(p+1)(p−2)/2 + p²(p−1)/2 = {(p - 1) * p * (p + 1)}")400 # 7:C9 (p07040), 7:X2 (p07021)401 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))402 # the fixed points (7:C10): a Möbius move fixes the roots of its characteristic form on ℙ¹(𝔽_p), two, one or none as the403 # discriminant is a nonzero square, zero or a nonsquare; the three kinds of maximal cyclic subgroup match the three kinds of direction404 ok, det = True, []405 for p, g in ENUM:406 def nz(u, v): return ((u * pow(v, -1, p)) % p, 1) if v % p else (1, 0)407 pts = [(x, 1) for x in range(p)] + [(1, 0)]408 tally, consistent = {0: 0, 1: 0, 2: 0}, True409 for a, b, c, d in PJ.pgl2(p):410 if (a, b, c, d) == (1, 0, 0, 1): continue411 fx = sum(1 for (x, y) in pts if nz((a * x + b * y) % p, (c * x + d * y) % p) == (x, y))412 disc = ((a + d) ** 2 - 4 * (a * d - b * c)) % p413 consistent &= fx == (1 if disc == 0 else 2 if SH.is_square(disc, p) else 0); tally[fx] += 1414 _, counts, _, _ = PJ.class_equation(p); null, internal, external = PJ.direction_classes(p, g)415 ok &= consistent and tally == {2: p * (p + 1) * (p - 2) // 2, 1: p * p - 1, 0: p * p * (p - 1) // 2}416 ok &= (counts[p - 1], counts[p], counts[p + 1]) == (external, null, internal)417 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}")418 # 7:C10 (p07051)419 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))420421422# ---- block D: time and the antipode (7:D1, D3–D6, X4) --------------------------------------------------------------------------423@R.block("D", BLOCK["D"])424def block_D():425 im = image(P, G)426 so = PJ.so3(P); dr = PJ.drive_on_square(P, G, G)427 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"]428 # 7:D1 (p07011)429 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,430 f"stabiliser {im['stabiliser']} = |SL₂(𝔽₁₃)|, all rational; so3 injective {so[0] == so[1]}")431 ok, det = True, []432 for p, g in MID:433 dr = PJ.drive_on_square(p, g, g)434 ok &= all(dr.values())435 det.append(f"p={p}: {dr}")436 # 7:D3 (p07013)437 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))438 ok, det = True, []439 for p, g in SHELLS:440 tc = PJ.two_circuits(p, g)441 ok &= tc["order"] == p + 1 and tc["contains_minus_I"] and tc["image_order"] == (p + 1) // 2 and tc["conjugate_to_torus"]442 det.append(f"p={p}: |N¹| = {tc['order']}, image on the square of order {tc['image_order']}, conjugate to the torus lift through P")443 # 7:D4 (p07014)444 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))445 ok, det = True, []446 for p, g in ENUM:447 iso, n = PJ.no_definite_space(p, g)448 ok &= iso and n == p ** 3 + p * p + p + 1449 det.append(f"p={p}: all {n} three-dimensional subspaces carry a null vector")450 # 7:D5 (p07015)451 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))452 ok, det = True, []453 for p, g in MID:454 k = (p - 1) // 4455 hh = PJ.antipode_half_step(p, g)456 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"]457 det.append(f"p={p}: {hh['generators']} generators, each reaching the antipode first at step {2 * k + 1}; the even steps never")458 for p, g in SHELLS:459 k = (p - 1) // 4460 ok &= (p + 1) // 2 == 2 * k + 1 and (2 * k + 1) % 2 == 1461 # 7:D6 (p07033)462 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))463464465# ---- block F: the arrow (7:F1, F3, F4, X6) ---------------------------------------------------------------------------------------466@R.block("F", BLOCK["F"])467def block_F():468 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)469 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)470 ok &= [SB.leak_rate(p, Om)[1] for p, Om in PAIRS] == [Fr(1, 232), Fr(1, 30088), Fr(1, 2408560)]471 # 7:F1 (p07044)472 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, "")473 im = image(P, G)474 ok = im["T_hits"] == im["P_hits"] == im["PT_hits"] == 0 and im["index"] == 4475 # the determinants of the three maps on the four coordinates, and the Frobenius as x₂ ↦ −x₂476 K = Ext(P, G)477 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)))478 ok &= frob479 # 7:F3 (p07046), 7:X6 (p07048)480 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,481 f"hits T {im['T_hits']}, P {im['P_hits']}, −I {im['PT_hits']}; index {im['index']}")482 lo = {pair: SB.drift_order(*pair) for pair in PAIRS}483 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())484 ok &= [v[1] for v in lo.values()] == [696, 1293784, 932112720]485 ok &= all(SB.drift_order(p, Om)[1] == SB.joint_cycle(p, Om)[0] for p, Om in ADMISSIBLE[:60])486 # 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,487 # the chart counts distinct on the first S/3 revolutions and repeating at S/3488 gl = {pair: SB.drift_order(*pair) for pair in ((13, 181), (13, 193), (13, 229), (13, 241))}489 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())490 ok &= gl[(13, 181)][1] == 180491 # the physical pair: the registrable depth p² below the cycle Ω − 1, the chart count injective on it, and the hosted period above it492 dd = {pair: SB.drift_depth(*pair) for pair in PAIRS + [(13, 181)]}493 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)494 # 7:F4 (p07047)495 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,496 "; ".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())))497 # the record (the state face): the chart counts n mod (Ω − 1) of the n ≤ p² registered chronons are 0, …, n themselves, strictly498 # 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²;499 # 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 order500 # 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)501 rec = {}502 for p, Om in PAIRS:503 d, cyc, kap = p * p, Om - 1, (p - 1) // 4504 counts = [n % cyc for n in range(d + 1)]505 rec[(p, Om)] = (counts == list(range(d + 1)), all(counts[i] < counts[i + 1] for i in range(d)),506 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)507 ok = all(all(v) for v in rec.values())508 orb = {}509 for p, g in SHELLS:510 kap = (p - 1) // 4; i = (-pow(g, kap, p)) % p511 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))512 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)))513 orb[p] = (free, reps_ == kap * (p + 1) == (p * p - 1) // 4)514 ok &= free and orb[p][1]515 # 7:F5 (p07052)516 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,517 "; ".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))518519520# ---- block P: the predictions (7:P1, 7:P2) --------------------------------------------------------------------------------------------521@R.block("P", BLOCK["P"])522def block_P():523 ok, det = True, []524 for p, g in MID:525 null, internal, external = PJ.direction_classes(p, g)526 ok &= null + internal + external == p * p + p + 1527 det.append(f"p={p}: {p * p + p + 1} directions of the three-dimensional space in three classes")528 for p, g in ENUM:529 divides, counts, partition, eq = PJ.class_equation(p)530 ok &= len(counts) == 3 and partition531 det.append(f"p={p}: three kinds of maximal cyclic subgroup, three cycles")532 for p, g in SHELLS:533 ok &= (p + 1) + p * (p - 1) // 2 + p * (p + 1) // 2 == p * p + p + 1534 # 7:P1 (p07026)535 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))536 # the floor and the temperature: with T_dS = ħH/(τ k_B) (Gibbons–Hawking, τ the full cycle 2π of the dictionary), a₀ = cH/τ (21:P3)537 # 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 the538 # 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 detail539 ok, det = True, []540 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))):541 kB = hbar / c542 T, a0 = hbar * H / (tau * kB), c * H / tau543 ok &= kB * T == (hbar / c) * a0 and T == a0544 for p, Om in PAIRS:545 r = CA.register((Om - 1) // 4)546 ok &= r["kB"] * r["c"] % Om == r["hbar"] and r["hbar"] ** 2 % Om == Om - 1 and r["kB"] ** 2 % Om == Om - 2547 det.append(f"Ω={Om}: k_B c = {r['kB']} · {r['c']} ≡ {r['hbar']} = ħ, ħ² ≡ −1, k_B² ≡ −2")548 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)549 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}")550 # 7:P2 (p07054)551 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))552553554if __name__ == "__main__":555 if len(sys.argv) > 1:556 for b in sys.argv[1:]: R.run_block(b)557 sys.exit(0 if R.summary(write=False) else 1)558 sys.exit(0 if R.verify_all() else 1)559