"""p38_s13 — the ledger file of 38-s13 (ledger migration; 12 October 2026). "The Light Cone of the Minimal Pair" (Akhtman, 2026). The paper's predicate ledger is docs/38-s13/38-s13-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 `# 38:XN ()` marker on the check that decides it (PREDICATES). The checks compute what the paper's validation package computes (src/38-s13: the six in-tree audits of September 2026, check_s13.js, check_o1.js, check_o2.js, check_o3.js, check_phi.py, check_fibrations.py, and the arithmetic of the laboratory's suites), rewritten onto the themes: the pair's arithmetic (frc/subject.py), the sky, the flow and the covering (frc/covering.py), the frame triple and the two fibrations by elements (frc/projective.py), the PPN faces over the rationals (frc/drift.py), and two chart readings (frc/chart.py, frc/chart_gravity.py: the floor at the entailed H₀, the apsidal bound against Mercury). The laboratory (docs/38-s13) stays the chart's own, its suites its own tests; the package stays the paper's published witness until the milestone's release pin retires it. The exact checks call the subject, projective and gravity themes and stay exact (gate G09); the two chart checks carry their tolerances in the verdict and the comparison with Mercury is [data]. The Lean side is lean/FrcCore/Theme/Pair.lean (the window, the leak rate, the joint cycle, the tick arithmetic, the covering parity theorem), the frame triple and the split fibration in Theme/Projective.lean, the nesting bound in Theme/Drift.lean, the kernel-decided instances in lean/FrcCore/S13.lean (core, no axioms), and lean/FrcLedger/Theme/Gravity.lean (the PPN faces and the dictionary over ℚ) with FrcLedger/Theme/Chart.lean (the floor); the certificates are lean/FrcCore/Ledgers/P38S13.lean and lean/FrcLedger/Ledgers/P38S13.lean. python3 -m frc.ledgers.p38_s13 every block, the census; exit 1 if a check fails (≈ 15 s) python3 -m frc.ledgers.p38_s13 E one block (A to F) from frc.ledgers.p38_s13 import R; R.predicate("38:D12") one predicate: its blocks run once per session Blocks: A the pair EXACT (38:A1, A2, A3, A4, A6, A8, B2, C10, C13, X1) B the frame variety EXACT (38:A7, A9, X4, D5) C the cycles EXACT (38:B4, B5, B7, C1, C2, C3, C4, C5, C14) D the sky and the meridians EXACT (38:B1, B3, B6, D1, D2, D3, D6, D7, D8, D9, D13) E the covering parity theorem EXACT (38:D12, D7) F the faces and the floor EXACT, CHART (38:C6, C7, C8, C12, P1, X3, C13) The notebook frc/ledgers/p38_s13.ipynb runs one predicate per cell, the cell's id its key (gate G13). """ import random import sys from fractions import Fraction from math import gcd, isqrt from frc import arith from frc import chart as C from frc import chart_gravity as CG from frc import covering as CV from frc import drift as D from frc import projective as PJ from frc import subject as SB from frc.registry import Registry # ---- generated by ci/make_ledgers.py from docs/38-s13/38-s13-ledger.json; edit the ledger, not this table ---- PAPER = "38-s13" KEYS = {"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 key LEAN = {"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 them # ---- end of the generated table ---- LEAN_ONLY = () # the predicates with a Lean declaration and no python check (gate G12): none P, OM, G, GO = 13, 233, 2, 78 # the pair, the Subject's drive and the Carrier's (38:A1, A4) KAP, S = 3, 58 SHELLS = [5, 13, 17, 29, 37] # the Ω-blind sweep of the covering (38:D7, D12) 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())] EVEN_PAIRS = [(p, Om) for p in range(5, 200) for Om in range(p * p + 1, 3000) if arith.is_prime(p) and p % 8 == 5 and arith.is_prime(Om) and Om % 16 == 1] # κ odd, S ≡ 0 (mod 4), p² < Ω # The paper's predicate ledger (its appendix, predicates cited as 38:XN): the predicate(s) each check witnesses. LEDGER = { "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", "A9": "38:C13", "B1": "38:A7", "B2": "38:A9, 38:X4", "B3": "38:A9, 38:A7", "B4": "38:D5", "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", "C8": "38:C4", "D1": "38:B1", "D2": "38:B3", "D3": "38:B6", "D4": "38:D1", "D5": "38:D2", "D6": "38:D3", "D7": "38:D6", "D8": "38:D7", "D9": "38:D8", "D10": "38:D9", "D11": "38:D13", "E1": "38:D12", "E2": "38:D12", "E3": "38:D12, 38:D7", "F1": "38:C6", "F2": "38:C7", "F3": "38:C8", "F4": "38:C12", "F5": "38:P1, 38:X3", "F6": "38:C13", } BLOCK = {"A": "the pair", # check-id prefix -> the block (the function block_ below) "B": "the frame variety", "C": "the cycles", "D": "the sky and the meridians", "E": "the covering parity theorem", "F": "the faces and the floor"} # the deciding check of each witnessed predicate PREDICATES = { "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", "38:C13": "A9", "38:A7": "B1", "38:A9": "B2", "38:X4": "B2", "38:D5": "B4", "38:B4": "C1", "38:B5": "C2", "38:C14": "C3", "38:B7": "C4", "38:C1": "C5", "38:C2": "C5", "38:C5": "C6", "38:C3": "C7", "38:C4": "C8", "38:B1": "D1", "38:B3": "D2", "38:B6": "D3", "38:D1": "D4", "38:D2": "D5", "38:D3": "D6", "38:D6": "D7", "38:D7": "D8", "38:D8": "D9", "38:D9": "D10", "38:D13": "D11", "38:D12": "E1", "38:C6": "F1", "38:C7": "F2", "38:C8": "F3", "38:C12": "F4", "38:P1": "F5", "38:X3": "F5", } R = Registry("38", "s13", LEDGER, PREDICATES, sources=[__file__]) Fr = Fraction def near(x, y, rel=None, abs_=None): """|x − y| within the stated tolerance, the chart's float x read as a Fraction against rational bounds.""" d = abs(Fr(x) - Fr(y)) return (rel is not None and d <= Fr(rel) * abs(Fr(y))) or (abs_ is not None and d <= Fr(abs_)) def nonsquare(p): return next(a for a in range(2, p) if pow(a, (p - 1) // 2, p) == p - 1) # ---- block A: the pair (38:A1, A2, A3, A4, A6, A8, C10, C13, X1) --------------------------------------------------------- @R.block("A", BLOCK["A"]) def block_A(): adm = SB.admissible(P, OM) k, s, i, g4, g9 = SB.pair(P, OM, G) ok = all(adm.values()) and (k, s) == (KAP, S) and i == 5 and i == (-pow(G, 3, P)) % P and g4 == 3 and g9 == 5 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) == 1 # 38:A1 (p38001) 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, f"admissibility {adm}; (κ, S, i, g⁴, g⁹) = {(k, s, i, g4, g9)}") ok = SB.tower_solution(3) == (1, 1) and SB.tower_solution(5) == (4, 3) and SB.tower_solution(7) == (2, 1) ok &= all(4 * SB.tower_solution(kk)[0] == kk * SB.tower_solution(kk)[1] + 1 for kk in range(1, 200, 2)) 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)) ok &= sorted(SB.fold_image(P, G)) == list(range(1, P)) and len(SB.fold_solutions(KAP)) >= 1 # 38:A2 (p38002) 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, f"solutions at κ = 3, 5, 7: {SB.tower_solution(3)}, {SB.tower_solution(5)}, {SB.tower_solution(7)}") ps = [p for p in range(5, 200) if p % 4 == 1 and arith.is_prime(p)] ok = gcd(12, 14) == 2 and gcd(12, 28) == 4 and pow(5, 2, P) == P - 1 and pow(5, P, P) == 5 for p in ps: sign, q4 = SB.channel(p, None) ok &= sorted(sign) == [1, p - 1] and len(q4) == 4 and all(pow(x, 4, p) == 1 for x in q4) ok &= gcd(p - 1, p + 1) == 2 and gcd(p - 1, 2 * (p + 1)) == 4 # 38:A3 (p38003) 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, f"{len(ps)} shells") q, hb, z8 = SB.carrier_roots(OM, GO) (a, b), (ab, ba) = SB.two_squares(OM) F = SB.fibonacci(13) 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 == OM 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 - 1 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] == 8 # 38:A4 (p38004) 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, f"(q, ħ, ζ₈) = {(q, hb, z8)}; Ω = {a}² + {b}²") reg = {} for Om in (233, 857, 30089): (a, b), (ab, ba) = SB.two_squares(Om) reg[Om] = (a, b, ab * ab % Om == Om - 1, ab + ba == Om) per = {Om: SB.pisano(Om) for Om in (233, 857, 30089)} ok = all(v[2] and v[3] for v in reg.values()) and reg[233][:2] == (13, 8) and reg[857][:2] == (29, 4) ok &= per[233] == 52 and 468 % 52 == 0 and (233 - 1) % 52 != 0 and per[857] == 1716 and 1716 == 2 * (857 + 1) ok &= per[30089] == 30088 and 30088 == 30089 - 1 ok &= pow(5, (233 - 1) // 2, 233) == 232 and pow(5, (857 - 1) // 2, 857) == 856 and pow(5, (30089 - 1) // 2, 30089) == 1 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, f"legs {reg}; Pisano periods {per}") ok = 2 * 7 % P == 1 and (-7) % P == 6 and 2 * 6 % P == P - 1 and 6 * 2 < P < 7 * 2 ok &= all(2 * (2 * ((p - 1) // 4) + 1) % p == 1 for p in ps) # 38:A6 (p38006) 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, "") ok = True for p in (5, 13, 17, 29): k, heights, sym = SB.window(p) ok &= heights == list(range(k + 1)) and all((4 * h < p) == (h <= k) for h in range(p)) and len(sym) == p - 1 ok &= SB.pairwise_conservation(p)[0] ok &= SB.window(P)[1] == [0, 1, 2, 3] and SB.window(P)[2] == list(range(-5, 7)) # 38:A8 (p38008), 38:B2 (p38010) 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, "") ang, per_, om1, cov = SB.leak_rate(P, OM) ang5, per5, _, _ = SB.leak_rate(5, OM) 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) ok &= all(SB.leak_rate(p, Om)[1] == Fr(1, Om - 1) for p, Om in ADMISSIBLE) # 38:C10 (p38044), 38:X1 (p38046) 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, f"{len(ADMISSIBLE)} admissible pairs; κ/S = {ang}, per chronon {per_}") ok = SB.apsidal_bound(P, OM) == (True, True) and D.nesting_bound(P, OM)[:2] == (True, True) 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) ok &= all(SB.apsidal_bound(p, Om) == (False, False) for p, Om in ((53, 157), (13, 157), (17, 233))) # 38:C13 (p38053) 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, f"the difference at (13, 233): {D.nesting_bound(P, OM)[2]} = (233 − 169)·232") # ---- block B: the frame variety (38:A7, A9, X4, D5) ------------------------------------------------------------------------ @R.block("B", BLOCK["B"]) def block_B(): inv = {p: PJ.involutions(p) for p in (5, 13)} 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)) == 2184 ok &= inv[13] == (1, 169) and inv[5] == (1, 25) sph = {p: PJ.sphere_is_sl2(p, r) for p, r in ((5, 2), (13, 5))} ok &= all(v[0] and v[3] and v[1] == v[2] == p * (p * p - 1) for p, v in sph.items()) # 38:A7 (p38007) 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, f"involutions {inv}; sphere {sph}") ok, det = True, [] for p in (5, 13, 17, 7, 11): nu = nonsquare(p) n, d, b, bij = PJ.frame_triple(p, nu) ns = PJ.nonsplit_fibration(p, nu) ok &= bij and n == (p + 1) * p * (p - 1) and d == p + 1 and b == p * (p - 1) ok &= ns["orbit_is_quadric"] and ns["base"] == p * (p - 1) and ns["fibres"] and ns["section"] if p % 4 == 1: # the split fibration by the unit i needs i² = −1, p = 4κ + 1 sp, cen = PJ.split_fibration(p), PJ.centraliser(p) ok &= sp["orbit_is_quadric"] and sp["base"] == p * (p + 1) and sp["fibres_are_cosets"] and sp["borel_whole_or_none"] 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) det.append(f"p={p}: {n} = {d}·{b}, non-split base {ns['base']}, split base {sp['base']}") else: det.append(f"p={p} (≡ 3 mod 4): {n} = {d}·{b}, non-split base {ns['base']}") # 38:A9 (p38050), 38:X4 (p38051) 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, "; ".join(det)) ok = True for p in (5, 13): nu = nonsquare(p) for M in random.Random(38).sample(PJ.pgl2(p), 40): direction, (al, be), chart = PJ.triple(M, nu, p) N = chart[0] 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) 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) != 0 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, "") classes, equi = CV.quarter_classes(P, G) 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()) ok &= 4 * 3 < P < 4 * 4 # 38:D5 (p38029) 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, f"classes {classes}") # ---- block C: the cycles (38:B4, B5, B7, C1–C5, C14) -------------------------------------------------------------------- @R.block("C", BLOCK["C"]) def block_C(): n, L, inj, eq = CV.fibre_product(12, 8, 4) ok = (n, L, inj, eq) == (24, 24, True, True) and 12 * 8 // gcd(12, 8) == 24 and 232 == 8 * 29 ok &= all((s + 12) % 24 != s and (s + 24) % 24 == s for s in range(24)) # 38:B4 (p38012) 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, "") Lc, half, hp, hO = SB.joint_cycle(P, OM) 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 == 1392 ok &= pow(G, 348, P) == 1 and pow(GO, 348, OM) == OM - 1 and pow(G, 696, P) == 1 and pow(GO, 696, OM) == 1 # 38:B5 (p38013) 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, f"L = {Lc}, half = {half}") rng = random.Random(1392) sample = rng.sample(ADMISSIBLE, min(200, len(ADMISSIBLE))) + rng.sample(EVEN_PAIRS, min(200, len(EVEN_PAIRS))) ok = True for p, Om in sample: Lc, half, hp, hO = SB.joint_cycle(p, Om) ok &= Lc == SB.least_return(p, Om) and hp == 0 and hO == (Om - 1) // 2 and Lc % (p - 1) == 0 and Lc % (Om - 1) == 0 ok &= Fr(p - 1, Om - 1) == Fr((p - 1) // 4, (Om - 1) // 4) Lc, half, hp, hO = SB.joint_cycle(17, 233) # the κ-even control: κ = 4 > S's 2-part, the roles swap ok &= Lc == 464 and half == 232 and hp == 8 and hO == 0 # 38:C14 (p38054) 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, f"{len(ADMISSIBLE)} admissible pairs, {len(EVEN_PAIRS)} with S ≡ 0 (mod 4)") rate = CV.composed_rate(P, OM) pairs, Lc, inj, eq = CV.pair_space(P, OM) 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 * 244 ok &= (pairs, Lc, inj, eq) == (696, 696, True, True) # 38:B7 (p38015) 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, f"rate {rate}; pairs {pairs}") 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)) # 38:C1 (p38016), 38:C2 (p38017) 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, "") ok = all(CV.stations(232, k) == (0, 116) for k in range(232)) and 116 == 232 // 2 # 38:C5 (p38020) 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, "") ok = CV.capacity_stations(P) == [1, 2, 3, 10, 11, 12] and 0 not in CV.capacity_stations(P) ok &= all((CV.tick(232, 0, b) + b) % 232 == 0 for b in range(232)) # 38:C3 (p38018) 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, "") 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)) # 38:C4 (p38019) 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, "") # ---- block D: the sky and the meridians (38:B1, B3, B6, D1, D2, D3, D6–D9, D13) --------------------------------------------- @R.block("D", BLOCK["D"]) def block_D(): nodes = CV.node_field(P) ok = len(nodes) == 72 == 3 * 2 * 12 and len({n[2] for n in nodes}) == 12 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)) ok &= all(CV.label(P, G, k, k) == k for k in range(13)) # 38:B1 (p38009) 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, "") m = CV.mounting(P, G) 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) == 3 # 38:B3 (p38011) 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)) i = PJ.unit(P) circ = PJ.circle(P) 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) ok &= PJ.centraliser(P)[1:] == (12, True) # 38:B6 (p38014) 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, "") st = CV.capacity_stations(P) 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)) ok &= all((CV.tick(232, k, b) + b) % 232 == k for b in range(232) for k in st) # 38:D1 (p38025) 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, "") step, rhs, eq, den = CV.step_law() ok = eq and step == Fr(9029, 9048) and den == 9048 and 9048 == 12 * 754 == 13 * 696 == 232 * 39 and 156 == 13 * 12 # 38:D2 (p38026) 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}") per, isn, seam, between = CV.tower_period(P, G) ok = per == 12 and isn and seam == (6, 7) and between # 38:D3 (p38027) 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, "") md = CV.momentum_dual(P, 5) 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] 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)] # 38:D6 (p38030) 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)) law = CV.covering_law(P) 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"] # 38:D7 (p38031) 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)) 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) # 38:D8 (p38032) 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, "") ok = all(CV.fusion()) and (5 * 39 + 13) == 2 * 104 # 38:D9 (p38033) 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, "") fl = CV.family_law(P) ok = all(fl[k] for k in ("M0", "M3", "law", "passages5", "drawn_iff_m_ge_4")) and fl["slots"] == 144 and fl["nodes"] == 72 # 38:D13 (p38037) 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)) # ---- block E: the covering parity theorem (38:D12, D7) ------------------------------------------------------------------- @R.block("E", BLOCK["E"]) def block_E(): ok = all(CV.reflection_identity(p) for p in SHELLS + [7, 11, 41]) 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)) # 38:D12 (p38036) 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, "") ok = CV.parity_table() 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, "") ok, det = True, [] for p in SHELLS: law = CV.covering_law(p) ok &= CV.decider(p) and law["complete"] and law["law"] and law["position"] and law["balance"] k = (p - 1) // 4 ok &= law["nodes"] == 2 * k * (p - 1) and law["slots"] == 4 * k * (p - 1) and law["once"] == law["thrice"] == k * (p - 1) det.append(f"p={p}: {law['nodes']} nodes, {law['slots']} slots") 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, "; ".join(det)) # ---- block F: the faces and the floor (38:C6, C7, C8, C12, P1, X3, C13) ------------------------------------------------------ @R.block("F", BLOCK["F"]) def block_F(): kt = SB.kill_test(53, 3, 157, 5) 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"] ok &= kt["v_O"] == 22 and not kt["kO_divides_kS"] and not kt["in_cube_subgroup"] ok &= kt["core_quarter"] == 28 and kt["inverse"] == 1 and kt["order3"] and kt["idempotent"] == 117 and kt["subject_face"] == 129 ok &= kt["ratio"] == Fr(3, 13) and kt["lcm"] == 156 and kt["half"] == 78 and 12 * 13 == 52 * 3 # 38:C6 (p38021) 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)) ang, per, om1, cov = SB.leak_rate(P, OM) ratio, angular, faces = D.registration_dictionary(KAP, S) ok = ang == Fr(3, 58) == Fr(12, 232) and cov * 12 == Fr(3, 116) and ang / (cov * 12) == 2 and faces == 2 ok &= all(SB.leak_rate(p, Om)[0] / (SB.leak_rate(p, Om)[3] * (p - 1)) == 2 for p, Om in ADMISSIBLE) # 38:C7 (p38022) 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, "") r11 = D.ppn_faces(1, 1) ok = r11 == (Fr(2), True, True, Fr(0)) for b2 in range(-4, 5): for g2 in range(-4, 5): ratio, is2, cond, dev = D.ppn_faces(Fr(b2, 2), Fr(g2, 2)) ok &= (is2 == cond) and dev == Fr(2, 3) * (2 * Fr(g2, 2) - Fr(b2, 2) - 1) bd = {w: D.brans_dicke(w) for w in (Fr(1, 3), 1, 10, 100, 40000)} ok &= all(v[1] == Fr(-2) / (2 + w) != 0 and v[2] == Fr(-4) / (3 * (2 + w)) for w, v in bd.items()) ok &= abs(bd[40000][1]) < Fr(1, 10000) and D.pn_coefficients()["ok"] ok &= abs(D.brans_dicke(19998)[1]) == Fr(1, 10000) and abs(D.brans_dicke(19999)[1]) < Fr(1, 10000) # 38:C8 (p38023) 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, f"Brans–Dicke {bd}") r3, a3, f3 = D.registration_dictionary(3, 58) r1, a1, f1 = D.registration_dictionary(1, 58) ok = (r3, a3, f3) == (58, Fr(3, 58), 2) and (r1, a1, f1) == (174, Fr(1, 58), 2) 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)) # 38:C12 (p38052) 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, "") a0 = C.floor() lo, hi = C.floor_bracket() 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)) ok &= Fr("1.04e-10") < Fr(lo) and Fr(hi) < Fr("1.05e-10") ok &= near(Fr(a0) / Fr(C.A0_FIT[0]), Fr(87, 100), abs_=Fr(1, 100)) # 38:P1 (p38049), 38:X3 (p38048) 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, 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__) ab = CG.apsidal_bound() 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"] > 50 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, f"{ab}", kind="CHART") if __name__ == "__main__": want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK) bad = [b for b in want if b not in BLOCK] if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}") for b in want: R.run_block(b) sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCK) else None) else 1)