The ledger file frc/ledgers/p38_s13.py of Exact Quantum Dynamics on (13,233), rendered with an anchor per line: the marked lines (# 38:C2 (p38010): a predicate and its accession key) are the checks that decide the predicates of the paper's predicate ledger — 41 of 41 checks passing; the predicates' theorems are the declarations of S13 in the core. ▶ run the predicates on Google Colab.
1"""p38_s13 — the ledger file of 38-s13 (ledger migration; 12 October 2026).23"The Light Cone of the Minimal Pair" (Akhtman, 2026). The paper's predicate ledger is docs/38-s13/38-s13-ledger.json.4This file binds its predicates to the framework: the table of keys (generated from the ledger by ci/make_ledgers.py),5and the checks of six blocks. Each check names the predicate(s) it witnesses (LEDGER) under a `# 38:XN (<key>)` marker on6the check that decides it (PREDICATES). The checks compute what the paper's validation package computes (src/38-s13:7the six in-tree audits of September 2026, check_s13.js, check_o1.js, check_o2.js, check_o3.js, check_phi.py,8check_fibrations.py, and the arithmetic of the laboratory's suites), rewritten onto the themes: the pair's arithmetic9(frc/subject.py), the sky, the flow and the covering (frc/covering.py), the frame triple and the two fibrations by10elements (frc/projective.py), the PPN faces over the rationals (frc/drift.py), and two chart readings (frc/chart.py,11frc/chart_gravity.py: the floor at the entailed H₀, the apsidal bound against Mercury). The laboratory (docs/38-s13)12stays the chart's own, its suites its own tests; the package stays the paper's published witness until the milestone's13release pin retires it.1415The exact checks call the subject, projective and gravity themes and stay exact (gate G09); the two chart checks carry16their tolerances in the verdict and the comparison with Mercury is [data]. The Lean side is lean/FrcCore/Theme/Pair.lean17(the window, the leak rate, the joint cycle, the tick arithmetic, the covering parity theorem), the frame triple and the18split fibration in Theme/Projective.lean, the nesting bound in Theme/Drift.lean, the kernel-decided instances in19lean/FrcCore/S13.lean (core, no axioms), and lean/FrcLedger/Theme/Gravity.lean (the PPN faces and the dictionary over ℚ)20with FrcLedger/Theme/Chart.lean (the floor); the certificates are lean/FrcCore/Ledgers/P38S13.lean and21lean/FrcLedger/Ledgers/P38S13.lean.2223 python3 -m frc.ledgers.p38_s13 every block, the census; exit 1 if a check fails (≈ 15 s)24 python3 -m frc.ledgers.p38_s13 E one block (A to F)25 from frc.ledgers.p38_s13 import R; R.predicate("38:D12") one predicate: its blocks run once per session2627Blocks: A the pair EXACT (38:A1, A2, A3, A4, A6, A8, B2, C10, C13, X1)28 B the frame variety EXACT (38:A7, A9, X4, D5)29 C the cycles EXACT (38:B4, B5, B7, C1, C2, C3, C4, C5, C14)30 D the sky and the meridians EXACT (38:B1, B3, B6, D1, D2, D3, D6, D7, D8, D9, D13)31 E the covering parity theorem EXACT (38:D12, D7)32 F the faces and the floor EXACT, CHART (38:C6, C7, C8, C12, P1, X3, C13)3334The notebook frc/ledgers/p38_s13.ipynb runs one predicate per cell, the cell's id its key (gate G13).35"""36import random37import sys38from fractions import Fraction39from math import gcd, isqrt4041from frc import arith42from frc import chart as C43from frc import chart_gravity as CG44from frc import covering as CV45from frc import drift as D46from frc import projective as PJ47from frc import subject as SB48from frc.registry import Registry4950# ---- generated by ci/make_ledgers.py from docs/38-s13/38-s13-ledger.json; edit the ledger, not this table ----51PAPER = "38-s13"52KEYS = {"A1": "p38001", "A2": "p38002", "A3": "p38003", "A4": "p38004", "A5": "p38005", "A6": "p38006", "A7": "p38007", "A8": "p38008", "A9": "p38050", "A10": "p38039", "B1": "p38009", "B2": "p38010", "B3": "p38011", "B4": "p38012", "B5": "p38013", "B6": "p38014", "B7": "p38015", "C1": "p38016", "C2": "p38017", "C3": "p38018", "C4": "p38019", "C5": "p38020", "C6": "p38021", "C7": "p38022", "C8": "p38023", "C10": "p38044", "C11": "p38045", "C12": "p38052", "C13": "p38053", "C14": "p38054", "D1": "p38025", "D2": "p38026", "D3": "p38027", "D4": "p38028", "D5": "p38029", "D6": "p38030", "D7": "p38031", "D8": "p38032", "D9": "p38033", "D10": "p38034", "D11": "p38035", "D12": "p38036", "D13": "p38037", "X1": "p38046", "X2": "p38047", "X3": "p38048", "X4": "p38051", "P1": "p38049"} # every row of the ledger: its label and its accession key53LEAN = {"A1": "core", "A2": "core", "A3": "core", "A4": "core", "A6": "core", "A7": "core", "A8": "core", "A9": "core", "B1": "core", "B2": "core, ml", "B3": "core", "B4": "core", "B5": "core", "B6": "core", "B7": "core", "C1": "core", "C3": "core", "C4": "core", "C5": "core", "C6": "core", "C7": "core, ml", "C8": "ml", "C10": "core", "C13": "core", "C14": "core", "D1": "core", "D2": "core", "D3": "core", "D5": "core", "D6": "core", "D7": "core", "D8": "core", "D9": "core", "D12": "core", "D13": "core", "X1": "core", "X3": "core, ml", "X4": "core", "P1": "ml"} # the rows with a Lean declaration: the libraries whose key files prove them54# ---- end of the generated table ----5556LEAN_ONLY = () # the predicates with a Lean declaration and no python check (gate G12): none5758P, OM, G, GO = 13, 233, 2, 78 # the pair, the Subject's drive and the Carrier's (38:A1, A4)59KAP, S = 3, 5860SHELLS = [5, 13, 17, 29, 37] # the Ω-blind sweep of the covering (38:D7, D12)61ADMISSIBLE = [(p, Om) for p in range(5, 200) for Om in range(p * p + 1, 3000)62 if SB.admissible(p, Om)["p_prime"] and Om % 48 == 41 and arith.is_prime(Om) and all(SB.admissible(p, Om).values())]63EVEN_PAIRS = [(p, Om) for p in range(5, 200) for Om in range(p * p + 1, 3000)64 if arith.is_prime(p) and p % 8 == 5 and arith.is_prime(Om) and Om % 16 == 1] # κ odd, S ≡ 0 (mod 4), p² < Ω6566# The paper's predicate ledger (its appendix, predicates cited as 38:XN): the predicate(s) each check witnesses.67LEDGER = {68 "A1": "38:A1", "A2": "38:A2", "A3": "38:A3", "A4": "38:A4", "A5": "38:A4", "A6": "38:A6", "A7": "38:A8, 38:B2", "A8": "38:C10, 38:X1",69 "A9": "38:C13",70 "B1": "38:A7", "B2": "38:A9, 38:X4", "B3": "38:A9, 38:A7", "B4": "38:D5",71 "C1": "38:B4", "C2": "38:B5, 38:C14", "C3": "38:C14", "C4": "38:B7", "C5": "38:C1, 38:C2", "C6": "38:C5", "C7": "38:C3",72 "C8": "38:C4",73 "D1": "38:B1", "D2": "38:B3", "D3": "38:B6", "D4": "38:D1", "D5": "38:D2", "D6": "38:D3", "D7": "38:D6", "D8": "38:D7",74 "D9": "38:D8", "D10": "38:D9", "D11": "38:D13",75 "E1": "38:D12", "E2": "38:D12", "E3": "38:D12, 38:D7",76 "F1": "38:C6", "F2": "38:C7", "F3": "38:C8", "F4": "38:C12", "F5": "38:P1, 38:X3", "F6": "38:C13",77}7879BLOCK = {"A": "the pair", # check-id prefix -> the block (the function block_<letter> below)80 "B": "the frame variety",81 "C": "the cycles",82 "D": "the sky and the meridians",83 "E": "the covering parity theorem",84 "F": "the faces and the floor"}8586# the deciding check of each witnessed predicate87PREDICATES = {88 "38:A1": "A1", "38:A2": "A2", "38:A3": "A3", "38:A4": "A4", "38:A6": "A6", "38:A8": "A7", "38:B2": "A7", "38:C10": "A8", "38:X1": "A8",89 "38:C13": "A9",90 "38:A7": "B1", "38:A9": "B2", "38:X4": "B2", "38:D5": "B4",91 "38:B4": "C1", "38:B5": "C2", "38:C14": "C3", "38:B7": "C4", "38:C1": "C5", "38:C2": "C5", "38:C5": "C6", "38:C3": "C7",92 "38:C4": "C8",93 "38:B1": "D1", "38:B3": "D2", "38:B6": "D3", "38:D1": "D4", "38:D2": "D5", "38:D3": "D6", "38:D6": "D7", "38:D7": "D8",94 "38:D8": "D9", "38:D9": "D10", "38:D13": "D11",95 "38:D12": "E1",96 "38:C6": "F1", "38:C7": "F2", "38:C8": "F3", "38:C12": "F4", "38:P1": "F5", "38:X3": "F5",97}9899R = Registry("38", "s13", LEDGER, PREDICATES, sources=[__file__])100Fr = Fraction101102103def near(x, y, rel=None, abs_=None):104 """|x − y| within the stated tolerance, the chart's float x read as a Fraction against rational bounds."""105 d = abs(Fr(x) - Fr(y))106 return (rel is not None and d <= Fr(rel) * abs(Fr(y))) or (abs_ is not None and d <= Fr(abs_))107108109def nonsquare(p):110 return next(a for a in range(2, p) if pow(a, (p - 1) // 2, p) == p - 1)111112113# ---- block A: the pair (38:A1, A2, A3, A4, A6, A8, C10, C13, X1) ---------------------------------------------------------114@R.block("A", BLOCK["A"])115def block_A():116 adm = SB.admissible(P, OM)117 k, s, i, g4, g9 = SB.pair(P, OM, G)118 ok = all(adm.values()) and (k, s) == (KAP, S) and i == 5 and i == (-pow(G, 3, P)) % P and g4 == 3 and g9 == 5119 ok &= arith.is_primitive_root(G, P) and i * i % P == P - 1 and g4 * i % P == G and pow(g4, 3, P) == 1 and pow(i, 4, P) == 1120 # 38:A1 (p38001)121 R.check("A1", "the pair (13, 233): p = 4·3 + 1 and Ω = 4·58 + 1 prime, κ = 3 odd, S = 58 ≡ 2 (4), ≡ 1 (3), p² < Ω; the drive g = 2 primitive, i = 5 = −g³ = g⁹ with i² = −1, the rung g⁴ = 3 of order 3, the tower g = 3·5", ok,122 f"admissibility {adm}; (κ, S, i, g⁴, g⁹) = {(k, s, i, g4, g9)}")123 ok = SB.tower_solution(3) == (1, 1) and SB.tower_solution(5) == (4, 3) and SB.tower_solution(7) == (2, 1)124 ok &= all(4 * SB.tower_solution(kk)[0] == kk * SB.tower_solution(kk)[1] + 1 for kk in range(1, 200, 2))125 ok &= all(not any(4 * a == kk * b + 1 for a in range(kk) for b in range(4)) for kk in range(2, 60, 2))126 ok &= sorted(SB.fold_image(P, G)) == list(range(1, P)) and len(SB.fold_solutions(KAP)) >= 1127 # 38:A2 (p38002)128 R.check("A2", "the tower identity C₁₂ = C₄ × C₃ at the instance (the fold iʳ(g⁴)ˢ fills 𝔽₁₃^×) and the general congruence 4a − κb = 1: solvable for every odd κ below 200 ((3κ + 1)/4, 3) or ((κ + 1)/4, 1), (1, 1) at κ = 3, (4, 3) at 5, (2, 1) at 7, and for no even κ below 60", ok,129 f"solutions at κ = 3, 5, 7: {SB.tower_solution(3)}, {SB.tower_solution(5)}, {SB.tower_solution(7)}")130 ps = [p for p in range(5, 200) if p % 4 == 1 and arith.is_prime(p)]131 ok = gcd(12, 14) == 2 and gcd(12, 28) == 4 and pow(5, 2, P) == P - 1 and pow(5, P, P) == 5132 for p in ps:133 sign, q4 = SB.channel(p, None)134 ok &= sorted(sign) == [1, p - 1] and len(q4) == 4 and all(pow(x, 4, p) == 1 for x in q4)135 ok &= gcd(p - 1, p + 1) == 2 and gcd(p - 1, 2 * (p + 1)) == 4136 # 38:A3 (p38003)137 R.check("A3", "the channel at the instance, gcd(12, 14) = 2 and gcd(12, 28) = 4 with N(i) = i² = −1 (i Frobenius-fixed, i¹³ = i), and on every p = 4κ + 1 below 200: C_{p−1} ∩ C_{p+1} = {±1} and C_{p−1} ∩ C_{2(p+1)} = Q₄ by search", ok,138 f"{len(ps)} shells")139 q, hb, z8 = SB.carrier_roots(OM, GO)140 (a, b), (ab, ba) = SB.two_squares(OM)141 F = SB.fibonacci(13)142 ok = arith.is_primitive_root(GO, OM) and (q, hb, z8) == (89, 144, 97) and q * q % OM == OM - 1 and hb * q % OM == 1 and hb + q == OM143 ok &= pow(z8, 2, OM) == q and pow(z8, 8, OM) == 1 and pow(z8, 4, OM) == OM - 1 and pow(GO, 116, OM) == OM - 1144 ok &= (a, b) == (13, 8) and (ab, ba) == (89, 144) and F[13] == 233 and F[12] == 144 and F[11] == 89 and F[7] == 13 and F[6] == 8145 # 38:A4 (p38004)146 R.check("A4", "the Carrier quarter roots on 𝔽₂₃₃ with the drive 78 (primitive): 78⁵⁸ = 89 = h, h² = −1, ħ = 144 = −h, ħh = 1, ħ + h = Ω; the octant ζ₈ = 78²⁹ = 97, ζ₈² = h, ζ₈⁴ = −1; 233 = 13² + 8² with the leg ratios 13/8 = h and 8/13 = ħ, the Fibonacci convergents (F₁₃ = 233, F₁₂ = 144, F₁₁ = 89, F₇ = 13, F₆ = 8)", ok,147 f"(q, ħ, ζ₈) = {(q, hb, z8)}; Ω = {a}² + {b}²")148 reg = {}149 for Om in (233, 857, 30089):150 (a, b), (ab, ba) = SB.two_squares(Om)151 reg[Om] = (a, b, ab * ab % Om == Om - 1, ab + ba == Om)152 per = {Om: SB.pisano(Om) for Om in (233, 857, 30089)}153 ok = all(v[2] and v[3] for v in reg.values()) and reg[233][:2] == (13, 8) and reg[857][:2] == (29, 4)154 ok &= per[233] == 52 and 468 % 52 == 0 and (233 - 1) % 52 != 0 and per[857] == 1716 and 1716 == 2 * (857 + 1)155 ok &= per[30089] == 30088 and 30088 == 30089 - 1156 ok &= pow(5, (233 - 1) // 2, 233) == 232 and pow(5, (857 - 1) // 2, 857) == 856 and pow(5, (30089 - 1) // 2, 30089) == 1157 R.check("A5", "the golden-ratio audit (check_phi, exact): ħ + h = Ω and Ω = a² + b² are forced at every admissible Carrier (233, 857, 30089), the leg ratios are the roots of −1; φ is no residue at 233 (5 a nonresidue, the Fibonacci recursion closes in the extension: 52 | 468) nor at 857 (period 1716 = 2(Ω + 1)) and is one at 30089 (period 30088 = Ω − 1)", ok,158 f"legs {reg}; Pisano periods {per}")159 ok = 2 * 7 % P == 1 and (-7) % P == 6 and 2 * 6 % P == P - 1 and 6 * 2 < P < 7 * 2160 ok &= all(2 * (2 * ((p - 1) // 4) + 1) % p == 1 for p in ps)161 # 38:A6 (p38006)162 R.check("A6", "the FRC algebra half on 𝔽₁₃: 2⁻¹ = 7, −2⁻¹ = 6 (2·6 = −1), the seam 13/2 between the rows 6 and 7; 2⁻¹ = 2S + 1 on every p = 4S + 1 below 200", ok, "")163 ok = True164 for p in (5, 13, 17, 29):165 k, heights, sym = SB.window(p)166 ok &= heights == list(range(k + 1)) and all((4 * h < p) == (h <= k) for h in range(p)) and len(sym) == p - 1167 ok &= SB.pairwise_conservation(p)[0]168 ok &= SB.window(P)[1] == [0, 1, 2, 3] and SB.window(P)[2] == list(range(-5, 7))169 # 38:A8 (p38008), 38:B2 (p38010)170 R.check("A7", "the resolvable window: on p = 5, 13, 17, 29 the symmetric heights number p − 1 and 4|k̂| < p exactly for |k̂| ≤ κ, two window heights sum to at most 2κ < p − 1; at the instance the window {0, ±1, ±2, ±3}", ok, "")171 ang, per_, om1, cov = SB.leak_rate(P, OM)172 ang5, per5, _, _ = SB.leak_rate(5, OM)173 ok = ang == Fr(3, 58) and per_ == Fr(1, 232) == om1 and cov == Fr(1, 464) and ang5 == Fr(1, 58) and per5 == Fr(1, 232)174 ok &= all(SB.leak_rate(p, Om)[1] == Fr(1, Om - 1) for p, Om in ADMISSIBLE)175 # 38:C10 (p38044), 38:X1 (p38046)176 R.check("A8", "the per-chronon leak rate (κ/S)/(p − 1) = 1/(4S) = 1/(Ω − 1) exactly, κ-free: 1/232 at (13, 233) and at (5, 233), the temporal face on the cover 1/464; on every admissible pair below (200, 3000) the rate is 1/(Ω − 1) — the 1/(4S) suppression of X1", ok,177 f"{len(ADMISSIBLE)} admissible pairs; κ/S = {ang}, per chronon {per_}")178 ok = SB.apsidal_bound(P, OM) == (True, True) and D.nesting_bound(P, OM)[:2] == (True, True)179 ok &= all(SB.apsidal_bound(p, Om) == (True, True) and D.nesting_bound(p, Om)[2] == (Om - p * p) * (Om - 1) for p, Om in ADMISSIBLE)180 ok &= all(SB.apsidal_bound(p, Om) == (False, False) for p, Om in ((53, 157), (13, 157), (17, 233)))181 # 38:C13 (p38053)182 R.check("A9", "the apsidal bound κ/S = (p − 1)/(Ω − 1) < 1/(√Ω + 1) is the nesting condition p² < Ω: in root-free form (p − 1)²Ω < (Ω − p)² with the exact difference (Ω − p²)(Ω − 1), it holds on every admissible pair and fails on (53, 157), (13, 157), (17, 233)", ok,183 f"the difference at (13, 233): {D.nesting_bound(P, OM)[2]} = (233 − 169)·232")184185186# ---- block B: the frame variety (38:A7, A9, X4, D5) ------------------------------------------------------------------------187@R.block("B", BLOCK["B"])188def block_B():189 inv = {p: PJ.involutions(p) for p in (5, 13)}190 ok = 14 * 13 * 12 == 2184 == 156 * 14 and 13 * 12 == 156 and 2 * 1092 == 2184 and len(PJ.pgl2(13)) == 2184 and len(PJ.sl2(13)) == 2184191 ok &= inv[13] == (1, 169) and inv[5] == (1, 25)192 sph = {p: PJ.sphere_is_sl2(p, r) for p, r in ((5, 2), (13, 5))}193 ok &= all(v[0] and v[3] and v[1] == v[2] == p * (p * p - 1) for p, v in sph.items())194 # 38:A7 (p38007)195 R.check("B1", "the frame counts: PGL₂(𝔽₁₃) and SL₂(𝔽₁₃) both have 2184 = 14·13·12 = 156·14 elements, the rotation half 1092; the norm-one sphere x² + y² + z² + w² = 1 is SL₂ (the quaternion matrix [[x + ry, z + rw], [−z + rw, x − ry]], r² = −1, has determinant the norm, and the sphere's matrices are exactly those of determinant one, at p = 5 and 13); SL₂ has one involution against PGL₂'s 169 = 13² (25 at p = 5): the sphere is the spin cover, not the variety", ok,196 f"involutions {inv}; sphere {sph}")197 ok, det = True, []198 for p in (5, 13, 17, 7, 11):199 nu = nonsquare(p)200 n, d, b, bij = PJ.frame_triple(p, nu)201 ns = PJ.nonsplit_fibration(p, nu)202 ok &= bij and n == (p + 1) * p * (p - 1) and d == p + 1 and b == p * (p - 1)203 ok &= ns["orbit_is_quadric"] and ns["base"] == p * (p - 1) and ns["fibres"] and ns["section"]204 if p % 4 == 1: # the split fibration by the unit i needs i² = −1, p = 4κ + 1205 sp, cen = PJ.split_fibration(p), PJ.centraliser(p)206 ok &= sp["orbit_is_quadric"] and sp["base"] == p * (p + 1) and sp["fibres_are_cosets"] and sp["borel_whole_or_none"]207 ok &= cen[1] == p - 1 and cen[2] and len(PJ.circle(p)) == p - 1 and PJ.sphere(p, 1) == p * (p + 1) and PJ.sphere(p, nu) == p * (p - 1)208 det.append(f"p={p}: {n} = {d}·{b}, non-split base {ns['base']}, split base {sp['base']}")209 else:210 det.append(f"p={p} (≡ 3 mod 4): {n} = {d}·{b}, non-split base {ns['base']}")211 # 38:A9 (p38050), 38:X4 (p38051)212 R.check("B2", "the two fibrations and the frame triple on p = 5, 13, 17 and on the odd-p controls 7, 11 by elements: every class of PGL₂ is one direction × one Borel class ((p + 1)·p·(p − 1), the triple of X4); the non-split orbit of u (u² = ν) is the quadric a² + bc = ν of p(p − 1) points with fibres C_{p+1} and the Borel a section; the split orbit of the unit i is the quadric a² + bc = −1 of p(p + 1) points (the unit sphere's count), the fibres the cosets of the diagonal centraliser C_{p−1} inside the Borel, no section; the circle x² + y² = 1 has p − 1 points", ok,213 "; ".join(det))214 ok = True215 for p in (5, 13):216 nu = nonsquare(p)217 for M in random.Random(38).sample(PJ.pgl2(p), 40):218 direction, (al, be), chart = PJ.triple(M, nu, p)219 N = chart[0]220 ok &= N != 0 and tuple(N * x % p for x in M) == PJ.mul(PJ.boost(nu, al, be, p), PJ.borel(*chart, p), p)221 ok &= direction == PJ.normal((al, be), p) and PJ.act(M, (1, 0), p) == (M[0], M[2]) and PJ.det(PJ.boost(nu, al, be, p), p) != 0222 R.check("B3", "the triple's factorisation N M = boost(a, c) · borel(N, ab − νcd, det M) with N = a² − νc² ≠ 0, the boost carrying the horizon to the direction M·[1 : 0], on 40 random classes at p = 5 and p = 13", ok, "")223 classes, equi = CV.quarter_classes(P, G)224 ok = equi and classes[1] == [2, 5, 6] and 5 in classes[1] and (P - 1) in classes[2] and all(len(v) == KAP for v in classes.values())225 ok &= 4 * 3 < P < 4 * 4226 # 38:D5 (p38029)227 R.check("B4", "four rays realise the four quarter classes: the cells of 𝔽₁₃^× split by dlog mod 4 into four classes of three, the quarter i = g⁹ in class 1 and −1 = g⁶ in class 2; the quarter fold 13/4 lies between 3 and 4", ok,228 f"classes {classes}")229230231# ---- block C: the cycles (38:B4, B5, B7, C1–C5, C14) --------------------------------------------------------------------232@R.block("C", BLOCK["C"])233def block_C():234 n, L, inj, eq = CV.fibre_product(12, 8, 4)235 ok = (n, L, inj, eq) == (24, 24, True, True) and 12 * 8 // gcd(12, 8) == 24 and 232 == 8 * 29236 ok &= all((s + 12) % 24 != s and (s + 24) % 24 == s for s in range(24))237 # 38:B4 (p38012)238 R.check("C1", "the sky chronon C₂₄ is the fibre product of C₁₂ and C₈ over C₄: 24 class-compatible pairs, the lcm 24 injecting onto them; antipodal at +12, closed at +24; 232 = 8·29", ok, "")239 Lc, half, hp, hO = SB.joint_cycle(P, OM)240 ok = Lc == 696 == SB.least_return(P, OM) and 696 == 58 * 12 == 3 * 232 and half == 348 and hp == 0 and hO == 116 and 2 * 696 == 1392241 ok &= pow(G, 348, P) == 1 and pow(GO, 348, OM) == OM - 1 and pow(G, 696, P) == 1 and pow(GO, 696, OM) == 1242 # 38:B5 (p38013)243 R.check("C2", "the recurrence data: 696 = lcm(12, 232) = 58·12 = 3·232 is the least common return (by search), the spinor 1392 = 2·696; the half event 348 ≡ 0 (12), ≡ 116 (232): the shell home and the Carrier at −1 (78³⁴⁸ = −1)", ok,244 f"L = {Lc}, half = {half}")245 rng = random.Random(1392)246 sample = rng.sample(ADMISSIBLE, min(200, len(ADMISSIBLE))) + rng.sample(EVEN_PAIRS, min(200, len(EVEN_PAIRS)))247 ok = True248 for p, Om in sample:249 Lc, half, hp, hO = SB.joint_cycle(p, Om)250 ok &= Lc == SB.least_return(p, Om) and hp == 0 and hO == (Om - 1) // 2 and Lc % (p - 1) == 0 and Lc % (Om - 1) == 0251 ok &= Fr(p - 1, Om - 1) == Fr((p - 1) // 4, (Om - 1) // 4)252 Lc, half, hp, hO = SB.joint_cycle(17, 233) # the κ-even control: κ = 4 > S's 2-part, the roles swap253 ok &= Lc == 464 and half == 232 and hp == 8 and hO == 0254 # 38:C14 (p38054)255 R.check("C3", f"the joint cycle in general: on {len(sample)} κ-odd pairs below (200, 3000) — the admissible ones (S ≡ 2 mod 4) and the S ≡ 0 (mod 4) pairs — the apsidal fraction (p − 1)/(Ω − 1) = κ/S, the least common return is lcm(p − 1, Ω − 1) with both counters home, and the exact midpoint is (home, (Ω − 1)/2): the Carrier at −1; at the κ-even control (17, 233) the midpoint is (−1, home), the roles swapped", ok,256 f"{len(ADMISSIBLE)} admissible pairs, {len(EVEN_PAIRS)} with S ≡ 0 (mod 4)")257 rate = CV.composed_rate(P, OM)258 pairs, Lc, inj, eq = CV.pair_space(P, OM)259 ok = Fr(1, 232) * 58 == Fr(1, 4) and 58 * 2 == 116 and 232 * 2 == 464 and rate == Fr(61, 696) and 61 * 12 * 232 == 696 * 244260 ok &= (pairs, Lc, inj, eq) == (696, 696, True, True)261 # 38:B7 (p38015)262 R.check("C4", "the frame leak: the tick π/116 reaches π/2 at the quarter station b_C = 58 (58·4 = 232; the halved tick π/232 is its reading on C₄₆₄), the composed rate 1/12 + 1/232 = 61/696, and between two (home, home) events every class-compatible pair (s mod 12, c mod 232) occurs exactly once (696 of them, the lcm injecting)", ok,263 f"rate {rate}; pairs {pairs}")264 ok = all(CV.tick(232, k, k) == 0 and CV.tick(232, k, 116 + k) == 116 for k in range(232))265 ok &= all((CV.tick(232, k, b) + b) % 232 == k for b in range(232) for k in range(13))266 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))267 # 38:C1 (p38016), 38:C2 (p38017)268 R.check("C5", "the one retarded flow law as a tick count on C₂₃₂: row k at clock b stands at (k − b) mod 232 — φ(k) = −(b_C − k)π/116 in units of 2π/232 — the same count on C₁₂, C₂₄, C₂₃₂ and C₄₆₄ (one flow across the representations); the count returns the row at every clock state", ok, "")269 ok = all(CV.stations(232, k) == (0, 116) for k in range(232)) and 116 == 232 // 2270 # 38:C5 (p38020)271 R.check("C6", "the C₄ stations: every row is home at b_C = k and at its parity image (116) at b_C = 116 + k, gauge-free", ok, "")272 ok = CV.capacity_stations(P) == [1, 2, 3, 10, 11, 12] and 0 not in CV.capacity_stations(P)273 ok &= all((CV.tick(232, 0, b) + b) % 232 == 0 for b in range(232))274 # 38:C3 (p38018)275 R.check("C7", "ownership: the origin is no station (the capacity stations are {1, 2, 3, 10, 11, 12}) and at every clock state its count is the clock's own: the rays anchor at the Observer", ok, "")276 ok = all(all(CV.half_turn(232, x)) for x in range(464)) and all(all(CV.half_turn(m, x)) for m in (6, 12, 116) for x in range(2 * m))277 # 38:C4 (p38019)278 R.check("C8", "the half turn on C₄₆₄ is the point reflection: two half turns are the identity, the reflection x ↦ 464 − x is the negation, the rim 232 is its own reflection (the rim kiss); the same on C₁₂, C₂₄, C₂₃₂", ok, "")279280281# ---- block D: the sky and the meridians (38:B1, B3, B6, D1, D2, D3, D6–D9, D13) ---------------------------------------------282@R.block("D", BLOCK["D"])283def block_D():284 nodes = CV.node_field(P)285 ok = len(nodes) == 72 == 3 * 2 * 12 and len({n[2] for n in nodes}) == 12286 ok &= all(CV.label(P, G, k, t + 1) == G * CV.label(P, G, k, t) % P and CV.label(P, G, k, t + 12) == CV.label(P, G, k, t) for k in range(13) for t in range(12))287 ok &= all(CV.label(P, G, k, k) == k for k in range(13))288 # 38:B1 (p38009)289 R.check("D1", "the node field 72 = 3·2·12 (three shells, two routes, twelve rows) and the retarded labels k·g^{t−k}: every row's label advances by the drive each chronon, returns after twelve, and reads the cell itself one chronon of lookback per row", ok, "")290 m = CV.mounting(P, G)291 ok = m["dlog3"] == 4 and m["order3"] and m["steps120"] == 8 and m["quarter_blind"] == (0, 0, 1) and m["count"] and pow(G, 4, P) == 3292 # 38:B3 (p38011)293 R.check("D2", "the mounting: ×3 = g⁴ (dlog 3 = 4, four drive steps, 3³ = 1), 120° = 8 steps of C₂₄, quarter-blind (8 ≡ 4 ≡ 0 mod 4, 4 ≡ 1 mod 3); the count 3·48 + 12 = 156 = 13·12", ok, str(m))294 i = PJ.unit(P)295 circ = PJ.circle(P)296 ok = i == (5, 0, 0, 8) and len(circ) == 12 and all(PJ.det((x + 5 * y, 0, 0, x - 5 * y), P) == 1 for x, y in circ)297 ok &= PJ.centraliser(P)[1:] == (12, True)298 # 38:B6 (p38014)299 R.check("D3", "the Hopf representation's exact content: the unit i = diag(5, −5) on 𝔽₁₃, the circle x² + y² = 1 has 12 points and lands in the diagonal torus with determinant 1 (x + yi ↦ diag(x + 5y, x − 5y)), the centraliser of i is that torus (12 classes); the drawn leaves are the chart's (A10)", ok, "")300 st = CV.capacity_stations(P)301 ok = st == [1, 2, 3, 10, 11, 12] and all((4 * min(t, P - t) < P) == (t in st) for t in range(1, P))302 ok &= all((CV.tick(232, k, b) + b) % 232 == k for b in range(232) for k in st)303 # 38:D1 (p38025)304 R.check("D4", "the capacity stations 4d < 13 select {1, 2, 3, 10, 11, 12}; the flow law threads every station on all 232 clock states (the tick from b to the station's home returns the station, the identity of C1)", ok, "")305 step, rhs, eq, den = CV.step_law()306 ok = eq and step == Fr(9029, 9048) and den == 9048 and 9048 == 12 * 754 == 13 * 696 == 232 * 39 and 156 == 13 * 12307 # 38:D2 (p38026)308 R.check("D5", "the step law 11π/12 + π/13 + π/232 = π − (π/156 − π/232) as exact fractions: 9029/9048 both sides, 9048 = lcm(12, 13, 232), 156 = 13·12", ok, f"{step}")309 per, isn, seam, between = CV.tower_period(P, G)310 ok = per == 12 and isn and seam == (6, 7) and between311 # 38:D3 (p38027)312 R.check("D6", "the scale-tower circuit: the period is the drive's own 4κ = 12 = p − 1 (no shorter return), with the seam 13/2 between the rows 6 and 7; the radius is the drawing chart's (A10)", ok, "")313 md = CV.momentum_dual(P, 5)314 ok = pow(G, 9, P) == 5 == (-pow(G, 3, P)) % P and [r for _, r, _ in md] == [5, 10, 11, 2, 3, 8] and [f for _, _, f in md] == [0, 0, 1, 1, 0, 0]315 ok &= all(CV.tent(P, u + 26) == CV.tent(P, u) for u in range(300)) and CV.passages(P, 5) == [Fr(13, 5), Fr(52, 5)]316 # 38:D6 (p38030)317 R.check("D7", "the momentum dual M₃ at winding 5 = g⁹ = −g³: stations at the rows 5, 10, 11 (direct) and 2, 3, 8 (echo) on the tent shells, the route flipping on the odd sheets (t = 3, 10), the C₂₆ fold, the drawn passages 13/5 and 52/5", ok, str(md))318 law = CV.covering_law(P)319 ok = law["nodes"] == 72 and law["slots"] == 144 and law["complete"] and law["law"] and law["once"] == 36 and law["thrice"] == 36 and law["sum"] == 144 and law["balance"]320 # 38:D7 (p38031)321 R.check("D8", "the covering: 144 slots (twelve windings, two rays, six stations) cover the 72 nodes completely, multiplicity 1 on the odd rows and 3 on the even, 36 once and 36 thrice, 144 = 36 + 108, direct and echo slots balanced", ok, str(law))322 ok = all(CV.ramification(P, m) == (Fr(13, 2 * m), True) for m in range(2, 13)) and CV.ramification(P, 1) == (Fr(13, 2), False)323 # 38:D8 (p38032)324 R.check("D9", "the half-cell ramification t_{1/2} = 13/(2m) lies in the drawn first segment for every sibling m ≥ 2 and not for M₀ (13/2, the seam, at the origin)", ok, "")325 ok = all(CV.fusion()) and (5 * 39 + 13) == 2 * 104326 # 38:D9 (p38033)327 R.check("D10", "the horizon fold fusion 5·39 ≡ −13 (mod 104): 5·39 + 13 = 208 = 2·104, 104 = 8·13, 39 = 3·13; eight ray ends fuse into four points", ok, "")328 fl = CV.family_law(P)329 ok = all(fl[k] for k in ("M0", "M3", "law", "passages5", "drawn_iff_m_ge_4")) and fl["slots"] == 144 and fl["nodes"] == 72330 # 38:D13 (p38037)331 R.check("D11", "the family law: the one meridian law has winding 1 as M₀ (rows t, no flip) and winding 5 as M₃, its 24 drawn curves place 144 stations on the 72 nodes with the parity multiplicities, the drawn passages of winding 5 are 13/5 and 52/5, and a passage is drawn exactly for m ≥ 4", ok, str(fl))332333334# ---- block E: the covering parity theorem (38:D12, D7) -------------------------------------------------------------------335@R.block("E", BLOCK["E"])336def block_E():337 ok = all(CV.reflection_identity(p) for p in SHELLS + [7, 11, 41])338 ok &= all(a * b // p + (p - a) * b // p == b - 1 for p in (101, 233) for a in range(1, p) for b in range(1, p, 7))339 # 38:D12 (p38036)340 R.check("E1", "the reflection identity ⌊ab/p⌋ + ⌊(p − a)b/p⌋ = b − 1 for all 0 < a, b < p on p = 5, 7, 11, 13, 17, 29, 37, 41 and sampled on 101, 233", ok, "")341 ok = CV.parity_table()342 R.check("E2", "the eight-case parity table (Lemma all-shell parity): with k̄ = ā M̄ + α the four candidates match iff α = 0, α = ā, α = M̄, α = 1 + ā + M̄; μ = 3 iff k̄ = 0, μ ∈ {1, 3}, and on an odd row the match is direct iff ā = 1", ok, "")343 ok, det = True, []344 for p in SHELLS:345 law = CV.covering_law(p)346 ok &= CV.decider(p) and law["complete"] and law["law"] and law["position"] and law["balance"]347 k = (p - 1) // 4348 ok &= law["nodes"] == 2 * k * (p - 1) and law["slots"] == 4 * k * (p - 1) and law["once"] == law["thrice"] == k * (p - 1)349 det.append(f"p={p}: {law['nodes']} nodes, {law['slots']} slots")350 R.check("E3", "the decider at every shell of p = 5, 13, 17, 29, 37: the four candidate wraps satisfy the four reflection identities and aM = pA + k, μ = 3 iff k even, μ ∈ {1, 3}, the odd sector's match direct iff the shell is odd, and μ equals the constructed covering's multiplicity on every node — the law is the pair structure, not the instance", ok,351 "; ".join(det))352353354# ---- block F: the faces and the floor (38:C6, C7, C8, C12, P1, X3, C13) ------------------------------------------------------355@R.block("F", BLOCK["F"])356def block_F():357 kt = SB.kill_test(53, 3, 157, 5)358 ok = 3 * 232 == 58 * 12 and 53 == 4 * 13 + 1 and kt["Om_form"] and kt["S"] == 39 and 39 % 4 == 3 and kt["primitive"]359 ok &= kt["v_O"] == 22 and not kt["kO_divides_kS"] and not kt["in_cube_subgroup"]360 ok &= kt["core_quarter"] == 28 and kt["inverse"] == 1 and kt["order3"] and kt["idempotent"] == 117 and kt["subject_face"] == 129361 ok &= kt["ratio"] == Fr(3, 13) and kt["lcm"] == 156 and kt["half"] == 78 and 12 * 13 == 52 * 3362 # 38:C6 (p38021)363 R.check("F1", "the dilation instance 3/58 = 12/232 and the (53, 13) kill test in the auxiliary modulus 157 (53 = 4·13 + 1; S = 39 ≡ 3 mod 4, not admissible): 5 primitive mod 157, v_O = 5¹³ = 22 outside ⟨5³⟩ (3 ∤ 13; 22⁵² ≠ 1), 22⁹ = 28 = 5⁻³⁹, 22⁴ of order 3, 117·13 ≡ 117 (156), 5³⁹ = 129, 12/52 = 3/13, lcm(12, 52) = 156 with the half event 78", ok, str(kt))364 ang, per, om1, cov = SB.leak_rate(P, OM)365 ratio, angular, faces = D.registration_dictionary(KAP, S)366 ok = ang == Fr(3, 58) == Fr(12, 232) and cov * 12 == Fr(3, 116) and ang / (cov * 12) == 2 and faces == 2367 ok &= all(SB.leak_rate(p, Om)[0] / (SB.leak_rate(p, Om)[3] * (p - 1)) == 2 for p, Om in ADMISSIBLE)368 # 38:C7 (p38022)369 R.check("F2", "the two faces of the leak: the angular face κ/S = 12/232 = 3/58 (one Carrier tick per chronon) and the temporal face κ/(2S) = 12/464 = 3/116 (the halved tick on C₄₆₄), ratio exactly 2 on the instance and on every admissible pair", ok, "")370 r11 = D.ppn_faces(1, 1)371 ok = r11 == (Fr(2), True, True, Fr(0))372 for b2 in range(-4, 5):373 for g2 in range(-4, 5):374 ratio, is2, cond, dev = D.ppn_faces(Fr(b2, 2), Fr(g2, 2))375 ok &= (is2 == cond) and dev == Fr(2, 3) * (2 * Fr(g2, 2) - Fr(b2, 2) - 1)376 bd = {w: D.brans_dicke(w) for w in (Fr(1, 3), 1, 10, 100, 40000)}377 ok &= all(v[1] == Fr(-2) / (2 + w) != 0 and v[2] == Fr(-4) / (3 * (2 + w)) for w, v in bd.items())378 ok &= abs(bd[40000][1]) < Fr(1, 10000) and D.pn_coefficients()["ok"]379 ok &= abs(D.brans_dicke(19998)[1]) == Fr(1, 10000) and abs(D.brans_dicke(19999)[1]) < Fr(1, 10000)380 # 38:C8 (p38023)381 R.check("F3", "the face-ratio identity over ℚ: the PPN face ratio (2/3)(2 + 2γ − β) equals 2 exactly when 2γ − β = 1, with deviation (2/3)(2γ − β − 1), on the half-integer lattice |β|, |γ| ≤ 2; the exponential metric β = γ = 1 (the series of frc.drift.pn_coefficients) satisfies it; Brans–Dicke's 2γ − β − 1 = −2/(2 + ω) is nonzero at every finite ω (deviation −4/(3(2 + ω))) and below 10⁻⁴ exactly past ω = 19 998", ok,382 f"Brans–Dicke {bd}")383 r3, a3, f3 = D.registration_dictionary(3, 58)384 r1, a1, f1 = D.registration_dictionary(1, 58)385 ok = (r3, a3, f3) == (58, Fr(3, 58), 2) and (r1, a1, f1) == (174, Fr(1, 58), 2)386 ok &= all(D.registration_dictionary(k, s)[0] == Fr(3 * s, k) and D.registration_dictionary(k, s)[1] == Fr(k, s) for k in (1, 3, 5, 7) for s in (10, 58, 602140))387 # 38:C12 (p38052)388 R.check("F4", "the laboratory dictionary: matching the temporal face κ/(2S) to the clock deficit (3/2) r_g/p_sl gives p_sl/r_g = 3S/κ (58 at (13, 233), 174 at (5, 233)), one relation homogeneous of degree 0, under which the angular face 3 r_g/p_sl = κ/S is C7's identity automatically", ok, "")389 a0 = C.floor()390 lo, hi = C.floor_bracket()391 ok = near(a0, Fr("1.042e-10"), rel=Fr(1, 100)) and near(a0, lo, rel=Fr(1, 10 ** 12)) and near(a0, hi, rel=Fr(1, 10 ** 12))392 ok &= Fr("1.04e-10") < Fr(lo) and Fr(hi) < Fr("1.05e-10")393 ok &= near(Fr(a0) / Fr(C.A0_FIT[0]), Fr(87, 100), abs_=Fr(1, 100))394 # 38:P1 (p38049), 38:X3 (p38048)395 R.check("F5", "the floor a₀ = cH₀/2π at the entailed H₀ = 67.4 km s⁻¹ Mpc⁻¹: 1.04 × 10⁻¹⁰ m s⁻² within the bracket of the chart theme, 13 % below the fitted 1.20 × 10⁻¹⁰ [data]; the leak's cyclic rate is the drive's own, one cycle per Ω − 1 chronons (X3)", ok,396 f"a₀ = {a0:.9e} m s⁻², bracket ({'%.9e' % lo}, {'%.9e' % hi})", kind="CHART") # the bracket's Fractions printed through %-formatting (Python 3.10 has no Fraction.__format__)397 ab = CG.apsidal_bound()398 ok = near(ab["log10_bound"], Fr(-616, 10), abs_=Fr(1, 10)) and near(ab["orders_above"], Fr(545, 10), abs_=Fr(5, 10)) and ab["orders_above"] > 50399 R.check("F6", "the apsidal bound on the physical Carrier (ln Ω = 283.5): 1/(√Ω + 1) is 10⁻⁶¹·⁶, and Mercury's apsidal fraction 8.0 × 10⁻⁸ per revolution [data] sits 54 orders above it: no hosted Subject registers an observed precession", ok,400 f"{ab}", kind="CHART")401402403if __name__ == "__main__":404 want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)405 bad = [b for b in want if b not in BLOCK]406 if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")407 for b in want: R.run_block(b)408 sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCK) else None) else 1)409