"""master/frame — a ledger file of the master's block C, the Subject: the rows the frame theme proves (the push on C12,
8 October 2026).

Block C is bound by one file per theme whose key file proves its rows (subject.py, extension.py, fourier.py,
projective.py and this file). This file binds C12, temperature and the classical arity (10-dimensions F3): the table of
keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the Subjects,
and the checks, which call the frame theme's lattice (frc/shell.py: the unit-domain lattice, the torsion-free lift of
the 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,
the key file lean/FrcCore/Keys/Frame.lean and the certificate lean/FrcCore/Ledgers/Master/Frame.lean.

    python3 -m frc.ledgers.master.frame        every block, the census; exit 1 if a check fails

Blocks:  D  the unit-domain lattice: temperature is acceleration, the classical shadow    EXACT  (00:C12)

The notebook frc/ledgers/master/frame.ipynb runs one row per cell, the cell's id its key (gate G13).
"""
import sys

from frc.registry import Registry

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "C"
KEYS = {"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 key
LEAN = {"C12": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them
# ---- end of the generated table ----

# The Lean proofs of the rows' keys: the theorems of the frame theme that each key conjoins (lean/make_keys.py writes
# the keys FRC.Ledger.p<key> from them).
PROOFS = {
    "C12": ["FRC.Domain.Lift.temp_eq_accel", "FRC.Domain.Lift.temp_flag_free", "FRC.Domain.Lift.unruh_closes",
            "FRC.Domain.Lift.not_primitive", "FRC.Domain.Lift.classical_exponents", "FRC.Domain.Lift.classical_arity",
            "FRC.Domain.Lift.modular_shadow"],
}

LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none

LEDGER = {"D1": "00:C12", "D2": "00:C12", "D3": "00:C12"}
BLOCKS = {"D": "the unit-domain lattice: temperature is acceleration, the classical shadow"}
PREDICATES = {"00:C12": "D1"}

R = Registry("00", "frame", LEDGER, PREDICATES, sources=[__file__])

# The Subjects (p, Ω), as in the subject theme's block file: p prime, p² < Ω.
SHELLS = [(13, 233), (173, 30089), (1373, 2408561)]
# ------------------------------------------------------------------------------------------------------------
# block D: the unit-domain lattice (00:C12; 10-dimensions C1, C2, F2, F3)
# the lift (r, s, j) of L^r T^s Iq^j over the integers, the torsion-free shadow of the modular domain group
# D_p = C_p × C_{p−1} with the flag Iq = T^κ: [Θ] = [E][k_B]⁻¹ = L T⁻² = [a], flag-free; the Unruh combination
# ħ a/(c k_B) closes on it; neither mass nor temperature is primitive; the classical M-L-T-Θ exponents map to the
# domains under M ↦ Iq L⁻² T, Θ ↦ L T⁻² (the frame theme's Domain.lean: temp_eq_accel, temp_flag_free, unruh_closes, not_primitive,
# classical_exponents, classical_arity).
@R.block("D", BLOCKS["D"])
def block_D():
    """Block D — the unit-domain lattice (EXACT): D1–D3."""
    from frc.shell import (dom, L, T, FLAG, SPEED, ACCEL, ENERGY, HBAR, KB, TEMP, MASS, DOMAINS, CLASSICAL, classical, modular)
    from fractions import Fraction as Q
    # 00:C12 (p00032)
    unruh = dom(HBAR, ACCEL, (SPEED, -1), (KB, -1))
    ok = (TEMP == ACCEL == (1, -2, 0) and TEMP[2] == 0 and KB == (-1, 1, 1) and HBAR == FLAG and ENERGY[2] == 1
          and unruh == TEMP and dom(ENERGY, (dom(HBAR, (SPEED, -1)), -1)) == ACCEL and MASS == (-2, 1, 1))
    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 "
            "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 "
            "the linkage, is the acceleration domain; mass Iq L⁻² T and temperature are monomials in the two generators and the flag, neither primitive",
            ok, f"[Θ] = {TEMP}, Unruh = {unruh}, [k_B] = {KB}")
    # D2 the classical dictionary: exponents recovered for the twelve quantities; the arity: the classical map ℤ⁴ → ℤ³ has
    # rank 3 with kernel generated by Θ L⁻¹ T² (temperature not a fourth generator; the flag in place of the mass primitive)
    ok = all(classical(*CLASSICAL[q]) == DOMAINS[q] for q in DOMAINS)
    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, Θ
    # rank by exact Gaussian elimination over ℚ
    A = [[Q(x) for x in row] for row in M]; rank = 0
    for col in range(3):
        piv = next((i for i in range(rank, 4) if A[i][col]), None)
        if piv is None: continue
        A[rank], A[piv] = A[piv], A[rank]
        for i in range(4):
            if i != rank and A[i][col]:
                f = A[i][col] / A[rank][col]; A[i] = [a - f * b for a, b in zip(A[i], A[rank])]
        rank += 1
    kernel_gen = classical(0, -1, 2, 1) == (0, 0, 0)
    gens = classical(0, 1, 0, 0) == L and classical(0, 0, 1, 0) == T and classical(1, 2, -1, 0) == FLAG
    ok &= rank == 3 and kernel_gen and gens
    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, "
            "S, P, pressure and G map to their domains under M ↦ Iq L⁻² T, Θ ↦ L T⁻²; the map ℤ⁴ → ℤ³ has rank 3, its kernel "
            "containing Θ L⁻¹ T², and L, T and the flag are classical monomials: two generators plus the flag", ok,
            f"rank {rank}; kernel Θ L⁻¹ T² ↦ {classical(0, -1, 2, 1)}")
    # D3 the modular image: on the three Subjects the identities hold in D_p = C_p × C_{4κ}, the flag has order four,
    # and the lift is a homomorphism onto the modular group (checked on random triples)
    import random
    rng, ok, det = random.Random(12), True, []
    for p, Om in SHELLS:
        kappa = (p - 1) // 4
        img = lambda t: modular(t, p, kappa)
        ok &= img(TEMP) == img(ACCEL) and img(unruh) == img(TEMP)
        ok &= img(dom((FLAG, 4))) == (0, 0) and all(img(dom((FLAG, m))) != (0, 0) for m in (1, 2, 3))
        for _ in range(200):
            a = tuple(rng.randrange(-50, 50) for _ in range(3)); b = tuple(rng.randrange(-50, 50) for _ in range(3))
            ia, ib = img(a), img(b)
            ok &= img(dom(a, b)) == ((ia[0] + ib[0]) % p, (ia[1] + ib[1]) % (4 * kappa))
        det.append(f"p = {p}: [Θ] ↦ {img(TEMP)}, flag order 4")
    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 "
            "Iq = T^κ has order exactly four, and the lift is a homomorphism (200 random pairs per Subject)", ok, "; ".join(det))



if __name__ == "__main__":
    blocks = [a for a in sys.argv[1:] if a in R.blocks]
    if blocks:
        for b in blocks: R.run_block(b)
        sys.exit(0 if R.summary(write=False) else 1)
    sys.exit(0 if R.verify_all() else 1)