"""master/horizon — a ledger file of the master's block Z, the horizon: the rows the horizon theme proves (ledger
migration, task LM26, 6 October 2026).

Block Z is bound by one file per theme whose key file proves its rows: this file (the horizon theme) and
frc/ledgers/master/logic.py (the logic theme). This file binds Z10, the shell theorem, whose key p20043 it shares with
20:E12: the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins
(PROOFS), the shells, and the checks, which call the horizon theme (frc/horizon.py). The Lean side is
lean/FrcCore/Theme/Horizon.lean, the key file lean/FrcCore/Keys/Horizon.lean and the certificate
lean/FrcCore/Ledgers/Master/Horizon.lean.

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

Blocks:  K  the shell theorem: the modes, the scale-shift, the readout on Tr = 1     EXACT  (00:Z10)

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

from frc import arith
from frc.registry import Registry
from frc.foundation import drive
from frc.horizon import zeta, mode_coeffs, expand, shift, fixed_points, readout, trace

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "Z"
KEYS = {"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 key
LEAN = {"Z10": "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 themes that each key conjoins (lean/make_keys.py writes the keys
# 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.
PROOFS = {
    "Z10": ["FRC.Horizon.zero_slot", "FRC.Horizon.mode_expansion", "FRC.Horizon.shift_power_character",
            "FRC.Horizon.eigenphase", "FRC.Horizon.shift_trace", "FRC.Horizon.readout_on_line",
            "FRC.Horizon.readout_slot_index"],
}

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

SUBJECTS = [13, 173, 1373]      # the Subjects of the Subject's block file
SWEEP = 400                     # the sweep runs over every prime p = 4κ + 1 below it

LEDGER = {"K1": "00:Z10", "K2": "00:Z10", "K3": "00:Z10"}
BLOCKS = {"K": "the shell theorem: the modes, the scale-shift, the readout on Tr = 1"}
PREDICATES = {"00:Z10": "K1"}

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


def _shells(lo, hi):
    return [n for n in range(lo, hi) if n % 4 == 1 and arith.is_prime(n)]


def _prime_vector(p, g):
    """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."""
    return [1 if arith.is_prime(pow(g, j, p)) else 0 for j in range(p - 1)]


def _shell_theorem(p, vectors):
    """The clauses of Z10 on the frame (p, drive(p)): the finite zeta, the expansion of each vector, the eigen-relation
    and its root of unity, the fixed-point count of every shift, the readouts on Tr = 1 and the slot indices."""
    g, n, k = drive(p), p - 1, (p - 1) // 4
    ok = all(zeta(p, e) == 0 for e in range(1, n)) and zeta(p, n) == p - 1
    for v in vectors:
        c = mode_coeffs(p, g, v)
        ok &= all(expand(p, g, c, j) == v[j] % p for j in range(n))
    rs = range(0, 2 * n + 1) if n <= 60 else list(range(0, 8)) + [n, 2 * n, n + 1]
    for r in rs:
        lam = [pow(pow(g, r, p), e, p) for e in range(n)]
        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)))
        ok &= all(pow(l, n, p) == 1 for l in lam)
        ok &= len(fixed_points(p, g, r)) == (n if r % n == 0 else 0)
    half = (2 * k + 1) % p
    ok &= 2 * half % p == 1 and half == (-2 * k) % p
    ok &= all(trace(p, readout(p, t)) == 1 and readout(p, t)[0] == half for t in range(p))
    ok &= all((-pow(g, e, p)) % p not in (0, p - 1) for e in range(1, n))
    return ok


# ------------------------------------------------------------------------------------------------------------
# block K: the shell theorem (00:Z10)
# the finite zeta vanishes on the nonterminal modes; every vector expands in the power modes; the scale-shift has the
# modes as eigenvectors with (p − 1)-th roots of unity as eigenvalues and fixes n·[n | r] points; every readout lies on
# Tr = 1 (Horizon.lean: zero_slot, mode_expansion, shift_power_character, eigenphase, shift_trace, readout_on_line,
# readout_slot_index).
@R.block("K", BLOCKS["K"])
def block_K():
    """Block K — the shell theorem (EXACT): K1–K3."""
    # 00:Z10 (p20043)
    rng = random.Random(10)
    bad = []
    for p in _shells(5, SWEEP):
        g = drive(p)
        vs = [_prime_vector(p, g), [rng.randrange(p) for _ in range(p - 1)]]
        if not _shell_theorem(p, vs): bad.append(p)
    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 "
            "vector and a random vector expand exactly in the power modes with the Lean proof's coefficients; (g^r x)^k = "
            "(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; "
            "every readout 2⁻¹ + θη has trace 1; no slot index is 0 or −1", not bad,
            f"{len(_shells(5, SWEEP))} shells; exceptions {bad}")
    # K2 the Subjects 13, 173 and 1373: the expansion of every basis vector at 13, of the prime vector at all three
    ok, det = True, []
    for p in SUBJECTS:
        g, n = drive(p), p - 1
        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 [])
        ok &= _shell_theorem(p, vs)
        det.append(f"p={p}: {sum(vs[0])} prime residues")
    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,
            "; ".join(det))
    # K3 a second method: the coefficients solve the Vandermonde system x_j^k (Gaussian elimination mod p)
    bad = []
    for p in (13, 17, 29, 37):
        g, n = drive(p), p - 1
        v = [rng.randrange(p) for _ in range(n)]
        A = [[pow(pow(g, j, p), e, p) for e in range(n)] + [v[j]] for j in range(n)]
        for col in range(n):                                    # Gauss-Jordan mod p
            piv = next(r for r in range(col, n) if A[r][col] % p)
            A[col], A[piv] = A[piv], A[col]
            inv = pow(A[col][col], -1, p)
            A[col] = [a * inv % p for a in A[col]]
            for r in range(n):
                if r != col and A[r][col]:
                    f = A[r][col]; A[r] = [(a - f * b) % p for a, b in zip(A[r], A[col])]
        if [A[e][n] for e in range(n)] != mode_coeffs(p, g, v): bad.append(p)
    R.check("K3", "p = 13, 17, 29, 37: the coefficients of a random vector by Gauss–Jordan elimination on the Vandermonde system "
            "equal the Lean proof's c_k = −Σ v_l g^((n−l)k)", not bad, f"exceptions {bad}")


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)