"""master/fourier — a ledger file of the master's block C, the Subject: the rows the fourier theme proves (ledger
migration, task LM25, 6 October 2026).

Block C is bound by one file per theme whose key file proves its rows: frc/ledgers/master/subject.py (the subject theme,
task LM24), this file (the fourier theme) and frc/ledgers/master/projective.py (the projective theme). This file binds C2
and C7 (since 9 October 2026 their keys also conjoin the declarations of 6-fourier's rows B5, C3, D4 and C9, the
paper's propagation list row 5): the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs each key conjoins
(PROOFS), the shells, and the checks, which call the fourier theme (frc/fourier.py). Each check names the rows it decides
or corroborates (LEDGER), under a `# 00:C2 (p00022)` marker on the check that decides the row (PREDICATES). The Lean side
is lean/FrcCore/Theme/Fourier.lean, the key file lean/FrcCore/Keys/Fourier.lean and the certificate
lean/FrcCore/Ledgers/Master/Fourier.lean.

    python3 -m frc.ledgers.master.fourier        every block, the census; exit 1 if a check fails
    python3 -m frc.ledgers.master.fourier O      one block (M or O)

Blocks:  M  scale-shift duality: the fractional family on the cycle     EXACT  (00:C2)
         O  orientation is derived: the conjugate frame, ħ^S = ±1         EXACT  (00:C7)

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

from frc import arith
from frc.registry import Registry
from frc.foundation import drive, quarter_turn, element_order
from frc.fourier import transform, identity, matmul, matpow, projectors, frft, meridian

# ---- 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 = {"C2": "core", "C7": "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 = {
    "C2": ["FRC.Shell.Frame.scale_shift", "FRC.Shell.Frame.frft_dilation",
           # the paper's declarations the row cites (6-fourier's propagation list, row 5; 9 October 2026): 6:B5 (p06012),
           # the operator relations; 6:C3 (p06017), the fractional family's additivity, cardinal values, period and powers;
           # 6:D4 (p06027), the meridian-scale covariance with its p = 13 ladder
           "FRC.Shell.Frame.W_sq'", "FRC.Shell.Frame.F_sq", "FRC.Shell.Frame.J_sq",
           "FRC.Shell.Frame.frft_add", "FRC.Shell.Frame.frft_cardinal", "FRC.Shell.Frame.frft_period", "FRC.Shell.Frame.frft_pow",
           "FRC.Shell.meridian_scale", "FRC.Shell.meridian_step", "FRC.Shell.scale_periodic", "FRC.Shell.ladder13"],
    "C7": ["FRC.Shell.Frame.orientation",
           # 6:C9 (p06023), the conjugate frame: its Fourier matrix, its projectors (the same propagation row)
           "FRC.Shell.Frame.inv_frame", "FRC.Shell.Frame.Fmat_conj", "FRC.Shell.Frame.proj_conj"],
}

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

# The Subjects p = 4κ + 1 with their Carriers Ω = 4S + 1, as in the Subject's block file.
SHELLS = [(13, 233), (173, 30089), (1373, 2408561)]
SWEEP = 60                      # the matrix sweeps run over every prime p = 4κ + 1 below it
CHARTS = 5000                   # the Carrier sweep runs over every prime Ω = 4S + 1 below it

# The rows each check decides or corroborates.
LEDGER = {"M1": "00:C2", "M2": "00:C2", "M3": "00:C2",
          "O1": "00:C7", "O2": "00:C7", "O3": "00:C7"}

BLOCKS = {"M": "scale-shift duality: the fractional family on the cycle", "O": "orientation is derived: the conjugate frame"}

# the deciding check of each row
PREDICATES = {"00:C2": "M1", "00:C7": "O1"}

R = Registry("00", "fourier", 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 _scale_shift(p, pairs=None):
    """The clauses of C2 on the frame (p, drive(p)): cardinal values, additivity on the given pairs (all by default),
    periodicity, (F^[1])^κ = F, and the meridian covariance."""
    g, n, k = drive(p), p - 1, (p - 1) // 4
    W, J, F = transform(p, g)
    P = projectors(p, g)
    fam = {s: frft(p, g, s, P) for s in range(n)}
    FJ = matmul(F, J, p)
    ok = fam[0] == identity(n) and fam[k] == F and fam[2 * k] == J and fam[3 * k] == FJ
    ok &= matmul(FJ, F, p) == identity(n) and matmul(F, F, p) == J
    ok &= frft(p, g, n + 5, P) == fam[5 % n]
    pairs = pairs if pairs is not None else [(s, r) for s in range(n) for r in range(n)]
    ok &= all(matmul(fam[s], fam[r], p) == fam[(s + r) % n] for s, r in pairs)
    ok &= matpow(fam[1], k, p) == F
    ok &= all([x * pow(g, r, p) % p for x in meridian(p, g, k, m)] == meridian(p, g, k, m + r) for m in range(n) for r in range(n))
    return ok


# ------------------------------------------------------------------------------------------------------------
# block M: scale-shift duality (00:C2)
# dilation x ↦ g x advances the meridian index; over the cycle the fractional family F^[s] = Σ_ℓ z^(ℓs) Π_ℓ is a
# representation of Z/(p−1) whose quarter-turn value F^[κ] is the transform F (Fourier.lean, scale_shift).
@R.block("M", BLOCKS["M"])
def block_M():
    """Block M — scale-shift duality (EXACT): M1–M3."""
    # 00:C2 (p00022)
    ok = _scale_shift(13)
    R.check("M1", "the Subject p = 13 with its drive g = 11: the projectors from the powers of F, F^[0] = I, F^[κ] = F, F^[2κ] = J, "
            "F^[3κ] = F J = F⁻¹, F^[s+r] = F^[s] F^[r] for all 144 pairs, F^[s+12] = F^[s], (F^[1])^κ = F, and S_r(M_m) = M_{m+r} "
            "for all m, r < 12", ok, f"n = 12, g = {drive(13)}")
    # M2 every prime p = 4κ + 1 below SWEEP: the same, additivity on the pairs (s, 1) and (s, κ)
    bad = []
    for p in _shells(5, SWEEP):
        n, k = p - 1, (p - 1) // 4
        if not _scale_shift(p, [(s, 1) for s in range(n)] + [(s, k) for s in range(n)]): bad.append(p)
    R.check("M2", f"every prime p = 4κ + 1 below {SWEEP} with its drive: the cardinal values, additivity on the pairs (s, 1) and "
            "(s, κ), periodicity, (F^[1])^κ = F and the meridian covariance", not bad,
            f"{len(_shells(5, SWEEP))} shells; exceptions {bad}")
    # M3 the Subject p = 173: the cardinal values and additivity on twelve pairs
    p = 173; n, k = p - 1, (p - 1) // 4
    g = drive(p); W, J, F = transform(p, g); P = projectors(p, g)
    fam = {s: frft(p, g, s, P) for s in (0, 1, 2, 5, k, 2 * k, 3 * k, k + 1, 7, 12, 50, 55, 60, 172 - 5)}
    ok = fam[0] == identity(n) and fam[k] == F and fam[2 * k] == J and fam[3 * k] == matmul(F, J, p)
    ok &= all(matmul(fam[s], fam[r], p) == frft(p, g, (s + r) % n, P) for s, r in [(1, 1), (5, 7), (k, 1), (50, 5), (60, 12), (172 - 5, 5)])
    R.check("M3", "the Subject p = 173 (n = 172) with its drive: F^[0] = I, F^[κ] = F, F^[2κ] = J, F^[3κ] = F J, and F^[s+r] = "
            "F^[s] F^[r] on six pairs", ok, f"g = {g}")


# ------------------------------------------------------------------------------------------------------------
# block O: orientation is derived (00:C7)
# ħ^S = ±1 on a Carrier with S even; on a frame i = (g⁻¹)^κ, the conjugate g⁻¹ is a frame with quarter-turn −i,
# transform −F J and projectors Π_{ℓ+2} (Fourier.lean, orientation).
def _conjugate(p):
    g, n, k = drive(p), p - 1, (p - 1) // 4
    z = pow(g, -1, p)
    i = (-pow(g, k, p)) % p
    _, J, F = transform(p, g)
    _, _, Fz = transform(p, z)
    P, Pz = projectors(p, g), projectors(p, z)
    FJ = matmul(F, J, p)
    ok = pow(z, k, p) == i and element_order(z, p) == n and (-pow(z, k, p)) % p == (p - i) % p
    ok &= Fz == [[(-v) % p for v in row] for row in FJ]
    ok &= all(Pz[l] == P[(l + 2) % 4] for l in range(4))
    return ok


@R.block("O", BLOCKS["O"])
def block_O():
    """Block O — orientation is derived (EXACT): O1–O3."""
    # 00:C7 (p00172)
    ok, det = True, []
    for p, Om in SHELLS:
        S = (Om - 1) // 4
        h = quarter_turn(Om)
        hS = pow(h, S, Om)
        ok &= S % 2 == 0 and hS in (1, Om - 1) and hS == (1 if (S // 2) % 2 == 0 else Om - 1)
        det.append(f"Ω={Om}: ħ={h}, ħ^S={'1' if hS == 1 else '−1'}")
    ok &= _conjugate(13) and _conjugate(29)
    R.check("O1", "on the three Carriers (S = 58, 7 522, 602 140, all even): ħ^S = (−1)^(S/2) ∈ {±1}; on the Subjects 13 and 29: "
            "(g⁻¹)^κ = i, g⁻¹ has order p − 1, the conjugate transform is −F J and its projectors are Π_{ℓ+2}", ok, "; ".join(det))
    # O2 every prime p = 4κ + 1 below SWEEP: the conjugate frame
    bad = [p for p in _shells(5, SWEEP) if not _conjugate(p)]
    R.check("O2", f"every prime p = 4κ + 1 below {SWEEP}: the conjugate frame's quarter-turn, transform and projectors", not bad,
            f"{len(_shells(5, SWEEP))} shells; exceptions {bad}")
    # O3 every prime Ω = 4S + 1 below CHARTS: ħ^S = ±1 exactly when S is even (for S odd, ħ^S = ±ħ)
    bad = []
    for Om in _shells(5, CHARTS):
        S = (Om - 1) // 4; h = quarter_turn(Om); hS = pow(h, S, Om)
        if (hS in (1, Om - 1)) != (S % 2 == 0) or (S % 2 == 1 and hS not in (h, Om - h)): bad.append(Om)
    R.check("O3", f"every prime Ω = 4S + 1 below {CHARTS}: ħ^S ∈ {{±1}} exactly when S is even, and ħ^S = ±ħ when S is odd", not bad,
            f"{len(_shells(5, CHARTS))} charts; exceptions {bad[:5]}")


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)