src/10-dimensions — dimensions.py

1"""2dimensions.py — the validation package of "Dimensional Analysis over Finite Holographic Substrate" (Akhtman, 2026; Preprints3doi 10.20944/preprints202605.0668.v1), the paper 10-dimensions of the FRC corpus (finite-ring-space/src/10-dimensions); one4script since 24 September 2026 (the registry dimcommon.py and the suites verify_domains.py, check_lift.py merged).5========================================================================================================================67One script, two blocks, thirteen family checks of 226 exact micro-checks, standard library only. Every check is exact:8integers, residues, exact rationals; no floats, no random sampling. Block dom (verify_domains) is organised in eight layers9A–H, each a family of micro-checks; block lift (check_lift) decides the five claims L1–L5 of Proposition `lift` on two shells10and two Carriers. A family is one check of the registry, identified as <block>.<family> (dom.A … dom.H, lift.L1 … lift.L5),11and names the predicate(s) of the paper's ledger it witnesses (LEDGER; predicates cited as 10:<label>) — the deciding12family's `# 10:<label> (<key>)` marker is what the ledger's source column links (PREDICATES;13finitering.space/src/10-dimensions/#<key>); the family checks are listed on the public page from14results.json. Master-ledger predicates reached through the paper predicates: 00:D7 (10:D7), 00:C12 (10:F3), 00:C13 (10:E9,1510:G2), 00:C8 (10:E4), 00:B10 (10:E5).1617    python3 dimensions.py         both blocks, results.json written; exit 1 if a family check fails (≈ 1 s)18    python3 dimensions.py lift    one block (dom or lift); no results.json19    from frc_10_dimensions import predicate; predicate("10:C5")    one predicate: its block runs once per session2021The manuscript's 105 source gates (validation/check_gates.py in the corpus tree, where sections/*.tex live) are not part22of this package.23"""24import os, json, sys25from collections import OrderedDict26from fractions import Fraction as Fr27from math import gcd2829SCRIPT = os.path.splitext(os.path.basename(__file__))[0]        # "dimensions": the one script, the name results.json and the site pages carry3031RESULTS = []32MICRO = []             # (block, family, label, ok)3334LEDGER = {35    "dom.A": "10:C2, 10:C3, 10:D2, 10:D6, 10:F2, 10:F4, 10:G1, 10:G3, 10:X1, 10:X3",36    "dom.B": "10:E2, 10:E3, 10:X1, 10:X2, 10:X3",37    "dom.C": "10:E4",38    "dom.D": "10:E4, 10:E5, 10:E9, 10:F3, 10:G1, 10:P2, 10:X2",39    "dom.E": "10:C5",40    "dom.F": "10:C5, 10:D1",41    "dom.G": "10:C5, 10:D2, 10:F5, 10:G2, 10:G4, 10:G5, 10:P1, 10:X4",42    "dom.H": "10:E4, 10:E5",43    "lift.L1": "10:D3", "lift.L2": "10:D3", "lift.L3": "10:D3", "lift.L4": "10:D3", "lift.L5": "10:C5, 10:D3",44}4546LABELS = {47    "dom.A": "shell datum and domain algebra on F_13: frame datum (g = 2, i = −g^κ, π = 2κ, 4κ = p−1); the group law, inverses and grading of D_p = Z_p × Z_{p−1}; the internal flag I_q = [T]^κ unique of order four, no flag of space, horizon-inaccessible, covariant; realization a homomorphism; the derived domains (m, F, S, G, Compton, Planck area, Schwarzschild, orbital frequency); fibrewise addition and local recovery at H = 5; the energy–momentum relation in one fibre at crossing degree two",48    "dom.B": "the quartet at the unit face: exponent-vector relation lattice over {ℓ_P, t_P, ħ} (both faces of c and ħ differ by ℓp = tE; rank two; k_B and ℓE add nothing); exact-rational instantiation of every stated equality (|k_B|c = ħ, m_P, G, Θ_P, {c, ħ, G} ↔ quartet); 4 − 1 = 3 degrees of freedom; flag positions (0,0,1,1)",49    "dom.C": "the defining congruences on the lab Carrier Ω = 2 408 561 (S = 602 140): admissibility; 2G ≡ −1 unique; ħ² ≡ −1, k_B² ≡ −2, 2c² ≡ 1 with their exact root pairs; G ≡ −c², G² ≡ 4⁻¹, h ≡ −ħ; m_P² ≐ Ω ≡ 0",50    "dom.D": "both Carriers (233 and the lab Carrier): the congruence-and-closure system, ħcG⁻¹ landing in the k_B pair; the representative annex; the admissibility minimality scan certifying (13, 233) with the counterfactuals; the constancy prediction P2 against the imported drift bound; [Θ] = [L][T]⁻² and the Unruh closure; the crossing-degree embedding injective and windowed-faithful",51    "dom.E": "covariance: the naive character ill-defined on the modular projection; (p−1, 0) trivial character yet non-neutral; the ε-composition failure; window covariance below the bound; pushforward-invariant labels {0, π}; the quarter-turn fix/swap criterion ε ≡ ±1 (mod 4); the index-two sublattice ⟨c, ħ, G⟩ (det −2)",52    "dom.F": "the (0, π) witness forcing H < 2κ; the σ-twisted action equivariant by full sweep on p = 13 and 229 with the plain-lift failure; σ multiplicative mod 4; δ_S, δ_C involutions, δ_C carrying [L] ↦ [p], [T] ↦ [E]",53    "dom.G": "realized action against the Z³-representative failure; the flagged label (0, 0; 1) moving under ε = −1; the window ladder 2√κ < κ/2 < κ < 2κ nested for every κ ≥ 17 and failing for κ = 3; (2√κ)² = p−1, (2√S)² = Ω−1; the flagged ratio F/a; meridian transport (L T^κ)^p = I_q on three shells; both roots on both Carriers; Buckingham's count on the integer lift (the pendulum: rank 3, one product); the resolution floor Ω^(−1/4) of order 1e−31 on the chart value, thirteen orders below 1e−18 and twenty-six below 2.2e−5, 102 bits against the 67 of the finest differential frequency comparison (the finest interspecies ratio, 58), the maximal coherent count Ω^(1/4) and the clock-bound crossover t* = t_P Ω^(3/8) ≈ 730 s (the prediction P1); the electromagnetic domain — [q]² = I_q[L][T]⁻¹, its two roots on the odd capacities and none on the even, the meridian half-turn, the even labels on the lift, the dilation character",54    "dom.H": "the pair layer: pair multiplication well defined; the linkage {±k_B}{±c} = {±ħ} derived at pair level; ħcG⁻¹ in the k_B pair via (ħcG⁻¹)² ≡ −2; representative inertness — exactly the four assignments with σ_ħ = σ_c σ_k admissible, a (Z/2)², every identity holding on each; the ħ-flip relabelling of {ħ, h}",55    "lift.L1": "operator four-cycle: F = iW on F_p^{p−1}, F² = J, F⁴ = I, F² ≠ I (p = 13, 173)",56    "lift.L2": "chart shadow of order two: F exchanges the two dual charts, J exchanges none; the cardinal skeleton acts on charts as s mod 2",57    "lift.L3": "record map s ↦ I_q^s an isomorphism Z_4 → the flag subgroup {0, κ, 2κ, 3κ}; the quotient by {0, 2κ} returns s mod 2",58    "lift.L4": "Carrier face: ħ² = −1 (mod Ω), ħ⁴ = 1, ħ² ≠ 1 — the crossing quantum has order four, never two (Ω = 233, 2 408 561)",59    "lift.L5": "invariance on the realized lattice: {u : εu = u for every admissible ε} = {0, 2κ}; witnesses (κ,1) ↦ 2κ and (−κ,1) ↦ 0 invariant, (0,1) ↦ κ not, (0,2) ↦ 2κ invariant",60}6162BLOCK = {"dom": "the eight layers A–H of exact micro-checks (verify_domains until 24 September 2026)",      # check-id prefix -> the block (the function block_<name> below)63         "lift": "Proposition `lift`, L1–L5 on two shells and two Carriers (check_lift)"}6465# the deciding family of each witnessed predicate: the one whose checks decide the predicate's statement (the other families66# that touch it are corroboration, listed by predicate() from the records)67PREDICATES = {68    "10:C2": "dom.A", "10:C3": "dom.A", "10:C5": "dom.E", "10:D1": "dom.F", "10:D2": "dom.A", "10:D3": "lift.L1",69    "10:D6": "dom.A", "10:E2": "dom.B", "10:E3": "dom.B", "10:E4": "dom.C", "10:E5": "dom.H", "10:E9": "dom.D",70    "10:F2": "dom.A", "10:F3": "dom.D", "10:F4": "dom.A", "10:G1": "dom.A", "10:G2": "dom.G", "10:G3": "dom.A",71    "10:F5": "dom.G", "10:G4": "dom.G", "10:G5": "dom.G", "10:P1": "dom.G", "10:P2": "dom.D",72    "10:X1": "dom.B", "10:X2": "dom.D", "10:X3": "dom.A", "10:X4": "dom.G",       # block X restates E2/F2, E3/F3, D2/E2, F5: the same deciding checks73}74_FAM = [None, None]75_RAN = set()                                            # blocks already run in this session (predicate() runs each once)7677def markers():78    """predicate label -> (script file, line) of its marker `# <paper>:<label> (<key>)`: the line of the check that decides it."""79    import re80    out = {}81    for i, line in enumerate(open(os.path.abspath(__file__), encoding="utf-8"), 1):82        m = re.match(r"\s*# ((?:\d+:[A-Z]+\d+[a-z]?(?: \(p\d{5}\))?)(?:, \d+:[A-Z]+\d+[a-z]?(?: \(p\d{5}\))?)*)\s*$", line)83        if m:84            for lab in re.findall(r"\d+:[A-Z]+\d+[a-z]?", m.group(1)): out.setdefault(lab, (SCRIPT + ".py", i))85    return out8687def _run_block(name):88    if name not in _RAN:89        globals()[f"block_{name}"](); _RAN.add(name)9091def predicate(label, lines=14):92    """Verify one ledger predicate: run the blocks of the families that cite it (each once per session), print the deciding93    check's source (from its marker) and every family record that cites the predicate, and return True iff all pass."""94    fam = PREDICATES.get(label)95    if fam is None:96        print(f"{label}: no python witness (see the predicate's Lean witness or its source)"); return None97    citing = {f.split(".")[0] for f, rows in LEDGER.items() if label in [t.strip() for t in rows.split(",")]}98    for b in sorted({fam.split(".")[0]} | citing): _run_block(b)     # the deciding block and every block whose families cite the predicate99    mk = markers().get(label)100    if mk:101        src = open(os.path.abspath(__file__), encoding="utf-8").read().split("\n")102        print(f"— {mk[0]}:{mk[1]} (the check that decides {label}; family {fam})")103        for j in range(mk[1] - 1, min(mk[1] - 1 + lines, len(src))): print(f"{j + 1:5d}  {src[j]}")104    else:105        print(f"— {SCRIPT}.py, block {fam.split('.')[0]} (the whole block witnesses {label})")106    recs = [r for r in RESULTS if label in [t.strip() for t in r["rows"].split(",")]]107    ok = all(r["ok"] for r in recs)108    for r in recs:109        role = "(deciding)" if r["id"] == fam else "(corroborating)"110        print(f"  [{'PASS' if r['ok'] else 'FAIL'}] {r['id']:8s} {role:16s} {r['detail']}")111    print(f"{label}: {'VERIFIED' if ok and recs else 'FAILED'} — {len(recs)} family record(s)")112    return ok113114def verify_all():115    """Run every block (those already run in this session are not re-run) and print the summary; True iff every family check passed."""116    for b in sorted(BLOCK): _run_block(b)117    return summary(write=False)118119def family(tag, fam):120    _FAM[0], _FAM[1] = tag, fam121122def chk(label, ok, tag=None, fam=None):123    """A micro-check, recorded under the current (block, family); never exits."""124    MICRO.append((tag or _FAM[0], fam or _FAM[1], label, bool(ok)))125    if not ok:126        print(f"    FAIL: {label}")127128def flush(tag, order=None):129    fams = OrderedDict()130    for t, fam, label, ok in MICRO:131        if t == tag:132            fams.setdefault(fam, []).append(ok)133    for fam in (order or fams):134        oks = fams.get(fam, [])135        check(f"{tag}.{fam}", ok=bool(oks) and all(oks), detail=f"{len(oks)} exact micro-checks")136137def check(pid, ok, detail="", kind="EXACT", label=None):138    """Record one family check. pid = <block>.<family>; LEDGER[pid] = the paper predicate(s) it witnesses."""139    ok = bool(ok)140    rows = LEDGER.get(pid, "")141    label = label or LABELS.get(pid, pid)142    RESULTS.append({"id": pid, "rows": rows, "block": pid.split(".")[0], "script": SCRIPT, "label": label, "ok": ok, "detail": detail, "kind": kind})143    print(f"  [{'PASS' if ok else 'FAIL'}] {pid:8s} {kind:5s} [{rows}] {label[:110]}" + (f"  --  {detail}" if detail else ""))144    return ok145146def summary(write=True):147    n_ok = sum(r["ok"] for r in RESULTS)148    print(f"\nSUMMARY: {n_ok}/{len(RESULTS)} checks passed ({len(MICRO)} exact micro-checks)" + ("" if n_ok == len(RESULTS) else "  <-- FAILURES"))149    if write:150        with open("results.json", "w") as f:151            json.dump(RESULTS, f, indent=1, ensure_ascii=False)152    return n_ok == len(RESULTS)153154# ------------------------------------------------------------------------------------------------------------155# block dom — verify_domains: exact-arithmetic verification for 10-dimensions (quartet edition)156# (quartet edition).157#158# Layers:159#   A. shell datum and domain algebra (F13 working shell): group law, grading,160#      fibrewise addition, neutral criterion, local recovery, flag arithmetic161#   B. the quartet at the unit face (symbolic, exact rationals over free162#      exponents): action identity, pairing closure rank, cancellation identity,163#      mechanical table re-derivation164#   C. the defining congruences on the lab Carrier (S = 602,140, Omega = 2,408,561): existence,165#      exhaustive root enumeration, root pairs, register identities166#   H. pair layer (round 05): pair-well-definedness of every congruence identity and167#      the representative-inertness sweep over all admissible sign assignments168#169# Every check is integer or exact-rational arithmetic; no floats, no RNG170# (the window-ladder orderings are compared by integer squares).171# Domains are triples (r mod p, s mod p-1, n mod 4): free [L],[T] exponents172# and the flag.173def block_dom():174    """Block dom — verify_domains: the eight layers A–H of exact micro-checks, one family check each (dom.A … dom.H)."""175    # A. shell datum and domain algebra on F13176    family('dom', 'A')177    P = 13178    KAPPA = (P - 1) // 4179    G13 = 2180181    order = next(k for k in range(1, P) if pow(G13, k, P) == 1)182    chk("g=2 primitive on F13 (order 12)", order == P - 1)183184    I13 = (-pow(G13, KAPPA, P)) % P185    chk("i = -g^kappa = 5", I13 == 5)186    chk("i = g^{-kappa}", I13 == pow(G13, (P - 1) - KAPPA, P))187    chk("i^2 = -1", (I13 * I13) % P == P - 1)188    PI13 = 2 * KAPPA189    chk("pi = 2 kappa = 6", PI13 == 6)190    chk("e = g^i = 6", pow(G13, I13, P) == 6)191    chk("g^pi = -1", pow(G13, PI13, P) == P - 1)192    chk("2 pi = p-1 == -1 (mod p)", (2 * PI13) % P == P - 1)193    chk("phase-cycle order p-1 = 4 kappa = 2 pi", P - 1 == 4 * KAPPA == 2 * PI13)194195    # capacity is a size: budget statement only (count-per-count), no duration196    chk("capacity budget: quarter cycle holds kappa steps", 4 * KAPPA == P - 1)197198    # 10:C2 (p10012)199    # domain group D_p = Z_p x Z_{p-1} with flag component mod 4200    def dmul(a, b):201        return ((a[0] + b[0]) % P, (a[1] + b[1]) % (P - 1), (a[2] + b[2]) % 4)202203    def dinv(a):204        return ((-a[0]) % P, (-a[1]) % (P - 1), (-a[2]) % 4)205206    ONE = (0, 0, 0)207    L = (1, 0, 0)208    T = (0, 1, 0)209    FLAG = (0, 0, 1)                 # the unit flag Iq210211    chk("group identity", dmul(ONE, L) == L)212    chk("inverses", dmul(L, dinv(L)) == ONE and dmul(FLAG, dinv(FLAG)) == ONE)213    chk("flag order four", dmul(dmul(FLAG, FLAG), dmul(FLAG, FLAG)) == ONE)214    # 10:D2 (p10018)215    # fork B: the flag is internal, Iq = [T]^kappa; realized label of (r,s;j) is216    # (r mod p, (s + j*kappa) mod (p-1)) with sector j mod 4217    def realize(a):218        return (a[0] % P, (a[1] + a[2] * KAPPA) % (P - 1))219    chk("realized flag label = (0, kappa)", realize(FLAG) == (0, KAPPA))220    o4 = [(r, s) for r in range(P) for s in range(P - 1)221          if (4 * r) % P == 0 and (4 * s) % (P - 1) == 0222          and not ((2 * r) % P == 0 and (2 * s) % (P - 1) == 0)]223    # 10:X3 (p10050)224    chk("unique order-four subgroup: exactly two generators", sorted(o4) == [(0, KAPPA), (0, 3 * KAPPA)])225    chk("no flag of space: all order-four elements have r = 0", all(r == 0 for r, _ in o4))226    chk("flag horizon-inaccessible on window H<kappa",227          all((0, KAPPA) != (r % P, s % (P - 1))228              for r in range(-1, 2) for s in range(-1, 2)))229    EPSILONS = [e for e in range(1, P - 1) if __import__("math").gcd(e, P - 1) == 1]230    chk("flag covariance: eps*kappa in {kappa, 3kappa} for all units eps",231          all((e * KAPPA) % (P - 1) in (KAPPA, 3 * KAPPA) for e in EPSILONS))232    chk("realization is a homomorphism",233          all(realize(dmul(a, b)) == ((realize(a)[0] + realize(b)[0]) % P,234                                      (realize(a)[1] + realize(b)[1]) % (P - 1))235              for a in [L, T, FLAG, (3, 5, 2)] for b in [L, T, FLAG, (7, 2, 3)]))236237    # 10:F2 (p10034)238    # derived domains239    def dpow(a, k):240        out = ONE241        step = a if k >= 0 else dinv(a)242        for _ in range(abs(k)):243            out = dmul(out, step)244        return out245246    # 10:D6 (p10022)247    E_dom = dmul(FLAG, dinv(T))                       # [E] = Iq T^-1248    p_dom = dmul(FLAG, dinv(L))                       # [p] = Iq L^-1249    v_dom = dmul(L, dinv(T))                          # [v] = L T^-1250    m_dom = dmul(E_dom, dinv(dpow(v_dom, 2)))         # [m] = [E][v]^-2251    chk("[m] = Iq L^-2 T", m_dom == ((-2) % P, 1, 1))252    F_dom = dmul(m_dom, dmul(L, dpow(dinv(T), 2)))    # [F] = [m][a]253    chk("[F] = Iq L^-1 T^-1", F_dom == ((-1) % P, (-1) % (P - 1), 1))254    S_dom = dmul(E_dom, T)255    chk("[S] = Iq (action carries the flag)", S_dom == FLAG)256    chk("phase count neutral: [E][T][hbar]^-1 = 1", dmul(S_dom, dinv(FLAG)) == ONE)257    G_dom = dmul(F_dom, dmul(dpow(L, 2), dinv(dpow(m_dom, 2))))258    chk("[G] = Iq^-1 L^5 T^-3", G_dom == (5, (-3) % (P - 1), 3))259    chk("Planck area flag-free: [G][hbar][c]^-3",260          dmul(G_dom, dmul(FLAG, dpow(dinv(v_dom), 3)))[2] == 0)261    chk("[G hbar c^-3] = L^2",262          dmul(G_dom, dmul(FLAG, dpow(dinv(v_dom), 3))) == (2, 0, 0))263    chk("[Gm/c^2] = L",264          dmul(G_dom, dmul(m_dom, dpow(dinv(v_dom), 2))) == (1, 0, 0))265    # 10:F4 (p10036)266    chk("[Gm/r^3] = T^-2 flag-free",267          dmul(G_dom, dmul(m_dom, dpow(dinv(L), 3))) == (0, (-2) % (P - 1), 0))268    chk("Compton flag-free: [m][c][hbar]^-1 = L^-1",269          dmul(m_dom, dmul(v_dom, dinv(FLAG))) == ((-1) % P, 0, 0))270271    # fibrewise addition / neutral criterion / local recovery272    # 10:C3 (p10013)273    chk("squaring leaves fibre: dom(Q) != dom(Q^2) for [L]", L != dpow(L, 2))274    H = 5275    # 10:G1 (p10037), 10:G3 (p10039)276    chk("local recovery bound: p-1 > 2H", P - 1 > 2 * H)277    pairs = [(r, s) for r in range(-H, H + 1) for s in range(-H, H + 1)]278    images = {(r % P, s % (P - 1)) for (r, s) in pairs}279    chk("local recovery: all |r|,|s| <= 5 distinguished", len(images) == len(pairs))280    # the energy--momentum relation E^2 = p^2 c^2 + m^2 c^4: its three terms in one fibre, at crossing degree two (the281    # half-period sector) -- Example ex:dispersion, predicate 10:G3282    E2 = dpow(E_dom, 2); pc2 = dpow(dmul(p_dom, v_dom), 2); mc4 = dpow(dmul(m_dom, dpow(v_dom, 2)), 2)283    chk("dispersion: [E]^2 = [pc]^2 = [mc^2]^2, one fibre at sector 2", E2 == pc2 == mc4 and E2[2] == 2)284285    # B. the quartet at the unit face (exact rationals over free scales)286    family('dom', 'B')287    # Represent horizons as exponent vectors over (l, t, p, E) and verify the288    # relation lattice; then instantiate with exact rationals satisfying the289    # one identity l*p = t*E and confirm every claimed equality numerically.290    import itertools291292    # exponent vectors: c = l - t (= E - p), hbar = l + p (= t + E), mix = p + t293    c_vec    = (1, -1, 0, 0)294    c_vec2   = (0, 0, -1, 1)295    hbar_vec = (1, 0, 1, 0)296    hbar_vec2= (0, 1, 0, 1)297    mix_vec  = (0, 1, 1, 0)298    lE_vec   = (1, 0, 0, 1)299    rel      = (1, -1, 1, -1)        # l - t + p - E = 0 <=> l*p = t*E300301    def add(u, v): return tuple(a + b for a, b in zip(u, v))302    def sub(u, v): return tuple(a - b for a, b in zip(u, v))303304    chk("c faces differ by the relation", sub(c_vec, c_vec2) == rel)305    chk("hbar faces differ by the relation", sub(hbar_vec, hbar_vec2) == rel)306    chk("l*E = hbar*c (exponent identity)", lE_vec == add(hbar_vec2, c_vec))307    chk("mix = hbar/c (exponent identity)", mix_vec == sub(hbar_vec2, c_vec2))308309    # rank of {c, hbar, mix} modulo the relation is 3 (full)310    def rank_int(rows):311        m = [list(map(Fr, r)) for r in rows]312        rank, ncols = 0, len(m[0])313        for col in range(ncols):314            piv = next((i for i in range(rank, len(m)) if m[i][col] != 0), None)315            if piv is None:316                continue317            m[rank], m[piv] = m[piv], m[rank]318            m[rank] = [x / m[rank][col] for x in m[rank]]319            for i in range(len(m)):320                if i != rank and m[i][col] != 0:321                    m[i] = [a - m[i][col] * b for a, b in zip(m[i], m[rank])]322            rank += 1323        return rank324325    # 10:E2 (p10025)326    # pairing lattice mod the relation has rank TWO: mix = hbar - c, lE = hbar + c327    chk("mix = hbar' - c' (exponent identity: k_B derived)",328          mix_vec == sub(hbar_vec2, c_vec2))329    chk("pairing rank 2 mod relation: rank{c,hbar,rel} = 3",330          rank_int([c_vec, hbar_vec, rel]) == 3)331    chk("mix adds nothing: rank{c,hbar,mix,rel} = 3",332          rank_int([c_vec, hbar_vec, mix_vec, rel]) == 3)333    chk("lE adds nothing: rank{c,hbar,mix,lE,rel} = 3",334          rank_int([c_vec, hbar_vec, mix_vec, lE_vec, rel]) == 3)335336    # 10:E3 (p10026)337    # numeric instantiation with the identity enforced: choose l,t,p free, E = l*p/t338    l, t, p = Fr(3, 7), Fr(2, 5), Fr(11, 4)339    E = l * p / t340    c_u, hbar_u = l / t, l * p341    chk("unit face: c = l/t = E/p", c_u == E / p)342    chk("unit face: hbar = l p = t E", hbar_u == t * E)343    chk("cancellation: (p t)(l/t) = l p  [k_B c = -hbar]", (p * t) * (l / t) == hbar_u)344    chk("mixed partner: l E = hbar c", l * E == hbar_u * c_u)345    m_P = p / c_u346    chk("m_P = p/c = E/c^2", m_P == E / c_u ** 2)347    G_num = hbar_u * c_u / m_P ** 2348    chk("G = hbar c / m_P^2 = l^2 c^3 / hbar", G_num == l ** 2 * c_u ** 3 / hbar_u)349    # bijection {c, hbar, G} <-> quartet: recover the free scale from G350    chk("bijection: l^2 = G hbar / c^3", l ** 2 == G_num * hbar_u / c_u ** 3)351    chk("recovered quartet: t=l/c, p=hbar/l, E=hbar c/l",352          t == l / c_u and p == hbar_u / l and E == hbar_u * c_u / l)353    Theta = E / (hbar_u / c_u)      # E_P / |k_B|354    chk("Theta_P = E_P/|k_B| = c^2/1 * ... consistent", Theta == E * c_u / hbar_u)355356    # DOF: quartet has 4 generators, 1 relation -> 3 free scales; +G -> 3+1357    # 10:X1 (p10048)358    chk("DOF: 4 - 1 = 3 free scales", 4 - rank_int([rel]) == 3)359360    # ------------------------------------------------------------------361    # flag positions of the quartet: (l, t, p, E) at (0, 0, 1, 1) mod 4;362    # every quartet relation must close on the flag component363    # ------------------------------------------------------------------364    FL = {"l": 0, "t": 0, "p": 1, "E": 1}365    def flag_of(expr):366        # expr: dict of generator -> exponent367        return sum(FL[g] * e for g, e in expr.items()) % 4368    chk("flag[hbar = l p] = 1", flag_of({"l": 1, "p": 1}) == 1)369    chk("flag[hbar = t E] = 1", flag_of({"t": 1, "E": 1}) == 1)370    chk("flag[c = l/t] = 0", flag_of({"l": 1, "t": -1}) == 0)371    chk("flag[c = E/p] = 0", flag_of({"E": 1, "p": -1}) == 0)372    chk("flag[k_B ~ p t] = 1", flag_of({"p": 1, "t": 1}) == 1)373    chk("flag[hbar c ~ l E] = 1", flag_of({"l": 1, "E": 1}) == 1)374    # G = l^2 c^3 / hbar: flags 2*0 + 3*0 - 1 = -1 = 3 mod 4 (inverse flag)375    chk("flag[G] = -1", (2 * FL["l"] + 3 * 0 - flag_of({"l": 1, "p": 1})) % 4 == 3)376    # Planck area G hbar / c^3 flag-free; Gm/c^2 flag-free (m at flag 1)377    chk("flag[G hbar/c^3] = 0", (3 + 1 + 0) % 4 == 0)378    chk("flag[G m/c^2] = 0 (m flag 1)", (3 + 1 + 0) % 4 == 0)379    # dual horizons are flag-crossed images: p = hbar/l, E = hbar/t380    chk("p = hbar/l (unit face)", p == hbar_u / l)381    chk("E = hbar/t (unit face)", E == hbar_u / t)382    # equivalent generating data {l, t, hbar} <-> {c, hbar, G}383    chk("{l,t,hbar} determine c, G", c_u == l / t and G_num == l ** 2 * (l / t) ** 3 / hbar_u)384385    # C. the defining congruences on the lab Carrier386    family('dom', 'C')387    S = 602_140388    Om = 4 * S + 1389    chk("Om = 2,408,561", Om == 2_408_561)390391    def is_prime(n):392        if n < 2: return False393        if n % 2 == 0: return n == 2394        d = 3395        while d * d <= n:396            if n % d == 0: return False397            d += 2398        return True399400    chk("admissibility: S even, S=1 mod 3, Om prime",401          S % 2 == 0 and S % 3 == 1 and is_prime(Om))402403    # 10:E4 (p10027)404    # congruence 1: 2G + 1 = 0 -- linear, unique405    G_pin = [x for x in (pow(2, -1, Om) * (Om - 1) % Om,) ]406    G_val = (Om - 1) // 2407    chk("congruence 2G+1=0 unique: G = 2S = 1,204,280", (2 * G_val + 1) % Om == 0 and G_val == 2 * S == 1_204_280)408409    # quadratic defining congruences: exhaustive-root verification via the known values410    hbar_val = 18_688411    kB_val = 1_880_160412    chk("congruence hbar^2 = -1", (hbar_val * hbar_val) % Om == Om - 1)413    chk("congruence k_B^2 = -2", (kB_val * kB_val) % Om == Om - 2)414    c2 = (2 * S + 1) % Om415    chk("congruence 2c^2 = 1: c^2 = 2S+1", (2 * c2) % Om == 1)416    # each quadratic congruence has exactly two roots: x and Om - x417    for name, val, target in (("hbar", hbar_val, Om - 1), ("k_B", kB_val, Om - 2)):418        other = Om - val419        chk(f"{name}: two roots {{x, -x}}", (other * other) % Om == target and other != val)420    # linkage consistency: the stated representatives satisfy k_B c = -hbar421    c_val = (-hbar_val * pow(kB_val, -1, Om)) % Om422    chk("c from k_B c = -hbar", (kB_val * c_val) % Om == (Om - hbar_val) % Om)423    chk("c^2 lands on the congruence", (c_val * c_val) % Om == c2)424    chk("register identities: G = -c^2, G^2 = 4^-1",425          (G_val + c2) % Om == 0 and (4 * G_val * G_val) % Om == 1)426    chk("h = 2 pi hbar = -hbar = k_B c", (Om - hbar_val) % Om == (kB_val * c_val) % Om)427    chk("m_P^2 = Om = 0 (scale face: the totality)", (Om) % Om == 0)428429430    # D. revision layer: both Carriers, face closure, minimality, temperature431    family('dom', 'D')432433    def sqrt_roots(a, Om):434        return sorted(x for x in range(Om) if (x * x) % Om == a % Om)435436    CARRIERS = {437        233: dict(S=58, hbar=89, kB=124, c=159, G=116, h=144),438        2_408_561: dict(S=602_140, hbar=18_688, kB=1_880_160, c=171_106, G=1_204_280, h=2_389_873),439    }440    # fill lab h and c consistently441    lab = CARRIERS[2_408_561]442    lab["c"] = (-lab["hbar"] * pow(lab["kB"], -1, 2_408_561)) % 2_408_561443    lab["h"] = (2_408_561 - lab["hbar"]) % 2_408_561444445    for Om_, R in CARRIERS.items():446        S_, hb, kB, c_, G_, h_ = R["S"], R["hbar"], R["kB"], R["c"], R["G"], R["h"]447        chk(f"[{Om_}] admissibility triple: S even, S=1 mod 3, Om prime",448              S_ % 2 == 0 and S_ % 3 == 1 and is_prime(Om_))449        chk(f"[{Om_}] two-way class: S even <=> Om = 1 mod 8", Om_ % 8 == 1)450        # congruence equations of the residue reading451        chk(f"[{Om_}] B: 2G = -1", (2 * G_ + 1) % Om_ == 0)452        chk(f"[{Om_}] B: c^2 = 2^-1", (2 * c_ * c_) % Om_ == 1)453        chk(f"[{Om_}] B: hbar^2 = -1", (hb * hb) % Om_ == Om_ - 1)454        chk(f"[{Om_}] B: k_B^2 = -2", (kB * kB) % Om_ == Om_ - 2)455        chk(f"[{Om_}] B: k_B c = -hbar", (kB * c_) % Om_ == (Om_ - hb) % Om_)456        chk(f"[{Om_}] B: h = -hbar", h_ == (Om_ - hb) % Om_)457        # closure consequences (Prop faces-closure)458        chk(f"[{Om_}] closure: G = -c^2", (G_ + c_ * c_) % Om_ == 0)459        chk(f"[{Om_}] closure: G^2 = 4^-1", (4 * G_ * G_) % Om_ == 1)460        chk(f"[{Om_}] closure: hbar^4 = 1", pow(hb, 4, Om_) == 1)461        chk(f"[{Om_}] closure: (k_B c)^2 = -1", pow(kB * c_, 2, Om_) == Om_ - 1)462        chk(f"[{Om_}] closure: hbar c G^-1 = k_B (m_P^2 monomial face on the k_B residue)",463              (hb * c_ * pow(G_, -1, Om_)) % Om_ == kB)464        chk(f"[{Om_}] monomial face nonzero: horizon declaration is not a congruence",465              (hb * c_ * pow(G_, -1, Om_)) % Om_ != 0)466        # defining congruences have exactly two roots each467        for name, val, tgt in (("hbar", hb, Om_ - 1), ("kB", kB, Om_ - 2)):468            roots = sorted(((val) % Om_, (Om_ - val) % Om_))469            chk(f"[{Om_}] {name}: root pair valid", all((x * x) % Om_ == tgt for x in roots))470471    # representative half-planes are chart data (suite annex): band predicates472    # carry no invariant content, as the pair form requires473    r233 = sqrt_roots(58, 233)474    chk("233: sqrt(S) roots {72,161}", r233 == [72, 161])475    chk("233: hbar-representative from the upper-half root of S (161 -> 89): chart datum",476          (2 * 161) % 233 == 89 and 161 > 233 // 2)477    chk("233: the other root gives the pair partner h (72 -> 144)", (2 * 72) % 233 == 144)478    chk("lab: hbar-representative from the lower-half root of S (9344): chart datum",479          (2 * 9344) % 2_408_561 == 18_688 and 9344 < 2_408_561 // 2)480    chk("half-plane of the hbar-representative differs across Carriers: band = chart data",481          (161 > 233 // 2) and (9344 < 2_408_561 // 2))482483    # -1 is QR unconditionally (Om = 4S+1 = 1 mod 4), S even needed only for 2484    chk("-1 QR even for odd S: Om=13 (S=3), 5^2 = -1", (5 * 5) % 13 == 12)485    chk("Om = 1 mod 4 for every S", all((4 * S0 + 1) % 4 == 1 for S0 in range(1, 50)))486487    # 10:E9 (p10032)488    # minimality scan under the complete predicate (the paper's Definitions 1 and 2, Remark 1)489    def admissible(p_, Om__):490        kap_ = (p_ - 1) // 4491        S__ = (Om__ - 1) // 4492        return (kap_ > 1 and is_prime(p_) and p_ % 4 == 1493                and Om__ % 4 == 1 and is_prime(Om__)494                and S__ % 2 == 0 and S__ % 3 == 1495                and p_ * p_ < Om__)496    adm = [(p_, Om__) for p_ in range(5, 40, 4) for Om__ in range(p_ * p_ + 1, 234)497           if admissible(p_, Om__)]498    chk("minimality: (13,233) admissible", (13, 233) in adm)499    chk("minimality: no admissible pair below 233", min(o for _, o in adm) == 233)500    chk("counterfactual: dropping mod-3 admits (13,193)",501          is_prime(193) and 48 % 2 == 0 and 48 % 3 == 0 and 13 * 13 < 193)502    chk("counterfactual: dropping kappa>1 admits (5,41)",503          is_prime(5) and is_prime(41) and 10 % 2 == 0 and 10 % 3 == 1 and 25 < 41)504    chk("F5 is its own quarter-turn core: 4*kappa = 4 = p-1 with kappa=1", 4 * 1 == 5 - 1)505    chk("kappa=2 not viable: 9 composite", not is_prime(9))506507    # 10:P2 (p10054)508    # constancy (the prediction P2): the dimensionless ratios of the constants are fixed, zero drift; the present bound on the509    # fine-structure constant, (1/alpha) dalpha/dt = 1.8(2.5)e-19 /yr (Filzinger et al. 2023, imported), brackets the predicted 0:510    # 18 - 25 <= 0 <= 18 + 25 in units of 1e-20 /yr.511    chk("P2: the predicted drift 0 lies within the imported bound 1.8(2.5)e-19 /yr", 18 - 25 <= 0 <= 18 + 25)512513    # 10:F3 (p10035), 10:X2 (p10049)514    # temperature and Unruh closures in (r, s, j) bookkeeping515    kB_dom = (-1, 1, 1)                    # Iq L^-1 T516    E_dom3 = (0, -1, 1)                    # Iq T^-1517    acc = (1, -2, 0)518    Theta = tuple(a - b for a, b in zip(E_dom3, kB_dom))519    chk("[Theta] = [E][k_B]^-1 = L T^-2, flag-free", Theta == acc)520    c_dom3 = (1, -1, 0)521    hb_dom3 = (0, 0, 1)522    unruh = tuple(h + a - c - k for h, a, c, k in zip(hb_dom3, acc, c_dom3, kB_dom))523    chk("Unruh closure: [hbar a / (c k_B)] = [Theta]", unruh == acc)524525    # crossing-degree recovery (Cor recovery-crossings)526    def embed(u, a, b):527        return (a - 2 * u, b + u, u)528    trip = [(u, a, b) for u in range(-2, 3) for a in range(-3, 4) for b in range(-3, 4)]529    chk("classical embedding injective on Z^3",530          len({embed(u, a, b) for u, a, b in trip}) == len(trip))531    P2, K2 = 229, 57532    def real2(r, s, j):533        return (r % P2, (s + j * K2) % (P2 - 1))534    win = [(r, s, j) for r in range(-5, 6) for s in range(-5, 6) for j in (-1, 0, 1)]535    chk("faithful realization on window (p=229, H=5, |j|<=1)",536          len({(real2(*w), w[2] % 4) for w in win}) == len(win))537    chk("sector saturates mod 4: hbar^4 realizes at sector zero",538          (4 * K2) % (P2 - 1) == 0)539540541    # E. round-02 layer: covariance counterexamples, window covariance,542    family('dom', 'E')543544    # (a) regression: the naive character on Z_p-reduced labels is ill-defined545    inv2 = pow(2, -1, 13)546    chk("r02: character ill-defined on the modular projection (r=3 vs r=16 differ)",547          pow(inv2, 3, 13) != pow(inv2, 16, 13))548    # (b) regression: (p-1, 0) has trivial character yet is non-neutral549    chk("r02: (p-1,0) trivial character for all m",550          all(pow(m, -(13 - 1), 13) == 1 for m in range(1, 13)))551    chk("r02: (p-1,0) is non-neutral in D_p", (13 - 1) % 13 != 0)552    # (c) regression: eps as field character fails composition (5^2=1 in Z_12^x)553    chk("r02: eps field-character composition fails",554          (5 * 5) % 12 == 1 and pow(pow(5, -1, 13), 2, 13) != 1)555556    # 10:C5 (p10015)557    # window covariance (Theorem 5, repaired form)558    H = 5559    chk("r02: window dilation: trivial character forces r=0 in window",560          all(not all(pow(m, -r, 13) == 1 for m in range(2, 13))561              for r in range(-H, H + 1) if r != 0))562    # pushforward invariant sublattice on the realized lattice is {0, pi}563    units12 = [e for e in range(1, 12) if __import__("math").gcd(e, 12) == 1]564    inv_labels = [s_ for s_ in range(12) if all((e * s_) % 12 == s_ for e in units12)]565    chk("r02: pushforward-invariant labels are exactly {0, pi}", inv_labels == [0, 6])566    chk("r02: eps=-1 admissible always", __import__("math").gcd(11, 12) == 1)567    # flag pair behaviour under pushforward: eps mod 4 in {1,3} decides fix/swap568    chk("r02: quarter-turn labels fixed iff eps=1 mod 4",569          all(((e * 3) % 12 == 3) == (e % 4 == 1) for e in units12))570571    # representative-convention data (chart-side record; no invariant content)572    chk("r02: hbar representative lower-half on 233 (chart datum)", 89 < 233 // 2 and (89 * 89) % 233 == 232)573    chk("r02: hbar representative lower-half on lab (chart datum)",574          18_688 < 2_408_561 // 2 and (18_688 ** 2) % 2_408_561 == 2_408_560)575    chk("r02: c representative halves differ across Carriers (chart data)",576          (159 > 233 // 2) and (171_106 < 2_408_561 // 2))577    chk("r02: +-c one residue class (-1 is QR)", pow(89, 2, 233) == 233 - 1)578579    # index-two sublattice <c, hbar, G> in Z^3 on (l, t, hbar)580    M = [[1, -1, 0], [0, 0, 1], [5, -3, -1]]581    det = (M[0][0] * (M[1][1] * M[2][2] - M[1][2] * M[2][1])582           - M[0][1] * (M[1][0] * M[2][2] - M[1][2] * M[2][0])583           + M[0][2] * (M[1][0] * M[2][1] - M[1][1] * M[2][0]))584    chk("r02: <c,hbar,G> has index two (det = -2)", det == -2)585    chk("r02: l^2 = G hbar / c^3 recovers the scale by positive root",586          l ** 2 == G_num * hbar_u / c_u ** 3 and l > 0)587588    # residue reading rho: multiplicative on constant monomials (both Carriers)589    for Om_, R in CARRIERS.items():590        hb, kB, c_, G_ = R["hbar"], R["kB"], R["c"], R["G"]591        lhs = (hb * c_ * pow(G_, -1, Om_)) % Om_592        chk(f"r02 [{Om_}]: rho multiplicative on hbar*c/G", lhs == kB)593        chk(f"r02 [{Om_}]: rho(h) = -rho(hbar)", R["h"] == (Om_ - hb) % Om_)594595596    # F. round-03 layer: window bound, sigma-twisted action, delta_C597    family('dom', 'F')598    import math as _m599    units12 = [e for e in range(1, 12) if _m.gcd(e, 12) == 1]600601    # window counterexample (regression): at H >= 2kap, (0, pi) is invariant and non-neutral602    chk("r03: pi invariant under every pushforward", all((e * 6) % 12 == 6 for e in units12))603    chk("r03: (0,pi) non-neutral", 6 % 12 != 0)604    # corrected window H < 2kap: only neutral label invariant605    Hc = 2 * KAPPA - 1606    inv_win = [s_ for s_ in range(-Hc, Hc + 1) if all((e * (s_ % 12)) % 12 == s_ % 12 for e in units12)]607    chk("r03: window H<2kap invariants = {0}", inv_win == [0])608    chk("r03: window bound equals local-recovery bound", (4 * KAPPA > 2 * Hc) and (Hc < 2 * KAPPA))609610    # sigma-twisted active action: full equivariance sweep on p=13 and p=229611    def sigma(e):612        return 1 if e % 4 == 1 else -1613    for P_, K_ in ((13, 3), (229, 57)):614        U_ = [e for e in range(1, P_ - 1) if _m.gcd(e, P_ - 1) == 1]615        ok = all(((e * s_) % (P_ - 1) + sigma(e) * j * K_) % (P_ - 1)616                 == (e * (s_ + j * K_)) % (P_ - 1)617                 for e in U_ for s_ in range(0, P_ - 1, max(1, (P_ - 1) // 12)) for j in (-2, -1, 0, 1, 2))618        chk(f"r03: sigma-twist equivariant on p={P_}", ok)619    chk("r03: witness e=7,(2;1) matches realized action", ((7 * 2) % 12 + sigma(7) * 3) % 12 == (7 * 5) % 12)620    chk("r03: witness e=-1,(0;1) matches realized action", ((11 * 0) % 12 + sigma(11) * 3) % 12 == (11 * 3) % 12)621    chk("r03: plain lift fails for e=7,(2;1) (regression)", ((7 * 2) % 12 + 3) % 12 != (7 * 5) % 12)622    chk("r03: sigma multiplicative mod 4",623          all(sigma(a * b) == sigma(a) * sigma(b) for a in units12 for b in units12))624625    # 10:D1 (p10017)626    # delta_S / delta_C: involutions; delta_C carries primal domains to dual horizon domains627    def dS_(a):628        return dinv(a)629    def dC_(a):630        return dmul(FLAG, dinv(a))631    chk("r03: delta_S involution", all(dS_(dS_(a)) == a for a in [L, T, FLAG, (3, 5, 2)]))632    chk("r03: delta_C involution", all(dC_(dC_(a)) == a for a in [L, T, FLAG, (3, 5, 2)]))633    chk("r03: delta_C[L] = [p] domain", dC_(L) == p_dom)634    chk("r03: delta_C[T] = [E] domain", dC_(T) == E_dom)635    chk("r03: delta_S flag-free", dS_(L)[2] == 0 and dS_(T)[2] == 0)636637638    # G. round-04 layer: realized action, j-restriction, ladder, k_B linkage typing639    family('dom', 'G')640    import math as _mm641642    # realized action composes with residue classes; Z^3 representatives do not643    u0 = 5644    chk("r04: realized action composes (5*5=1 in Z_12^x)", ((5 * (5 * u0)) % 12) == ((25 % 12) * u0) % 12 == u0 % 12)645    chk("r04: integer representatives do not compose on Z (25s != s)", 25 * 2 != 2)646647    # j-suppression witness: (0,0;1) moves under eps=-1 (flag-free restriction needed)648    chk("r04: (0,0;1) sector moves under eps=-1", ((-1) * (0 + 3)) % 12 == 9 != 3)649650    # 10:G2 (p10038)651    # window ladder: nested for kappa >= 17; toy fails.  All orderings exact:652    # 2 sqrt(k) < k/2  <=>  (4 sqrt(k))^2 < k^2  <=>  16 k < k^2  <=>  k > 16.653    def ladder(k):654        return 16 * k < k * k and 0 < k655    chk("r04: ladder nested for kappa=17,387,602140 (integer-square ordering)",656          all(ladder(k) for k in (17, 387, 602140)))657    chk("r04: toy kappa=3 below nesting threshold", not ladder(3))658    chk("r04: coherence window identity (2 sqrt kappa)^2 = 4 kappa = p-1 exactly",659          all((2 * 2 * k == 4 * k) and (4 * k == (4 * k + 1) - 1) for k in (3, 387, 602140)))660    chk("r04: totality closure exact: (2 sqrt S)^2 = Om - 1",661          4 * 602140 == 2408561 - 1)662663    # 10:G5 (p10052), 10:P1 (p10053)664    # the resolution floor (Remark rem:measured; the prediction P1): a single coherent registration on a shell of cardinality p resolves no finer665    # than p^(-1/2) (coherent counts bounded at sqrt p, the import A5); under p^2 < Om the floor is at least Om^(-1/4) on every666    # admissible shell. On the chart value S = 2.6e122 (A2), Om = 4S+1: Om^(-1/4) is of the order of 1e-31667    # (1e-31 <= Om^(-1/4) < 1e-30  <=>  1e120 < Om <= 1e124); the ratio 1e-18 / Om^(-1/4) rounds to thirteen orders668    # (1e12.5 <= Om^(1/4) 1e-18 < 1e13.5  <=>  1e122 <= Om < 1e126); the ratio 2.2e-5 / Om^(-1/4) rounds to twenty-six669    # (1e25.5 <= 2.2e-5 Om^(1/4) < 1e26.5  <=>  1e126 <= 22^4 Om < 1e130). Every comparison exact in integers.670    S_chart = 26 * 10**121; Om_chart = 4 * S_chart + 1671    chk("r04: floor Om^(-1/4) of order 1e-31 on the chart value S = 2.6e122", 10**120 < Om_chart <= 10**124)672    chk("r04: the floor thirteen orders below the 1e-18 frequency comparisons", 10**122 <= Om_chart < 10**126)673    chk("r04: the floor twenty-six orders below 2.2e-5, the relative uncertainty of G", 10**126 <= 22**4 * Om_chart < 10**130)674    # P1: the floor in bits, to the nearest integer (101.5 <= log2 Om^(1/4) < 102.5  <=>  2^406 <= Om < 2^410); the finest interspecies675    # frequency ratio 3.2e-18 is 58 bits (57.5 <= log2(1/3.2e-18) < 58.5  <=>  2^125 <= 1e38 < 2^127) and the finest differential676    # comparison 7.6e-21 is 67 bits (66.5 <= log2(1/7.6e-21) < 67.5  <=>  76^2 2^133 <= 1e44 < 76^2 2^135); the maximal coherent count Om^(1/4) between 5e30 and 6e30; the duration677    # beyond which the mass-independent clock bound (t_P^2 t)^(1/3) permits finer than the floor, t* = t_P Om^(3/8), between 600 s678    # and 900 s with t_P = 5.391247e-44 s (CODATA 2022): t*^8 = t_P^8 Om^3.679    chk("P1: the floor is 102 bits to the nearest integer (2^406 <= Om < 2^410)", 2**406 <= Om_chart < 2**410)680    chk("P1: the finest interspecies frequency ratio 3.2e-18 is 58 bits to the nearest integer (2^125 <= 1e38 < 2^127)", 2**125 <= 10**38 < 2**127)681    chk("P1: the finest differential frequency comparison 7.6e-21 is 67 bits to the nearest integer (76^2 2^133 <= 1e44 < 76^2 2^135)", 76**2 * 2**133 <= 10**44 < 76**2 * 2**135)682    chk("P1: the maximal coherent count Om^(1/4) lies between 5e30 and 6e30", 5**4 * 10**120 < Om_chart < 6**4 * 10**120)683    chk("P1: the clock-bound crossover t* = t_P Om^(3/8) lies between 600 s and 900 s", 600**8 * 10**400 < 5391247**8 * Om_chart**3 < 900**8 * 10**400)684685    # F/a is flagged (equal-crossing-degree correction): [F]=(-1,-1;1), [a]=(1,-2;0)686    F3 = (-1, -1, 1); A3 = (1, -2, 0)687    ratio = tuple(f - a for f, a in zip(F3, A3))688    chk("r04: F/a crossing degree 1 (flagged, = [m])", ratio == (-2, 1, 1))689690    # meridian transport onto the flag: (L T^kappa)^p = Iq on several shells691    for P_, K_ in ((13, 3), (29, 7), (229, 57)):692        chk(f"r04: meridian transport p={P_}", (P_ % P_, (P_ * K_) % (P_ - 1)) == (0, K_))693694    # Buckingham's count on the integer lift (Corollary cor:pi-theorem): the pendulum (T, l, g, m) with lifted labels695    # (0,1;0), (1,0;0), (1,-2;0), (-2,1;1) has rank 3, hence N - rank = 1 dimensionless product, T^2 g / l, whose696    # lifted label vanishes; the mass, the only quantity with a crossing degree, cannot enter it697    pend = [(0, 1, 0), (1, 0, 0), (1, -2, 0), (-2, 1, 1)]698    kvec = (2, -1, 1, 0)699    lab_ = tuple(sum(k * q[i] for k, q in zip(kvec, pend)) for i in range(3))700    # 10:G4 (p10046)701    chk("Buckingham: pendulum (T, l, g, m) rank 3, one product T^2 g/l with label (0,0;0)", rank_int(pend) == 3 and lab_ == (0, 0, 0))702    # The electromagnetic domain (Remark rem:electromagnetic, predicate 10:F5): with the Coulomb constant neutral, [q]^2 = [E][L] =703    # I_q [L][T]^-1, on the shell (1, kappa-1), on the lift (1,-1;1). Its square roots in D_p = Z_p x Z_{4 kappa}: the space half704    # 2^-1 = 2 kappa + 1 = -2 kappa (the meridian half-turn); the phase equation 2s = kappa-1 (mod 4 kappa) is solvable iff kappa705    # is odd, then two roots differing by the half-period (0, 2 kappa) = I_q^2; on the lift no root at all (odd coordinates).706    def charge_roots(k):707        p_, n_ = 4 * k + 1, 4 * k708        return sorted((r, s) for r in range(p_) for s in range(n_) if ((2 * r) % p_, (2 * s) % n_) == (1, (k - 1) % n_))709    # 10:F5 (p10047), 10:X4 (p10051)710    chk("charge: [q]^2 = [E][L] = I_q [L][T]^-1 = (1, 2) on F_13, its roots exactly (7,1) and (7,7), differing by the half-period (0, 6)",711          ((0 + 1) % 13, (3 - 1 + 0) % 12) == (1, 2) and charge_roots(3) == [(7, 1), (7, 7)] and ((7 - 7) % 13, (7 - 1) % 12) == (0, 6))712    chk("charge: the roots exist iff kappa is odd, then exactly (2 kappa+1, (kappa-1)/2) and its half-period partner (every prime p = 4 kappa+1, kappa <= 30)",713          all((charge_roots(k) == sorted([(2 * k + 1, (k - 1) // 2), (2 * k + 1, (k - 1) // 2 + 2 * k)])) if k % 2 else charge_roots(k) == []714              for k in range(1, 31) if all((4 * k + 1) % d for d in range(2, 4 * k + 1))))715    chk("charge: the space exponent 2^-1 = 2 kappa+1 = -2 kappa is the meridian half-turn, |r| = 2 kappa, on p = 13, 29, 173, 229",716          all((2 * (2 * k + 1)) % (4 * k + 1) == 1 and (2 * k + 1) - (4 * k + 1) == -2 * k for k in (3, 7, 43, 57)))717    chk("charge: on the lift [q]^2 = (1,-1;1) has no half; [phi]^2 = [q]^2 [L]^-2 = [F], [E_field]^2 = [F]^2 [q]^-2 = the energy density, e^2/(hbar c) neutral",718          all(c % 2 for c in (1, -1, 1)) and (1 - 2, -1, 1) == (-1, -1, 1) and (2 * (-1) - 1, 2 * (-1) + 1, 2 - 1) == (0 - 3, -1, 1)719          and (0 + 1, 0 - 1, 1 + 0) == (1, -1, 1))720    chk("charge: the dilation character m^-r at r = 2 kappa+1 is m^-1 (m|p) (Euler); a non-square dilation flips the sign, never window-covariant (p = 13, 29)",721          all(pow(m, -(2 * k + 1), 4 * k + 1) == (pow(m, -1, 4 * k + 1) * pow(m, 2 * k, 4 * k + 1)) % (4 * k + 1)722              and pow(m, 2 * k, 4 * k + 1) == (1 if any((x * x) % (4 * k + 1) == m for x in range(1, 4 * k + 1)) else 4 * k)723              for k in (3, 7) for m in range(1, 4 * k + 1))724          and any(pow(m, 6, 13) == 12 for m in range(1, 13)))725726    # both roots of -2 satisfy the congruence individually (the pair is the canonical727    # object); the stated representative is the linkage-consistent one728    for Om_, R in CARRIERS.items():729        kB = R["kB"]; other = Om_ - kB730        chk(f"r04 [{Om_}]: both k_B roots satisfy the congruence", (other * other) % Om_ == Om_ - 2)731        chk(f"r04 [{Om_}]: stated representative is linkage-consistent, its partner is not",732              (kB * R["c"]) % Om_ == (Om_ - R["hbar"]) % Om_ and (other * R["c"]) % Om_ != (Om_ - R["hbar"]) % Om_)733734735    # H. round-05 pair layer: pair-well-definedness and representative inertness736    family('dom', 'H')737    # pair multiplication {±a}{±b} = {±ab} is well defined: the four member738    # products fall in one pair739    for Om_, R in CARRIERS.items():740        a_, b_ = R["kB"], R["c"]741        prods = {(sa * a_ * sb * b_) % Om_ for sa in (1, -1) for sb in (1, -1)}742        chk(f"H [{Om_}]: pair product well defined ({{±k_B}}{{±c}} is one pair)",743              prods == {(a_ * b_) % Om_, (-a_ * b_) % Om_})744        # linkage as a pair THEOREM: (k_B c)^2 = -1, so the product pair is the745        # root pair of -1, which is {±hbar}746        chk(f"H [{Om_}]: (k_B c)^2 = -1 (linkage derived at pair level)",747              pow(a_ * b_, 2, Om_) == Om_ - 1)748        chk(f"H [{Om_}]: product pair equals {{±hbar}}",749              prods == {R["hbar"] % Om_, (Om_ - R["hbar"]) % Om_})750        # (hbar c / G)^2 = -2: the monomial lands in the k_B pair751        mono = (R["hbar"] * R["c"] * pow(R["G"], -1, Om_)) % Om_752        chk(f"H [{Om_}]: (hbar c/G)^2 = -2, landing in the k_B pair",753              pow(mono, 2, Om_) == Om_ - 2 and mono in {R["kB"], Om_ - R["kB"]})754        # 10:E5 (p10028)755    # representative inertness: exactly the assignments with s_h = s_c*s_k are756        # admissible (a (Z/2)^2 group), and every checked identity holds on each757        admissible_count = 0758        for s_c in (1, -1):759            for s_h in (1, -1):760                for s_k in (1, -1):761                    hb2, c2_, kB2 = (s_h * R["hbar"]) % Om_, (s_c * R["c"]) % Om_, (s_k * R["kB"]) % Om_762                    quad = ((2 * c2_ * c2_) % Om_ == 1 and (hb2 * hb2) % Om_ == Om_ - 1763                            and (kB2 * kB2) % Om_ == Om_ - 2)764                    link = (kB2 * c2_) % Om_ == (Om_ - hb2) % Om_765                    if quad and link:766                        admissible_count += 1767                        h2 = (Om_ - hb2) % Om_768                        chk(f"H [{Om_}] ({s_c},{s_h},{s_k}): h-form holds", h2 == (-hb2) % Om_)769                        chk(f"H [{Om_}] ({s_c},{s_h},{s_k}): monomial lands on this assignment's k_B",770                              (hb2 * c2_ * pow(R["G"], -1, Om_)) % Om_ == kB2)771                    assert quad, "quadratic defining congruences are sign-blind"772        chk(f"H [{Om_}]: admissible assignments form (Z/2)^2 (exactly four)",773              admissible_count == 4)774    # hbar-flip relabels within the pair: {hbar, h} -> {h, hbar}775    chk("H: hbar-flip relabels the {hbar,h} pair (233: 89 <-> 144)",776          (233 - 89) % 233 == 144 and (233 - 144) % 233 == 89)777    flush('dom', order=list('ABCDEFGH'))778779# ------------------------------------------------------------------------------------------------------------780# block lift — check_lift: exact verification of Proposition [The lift] (prop:lift)781#782# The flag records the fractional-Fourier quarter that the chart duality forgets.783# All arithmetic is exact (Python integers, modular); no floats, no RNG.784#785# Checks, per shell (p, g) and per Carrier Om:786#   L1  operator four-cycle: F = i*W on F_p^{p-1}, F^2 = J (parity), F^4 = id,787#       F^2 != id  (order exactly four).788#   L2  chart shadow order two: F exchanges the two dual charts, J exchanges789#       none; the cardinal skeleton acts on charts as s mod 2.790#   L3  record map: s -> Iq^s is an isomorphism Z_4 -> flag subgroup791#       {0, k, 2k, 3k} of Z_{p-1}; quotient by {0, 2k} returns s mod 2792#       (the diagram commutes; kernel of the forgetting = {id, J}).793#   L4  Carrier face: hbar^2 = -1 (mod Om), hbar^4 = 1, hbar^2 != 1:794#       the crossing quantum has order four, never two.795#   L5  invariance classification on the realized lattice (Theorem 5 preamble):796#       {u in Z_{p-1} : eps*u = u for every admissible eps} = {0, 2k} exactly;797#       witnesses (s,j) = (k,1) -> u = 2k invariant, (-k,1) -> u = 0 invariant,798#       (0,1) -> u = k not invariant, (0,2) -> u = 2k invariant.799#800# Instances: shell (13, 2) with the laboratory-scale shell (173, 3) as the801# second witness; Carriers 233 and 2408561 (the laboratory Carrier).802def modmat_mul(A, B, p):803    n = len(A)804    return [[sum(A[i][t] * B[t][j] for t in range(n)) % p for j in range(n)]805            for i in range(n)]806807def check_shell(p, g):808    n = p - 1                       # meridian cycle order 4k809    k = n // 4                      # capacity810    i_res = (-pow(g, k, p)) % p     # oriented quarter-turn residue811    assert (i_res * i_res) % p == p - 1, "i^2 != -1"812813    # 10:D3 (p10019)814    # shell Fourier matrix W_{jk} = g^{jk} on F_p^{n}; F = i*W815    W = [[pow(g, (j * l) % n, p) for l in range(n)] for j in range(n)]816    F = [[(i_res * W[j][l]) % p for l in range(n)] for j in range(n)]817818    F2 = modmat_mul(F, F, p)819    F4 = modmat_mul(F2, F2, p)820    I = [[1 if a == b else 0 for b in range(n)] for a in range(n)]821    # parity J: index inversion j -> -j mod n822    J = [[1 if b == (-a) % n else 0 for b in range(n)] for a in range(n)]823824    l1 = (F2 == J) and (F4 == I) and (F2 != I)825826    # L2: chart shadow. Charts = the primal/dual pair; F steps the cardinal827    # skeleton s=0,k,2k,3k; chart action is s mod 2 (F exchanges, J fixes).828    skeleton = [0, 1, 2, 3]                      # multiples of k829    chart_action = [s % 2 for s in skeleton]     # id, swap, id, swap830    l2 = chart_action == [0, 1, 0, 1]831832    # L3: record map s -> s*k in Z_n; image = flag subgroup, order four;833    # quotient by {0, 2k} returns s mod 2.834    flag = [(s * k) % n for s in skeleton]835    order4 = len(set(flag)) == 4 and all((4 * f) % n == 0 or f % k == 0 for f in flag)836    subgroup = all(((flag[a] + flag[b]) % n) in flag for a in skeleton for b in skeleton)837    quotient = all((flag[s] % (2 * k) == 0) == (chart_action[s] == 0) for s in skeleton)838    l3 = order4 and subgroup and quotient839840    return l1, l2, l3841842def check_invariance(p):843    n = p - 1844    k = n // 4845    units = [e for e in range(1, n) if gcd(e, n) == 1]846    fixed = {u for u in range(n) if all((e * u) % n == u for e in units)}847    classified = fixed == {0, 2 * k}848    real = lambda s, j: (s + j * k) % n849    witnesses = (real(k, 1) in fixed and real(-k, 1) in fixed850                 and real(0, 1) not in fixed and real(0, 2) in fixed)851    return classified and witnesses852853def check_carrier(Om):854    # hbar = a square root of -1 mod Om (exists since Om = 1 mod 4)855    hbar = None856    for x in range(2, Om):857        if (x * x) % Om == Om - 1:858            hbar = x859            break860    assert hbar is not None861    l4 = (pow(hbar, 2, Om) == Om - 1) and (pow(hbar, 4, Om) == 1) \862         and (pow(hbar, 2, Om) != 1)863    return l4864865def block_lift():866    """Block lift — check_lift: Proposition `lift`, the five claims L1–L5 on two shells and two Carriers (lift.L1 … lift.L5)."""867    for (p, g) in [(13, 2), (173, 3)]:868        l1, l2, l3 = check_shell(p, g)869        chk("L1(p=%d)" % p, l1, "lift", "L1"); chk("L2(p=%d)" % p, l2, "lift", "L2")870        chk("L3(p=%d)" % p, l3, "lift", "L3"); chk("L5(p=%d)" % p, check_invariance(p), "lift", "L5")871    for Om in [233, 2408561]:872        chk("L4(Om=%d)" % Om, check_carrier(Om), "lift", "L4")873    flush("lift", order=["L1", "L2", "L3", "L4", "L5"])874875if __name__ == "__main__":876    import time877    want = [a.lower() for a in sys.argv[1:]] or sorted(BLOCK)878    bad = [b for b in want if b not in BLOCK]879    if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")880    t0 = time.time()881    for b in want:882        t = time.time(); print(f"— block {b}"); _run_block(b); print(f"    [block {b}: {time.time() - t:.1f} s]")883    ok = summary(write=(want == sorted(BLOCK)))884    print(f"{len(RESULTS)} family checks, {len(MICRO)} exact micro-checks, {time.time() - t0:.1f} s" + ("; results.json written" if want == sorted(BLOCK) else ""))885    sys.exit(0 if ok else 1)886