frame.py — frc/ledgers/master

1"""master/frame — a ledger file of the master's block C, the Subject: the rows the frame theme proves (the push on C12,28 October 2026).34Block C is bound by one file per theme whose key file proves its rows (subject.py, extension.py, fourier.py,5projective.py and this file). This file binds C12, temperature and the classical arity (10-dimensions F3): the table of6keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the Subjects,7and the checks, which call the frame theme's lattice (frc/shell.py: the unit-domain lattice, the torsion-free lift of8the modular domain group D_p = C_p × C_{p−1} on the frame's two charts). The Lean side is lean/FrcCore/Theme/Domain.lean,9the key file lean/FrcCore/Keys/Frame.lean and the certificate lean/FrcCore/Ledgers/Master/Frame.lean.1011    python3 -m frc.ledgers.master.frame        every block, the census; exit 1 if a check fails1213Blocks:  D  the unit-domain lattice: temperature is acceleration, the classical shadow    EXACT  (00:C12)1415The notebook frc/ledgers/master/frame.ipynb runs one row per cell, the cell's id its key (gate G13).16"""17import sys1819from frc.registry import Registry2021# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----22BLOCK = "C"23KEYS = {"C1": "p00021", "C2": "p00022", "C3": "p00150", "C4": "p00024", "C5": "p00025", "C6": "p00171", "C7": "p00189", "C8": "p00028", "C9": "p00029", "C10": "p00030", "C11": "p22028", "C12": "p00032", "C14": "p00034", "C16": "p00151", "C19": "p00190", "C20": "p00040", "C21": "p00041", "C22": "p00152", "C23": "p00182", "C24": "p13064", "C25": "p00139", "C26": "p00174", "C27": "p00183"}       # every row of the block: its label and its accession key24LEAN = {"C12": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them25# ---- end of the generated table ----2627# The Lean proofs of the rows' keys: the theorems of the frame theme that each key conjoins (lean/make_keys.py writes28# the keys FRC.Ledger.p<key> from them).29PROOFS = {30    "C12": ["FRC.Domain.Lift.temp_eq_accel", "FRC.Domain.Lift.temp_flag_free", "FRC.Domain.Lift.unruh_closes",31            "FRC.Domain.Lift.not_primitive", "FRC.Domain.Lift.classical_exponents", "FRC.Domain.Lift.classical_arity",32            "FRC.Domain.Lift.modular_shadow"],33}3435LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none3637LEDGER = {"D1": "00:C12", "D2": "00:C12", "D3": "00:C12"}38BLOCKS = {"D": "the unit-domain lattice: temperature is acceleration, the classical shadow"}39PREDICATES = {"00:C12": "D1"}4041R = Registry("00", "frame", LEDGER, PREDICATES, sources=[__file__])4243# The Subjects (p, Ω), as in the subject theme's block file: p prime, p² < Ω.44SHELLS = [(13, 233), (173, 30089), (1373, 2408561)]45# ------------------------------------------------------------------------------------------------------------46# block D: the unit-domain lattice (00:C12; 10-dimensions C1, C2, F2, F3)47# the lift (r, s, j) of L^r T^s Iq^j over the integers, the torsion-free shadow of the modular domain group48# D_p = C_p × C_{p−1} with the flag Iq = T^κ: [Θ] = [E][k_B]⁻¹ = L T⁻² = [a], flag-free; the Unruh combination49# ħ a/(c k_B) closes on it; neither mass nor temperature is primitive; the classical M-L-T-Θ exponents map to the50# domains under M ↦ Iq L⁻² T, Θ ↦ L T⁻² (the frame theme's Domain.lean: temp_eq_accel, temp_flag_free, unruh_closes, not_primitive,51# classical_exponents, classical_arity).52@R.block("D", BLOCKS["D"])53def block_D():54    """Block D — the unit-domain lattice (EXACT): D1–D3."""55    from frc.shell import (dom, L, T, FLAG, SPEED, ACCEL, ENERGY, HBAR, KB, TEMP, MASS, DOMAINS, CLASSICAL, classical, modular)56    from fractions import Fraction as Q57    # 00:C12 (p00032)58    unruh = dom(HBAR, ACCEL, (SPEED, -1), (KB, -1))59    ok = (TEMP == ACCEL == (1, -2, 0) and TEMP[2] == 0 and KB == (-1, 1, 1) and HBAR == FLAG and ENERGY[2] == 160          and unruh == TEMP and dom(ENERGY, (dom(HBAR, (SPEED, -1)), -1)) == ACCEL and MASS == (-2, 1, 1))61    R.check("D1", "in the lift: [Θ] = [E][k_B]⁻¹ = L T⁻² = [a], flag-free, with [k_B] = [ħ][c]⁻¹ = Iq L⁻¹ T from the Carrier linkage "62            "k_B c = −ħ; the Unruh combination ħ a/(c k_B) is the temperature domain exactly; Θ_P = E_P/|k_B|, written out from the energy and "63            "the linkage, is the acceleration domain; mass Iq L⁻² T and temperature are monomials in the two generators and the flag, neither primitive",64            ok, f"[Θ] = {TEMP}, Unruh = {unruh}, [k_B] = {KB}")65    # D2 the classical dictionary: exponents recovered for the twelve quantities; the arity: the classical map ℤ⁴ → ℤ³ has66    # rank 3 with kernel generated by Θ L⁻¹ T² (temperature not a fourth generator; the flag in place of the mass primitive)67    ok = all(classical(*CLASSICAL[q]) == DOMAINS[q] for q in DOMAINS)68    M = [list(classical(*e)) for e in ((1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 1, 0), (0, 0, 0, 1))]   # rows: images of M, L, T, Θ69    # rank by exact Gaussian elimination over ℚ70    A = [[Q(x) for x in row] for row in M]; rank = 071    for col in range(3):72        piv = next((i for i in range(rank, 4) if A[i][col]), None)73        if piv is None: continue74        A[rank], A[piv] = A[piv], A[rank]75        for i in range(4):76            if i != rank and A[i][col]:77                f = A[i][col] / A[rank][col]; A[i] = [a - f * b for a, b in zip(A[i], A[rank])]78        rank += 179    kernel_gen = classical(0, -1, 2, 1) == (0, 0, 0)80    gens = classical(0, 1, 0, 0) == L and classical(0, 0, 1, 0) == T and classical(1, 2, -1, 0) == FLAG81    ok &= rank == 3 and kernel_gen and gens82    R.check("D2", "classical dimensional analysis recovered in exponents and arity: the M-L-T-Θ exponents of m, v, a, E, ħ, k_B, Θ, F, p, "83            "S, P, pressure and G map to their domains under M ↦ Iq L⁻² T, Θ ↦ L T⁻²; the map ℤ⁴ → ℤ³ has rank 3, its kernel "84            "containing Θ L⁻¹ T², and L, T and the flag are classical monomials: two generators plus the flag", ok,85            f"rank {rank}; kernel Θ L⁻¹ T² ↦ {classical(0, -1, 2, 1)}")86    # D3 the modular image: on the three Subjects the identities hold in D_p = C_p × C_{4κ}, the flag has order four,87    # and the lift is a homomorphism onto the modular group (checked on random triples)88    import random89    rng, ok, det = random.Random(12), True, []90    for p, Om in SHELLS:91        kappa = (p - 1) // 492        img = lambda t: modular(t, p, kappa)93        ok &= img(TEMP) == img(ACCEL) and img(unruh) == img(TEMP)94        ok &= img(dom((FLAG, 4))) == (0, 0) and all(img(dom((FLAG, m))) != (0, 0) for m in (1, 2, 3))95        for _ in range(200):96            a = tuple(rng.randrange(-50, 50) for _ in range(3)); b = tuple(rng.randrange(-50, 50) for _ in range(3))97            ia, ib = img(a), img(b)98            ok &= img(dom(a, b)) == ((ia[0] + ib[0]) % p, (ia[1] + ib[1]) % (4 * kappa))99        det.append(f"p = {p}: [Θ] ↦ {img(TEMP)}, flag order 4")100    R.check("D3", "on the three Subjects p = 13, 173, 1373: the identities hold in the modular domain group C_p × C_{4κ}, the flag "101            "Iq = T^κ has order exactly four, and the lift is a homomorphism (200 random pairs per Subject)", ok, "; ".join(det))102103104105if __name__ == "__main__":106    blocks = [a for a in sys.argv[1:] if a in R.blocks]107    if blocks:108        for b in blocks: R.run_block(b)109        sys.exit(0 if R.summary(write=False) else 1)110    sys.exit(0 if R.verify_all() else 1)111