horizon.py — frc/ledgers/master

1"""master/horizon — a ledger file of the master's block Z, the horizon: the rows the horizon theme proves (ledger2migration, task LM26, 6 October 2026).34Block Z is bound by one file per theme whose key file proves its rows: this file (the horizon theme) and5frc/ledgers/master/logic.py (the logic theme). This file binds Z10, the shell theorem, whose key p20043 it shares with620:E12: the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins7(PROOFS), the shells, and the checks, which call the horizon theme (frc/horizon.py). The Lean side is8lean/FrcCore/Theme/Horizon.lean, the key file lean/FrcCore/Keys/Horizon.lean and the certificate9lean/FrcCore/Ledgers/Master/Horizon.lean.1011    python3 -m frc.ledgers.master.horizon        every block, the census; exit 1 if a check fails1213Blocks:  K  the shell theorem: the modes, the scale-shift, the readout on Tr = 1     EXACT  (00:Z10)1415The notebook frc/ledgers/master/horizon.ipynb runs one row per cell, the cell's id its key (gate G13).16"""17import random18import sys1920from frc import arith21from frc.registry import Registry22from frc.foundation import drive23from frc.horizon import zeta, mode_coeffs, expand, shift, fixed_points, readout, trace2425# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----26BLOCK = "Z"27KEYS = {"Z1": "p00186", "Z2": "p00110", "Z3": "p00111", "Z4": "p00112", "Z5": "p27021", "Z6": "p00114", "Z7": "p00115", "Z8": "p00116", "Z9": "p00187", "Z10": "p20043", "Z11": "p00135"}       # every row of the block: its label and its accession key28LEAN = {"Z10": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them29# ---- end of the generated table ----3031# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys32# FRC.Ledger.p<key> from them). The master's block file is the binding's source, as a paper's \lean{} cells are its own.33PROOFS = {34    "Z10": ["FRC.Horizon.zero_slot", "FRC.Horizon.mode_expansion", "FRC.Horizon.shift_power_character",35            "FRC.Horizon.eigenphase", "FRC.Horizon.shift_trace", "FRC.Horizon.readout_on_line",36            "FRC.Horizon.readout_slot_index"],37}3839LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none4041SUBJECTS = [13, 173, 1373]      # the Subjects of the Subject's block file42SWEEP = 400                     # the sweep runs over every prime p = 4κ + 1 below it4344LEDGER = {"K1": "00:Z10", "K2": "00:Z10", "K3": "00:Z10"}45BLOCKS = {"K": "the shell theorem: the modes, the scale-shift, the readout on Tr = 1"}46PREDICATES = {"00:Z10": "K1"}4748R = Registry("00", "horizon", LEDGER, PREDICATES, sources=[__file__])495051def _shells(lo, hi):52    return [n for n in range(lo, hi) if n % 4 == 1 and arith.is_prime(n)]535455def _prime_vector(p, g):56    """20-rh's prime vector on the cycle: v_j = 1 when the residue g^j, read in [1, p), is a prime, else 0."""57    return [1 if arith.is_prime(pow(g, j, p)) else 0 for j in range(p - 1)]585960def _shell_theorem(p, vectors):61    """The clauses of Z10 on the frame (p, drive(p)): the finite zeta, the expansion of each vector, the eigen-relation62    and its root of unity, the fixed-point count of every shift, the readouts on Tr = 1 and the slot indices."""63    g, n, k = drive(p), p - 1, (p - 1) // 464    ok = all(zeta(p, e) == 0 for e in range(1, n)) and zeta(p, n) == p - 165    for v in vectors:66        c = mode_coeffs(p, g, v)67        ok &= all(expand(p, g, c, j) == v[j] % p for j in range(n))68    rs = range(0, 2 * n + 1) if n <= 60 else list(range(0, 8)) + [n, 2 * n, n + 1]69    for r in rs:70        lam = [pow(pow(g, r, p), e, p) for e in range(n)]71        ok &= all(pow(shift(p, g, r, x), e, p) == lam[e] * pow(x, e, p) % p for x in range(1, p, max(1, p // 40)) for e in range(0, n, max(1, n // 12)))72        ok &= all(pow(l, n, p) == 1 for l in lam)73        ok &= len(fixed_points(p, g, r)) == (n if r % n == 0 else 0)74    half = (2 * k + 1) % p75    ok &= 2 * half % p == 1 and half == (-2 * k) % p76    ok &= all(trace(p, readout(p, t)) == 1 and readout(p, t)[0] == half for t in range(p))77    ok &= all((-pow(g, e, p)) % p not in (0, p - 1) for e in range(1, n))78    return ok798081# ------------------------------------------------------------------------------------------------------------82# block K: the shell theorem (00:Z10)83# the finite zeta vanishes on the nonterminal modes; every vector expands in the power modes; the scale-shift has the84# modes as eigenvectors with (p − 1)-th roots of unity as eigenvalues and fixes n·[n | r] points; every readout lies on85# Tr = 1 (Horizon.lean: zero_slot, mode_expansion, shift_power_character, eigenphase, shift_trace, readout_on_line,86# readout_slot_index).87@R.block("K", BLOCKS["K"])88def block_K():89    """Block K — the shell theorem (EXACT): K1–K3."""90    # 00:Z10 (p20043)91    rng = random.Random(10)92    bad = []93    for p in _shells(5, SWEEP):94        g = drive(p)95        vs = [_prime_vector(p, g), [rng.randrange(p) for _ in range(p - 1)]]96        if not _shell_theorem(p, vs): bad.append(p)97    R.check("K1", f"every prime p = 4κ + 1 below {SWEEP} with its drive: Z(k) = 0 for 0 < k < p − 1 and Z(p − 1) = −1; the prime "98            "vector and a random vector expand exactly in the power modes with the Lean proof's coefficients; (g^r x)^k = "99            "(g^r)^k x^k with (g^r)^k an (p − 1)-th root of unity; g^r fixes p − 1 points when (p − 1) | r and none otherwise; "100            "every readout 2⁻¹ + θη has trace 1; no slot index is 0 or −1", not bad,101            f"{len(_shells(5, SWEEP))} shells; exceptions {bad}")102    # K2 the Subjects 13, 173 and 1373: the expansion of every basis vector at 13, of the prime vector at all three103    ok, det = True, []104    for p in SUBJECTS:105        g, n = drive(p), p - 1106        vs = [_prime_vector(p, g)] + ([[1 if j == i else 0 for j in range(n)] for i in range(n)] if p == 13 else [])107        ok &= _shell_theorem(p, vs)108        det.append(f"p={p}: {sum(vs[0])} prime residues")109    R.check("K2", "the Subjects 13, 173 and 1373: the clauses of K1, with every basis vector at 13 (the modes span the cycle)", ok,110            "; ".join(det))111    # K3 a second method: the coefficients solve the Vandermonde system x_j^k (Gaussian elimination mod p)112    bad = []113    for p in (13, 17, 29, 37):114        g, n = drive(p), p - 1115        v = [rng.randrange(p) for _ in range(n)]116        A = [[pow(pow(g, j, p), e, p) for e in range(n)] + [v[j]] for j in range(n)]117        for col in range(n):                                    # Gauss-Jordan mod p118            piv = next(r for r in range(col, n) if A[r][col] % p)119            A[col], A[piv] = A[piv], A[col]120            inv = pow(A[col][col], -1, p)121            A[col] = [a * inv % p for a in A[col]]122            for r in range(n):123                if r != col and A[r][col]:124                    f = A[r][col]; A[r] = [(a - f * b) % p for a, b in zip(A[r], A[col])]125        if [A[e][n] for e in range(n)] != mode_coeffs(p, g, v): bad.append(p)126    R.check("K3", "p = 13, 17, 29, 37: the coefficients of a random vector by Gauss–Jordan elimination on the Vandermonde system "127            "equal the Lean proof's c_k = −Σ v_l g^((n−l)k)", not bad, f"exceptions {bad}")128129130if __name__ == "__main__":131    blocks = [a for a in sys.argv[1:] if a in R.blocks]132    if blocks:133        for b in blocks: R.run_block(b)134        sys.exit(0 if R.summary(write=False) else 1)135    sys.exit(0 if R.verify_all() else 1)136