fourier.py — frc/ledgers/master

1"""master/fourier — a ledger file of the master's block C, the Subject: the rows the fourier theme proves (ledger2migration, task LM25, 6 October 2026).34Block C is bound by one file per theme whose key file proves its rows: frc/ledgers/master/subject.py (the subject theme,5task LM24), this file (the fourier theme) and frc/ledgers/master/projective.py (the projective theme). This file binds C26and C7 (since 9 October 2026 their keys also conjoin the declarations of 6-fourier's rows B5, C3, D4 and C9, the7paper'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 conjoins8(PROOFS), the shells, and the checks, which call the fourier theme (frc/fourier.py). Each check names the rows it decides9or corroborates (LEDGER), under a `# 00:C2 (p00022)` marker on the check that decides the row (PREDICATES). The Lean side10is lean/FrcCore/Theme/Fourier.lean, the key file lean/FrcCore/Keys/Fourier.lean and the certificate11lean/FrcCore/Ledgers/Master/Fourier.lean.1213    python3 -m frc.ledgers.master.fourier        every block, the census; exit 1 if a check fails14    python3 -m frc.ledgers.master.fourier O      one block (M or O)1516Blocks:  M  scale-shift duality: the fractional family on the cycle     EXACT  (00:C2)17         O  orientation is derived: the conjugate frame, ħ^S = ±1         EXACT  (00:C7)1819The notebook frc/ledgers/master/fourier.ipynb runs one row per cell, the cell's id its key (gate G13).20"""21import sys2223from frc import arith24from frc.registry import Registry25from frc.foundation import drive, quarter_turn, element_order26from frc.fourier import transform, identity, matmul, matpow, projectors, frft, meridian2728# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----29BLOCK = "C"30KEYS = {"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 key31LEAN = {"C2": "core", "C7": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them32# ---- end of the generated table ----3334# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys35# 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.36PROOFS = {37    "C2": ["FRC.Shell.Frame.scale_shift", "FRC.Shell.Frame.frft_dilation",38           # the paper's declarations the row cites (6-fourier's propagation list, row 5; 9 October 2026): 6:B5 (p06012),39           # the operator relations; 6:C3 (p06017), the fractional family's additivity, cardinal values, period and powers;40           # 6:D4 (p06027), the meridian-scale covariance with its p = 13 ladder41           "FRC.Shell.Frame.W_sq'", "FRC.Shell.Frame.F_sq", "FRC.Shell.Frame.J_sq",42           "FRC.Shell.Frame.frft_add", "FRC.Shell.Frame.frft_cardinal", "FRC.Shell.Frame.frft_period", "FRC.Shell.Frame.frft_pow",43           "FRC.Shell.meridian_scale", "FRC.Shell.meridian_step", "FRC.Shell.scale_periodic", "FRC.Shell.ladder13"],44    "C7": ["FRC.Shell.Frame.orientation",45           # 6:C9 (p06023), the conjugate frame: its Fourier matrix, its projectors (the same propagation row)46           "FRC.Shell.Frame.inv_frame", "FRC.Shell.Frame.Fmat_conj", "FRC.Shell.Frame.proj_conj"],47}4849LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none5051# The Subjects p = 4κ + 1 with their Carriers Ω = 4S + 1, as in the Subject's block file.52SHELLS = [(13, 233), (173, 30089), (1373, 2408561)]53SWEEP = 60                      # the matrix sweeps run over every prime p = 4κ + 1 below it54CHARTS = 5000                   # the Carrier sweep runs over every prime Ω = 4S + 1 below it5556# The rows each check decides or corroborates.57LEDGER = {"M1": "00:C2", "M2": "00:C2", "M3": "00:C2",58          "O1": "00:C7", "O2": "00:C7", "O3": "00:C7"}5960BLOCKS = {"M": "scale-shift duality: the fractional family on the cycle", "O": "orientation is derived: the conjugate frame"}6162# the deciding check of each row63PREDICATES = {"00:C2": "M1", "00:C7": "O1"}6465R = Registry("00", "fourier", LEDGER, PREDICATES, sources=[__file__])666768def _shells(lo, hi):69    return [n for n in range(lo, hi) if n % 4 == 1 and arith.is_prime(n)]707172def _scale_shift(p, pairs=None):73    """The clauses of C2 on the frame (p, drive(p)): cardinal values, additivity on the given pairs (all by default),74    periodicity, (F^[1])^κ = F, and the meridian covariance."""75    g, n, k = drive(p), p - 1, (p - 1) // 476    W, J, F = transform(p, g)77    P = projectors(p, g)78    fam = {s: frft(p, g, s, P) for s in range(n)}79    FJ = matmul(F, J, p)80    ok = fam[0] == identity(n) and fam[k] == F and fam[2 * k] == J and fam[3 * k] == FJ81    ok &= matmul(FJ, F, p) == identity(n) and matmul(F, F, p) == J82    ok &= frft(p, g, n + 5, P) == fam[5 % n]83    pairs = pairs if pairs is not None else [(s, r) for s in range(n) for r in range(n)]84    ok &= all(matmul(fam[s], fam[r], p) == fam[(s + r) % n] for s, r in pairs)85    ok &= matpow(fam[1], k, p) == F86    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))87    return ok888990# ------------------------------------------------------------------------------------------------------------91# block M: scale-shift duality (00:C2)92# dilation x ↦ g x advances the meridian index; over the cycle the fractional family F^[s] = Σ_ℓ z^(ℓs) Π_ℓ is a93# representation of Z/(p−1) whose quarter-turn value F^[κ] is the transform F (Fourier.lean, scale_shift).94@R.block("M", BLOCKS["M"])95def block_M():96    """Block M — scale-shift duality (EXACT): M1–M3."""97    # 00:C2 (p00022)98    ok = _scale_shift(13)99    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, "100            "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} "101            "for all m, r < 12", ok, f"n = 12, g = {drive(13)}")102    # M2 every prime p = 4κ + 1 below SWEEP: the same, additivity on the pairs (s, 1) and (s, κ)103    bad = []104    for p in _shells(5, SWEEP):105        n, k = p - 1, (p - 1) // 4106        if not _scale_shift(p, [(s, 1) for s in range(n)] + [(s, k) for s in range(n)]): bad.append(p)107    R.check("M2", f"every prime p = 4κ + 1 below {SWEEP} with its drive: the cardinal values, additivity on the pairs (s, 1) and "108            "(s, κ), periodicity, (F^[1])^κ = F and the meridian covariance", not bad,109            f"{len(_shells(5, SWEEP))} shells; exceptions {bad}")110    # M3 the Subject p = 173: the cardinal values and additivity on twelve pairs111    p = 173; n, k = p - 1, (p - 1) // 4112    g = drive(p); W, J, F = transform(p, g); P = projectors(p, g)113    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)}114    ok = fam[0] == identity(n) and fam[k] == F and fam[2 * k] == J and fam[3 * k] == matmul(F, J, p)115    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)])116    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] = "117            "F^[s] F^[r] on six pairs", ok, f"g = {g}")118119120# ------------------------------------------------------------------------------------------------------------121# block O: orientation is derived (00:C7)122# ħ^S = ±1 on a Carrier with S even; on a frame i = (g⁻¹)^κ, the conjugate g⁻¹ is a frame with quarter-turn −i,123# transform −F J and projectors Π_{ℓ+2} (Fourier.lean, orientation).124def _conjugate(p):125    g, n, k = drive(p), p - 1, (p - 1) // 4126    z = pow(g, -1, p)127    i = (-pow(g, k, p)) % p128    _, J, F = transform(p, g)129    _, _, Fz = transform(p, z)130    P, Pz = projectors(p, g), projectors(p, z)131    FJ = matmul(F, J, p)132    ok = pow(z, k, p) == i and element_order(z, p) == n and (-pow(z, k, p)) % p == (p - i) % p133    ok &= Fz == [[(-v) % p for v in row] for row in FJ]134    ok &= all(Pz[l] == P[(l + 2) % 4] for l in range(4))135    return ok136137138@R.block("O", BLOCKS["O"])139def block_O():140    """Block O — orientation is derived (EXACT): O1–O3."""141    # 00:C7 (p00172)142    ok, det = True, []143    for p, Om in SHELLS:144        S = (Om - 1) // 4145        h = quarter_turn(Om)146        hS = pow(h, S, Om)147        ok &= S % 2 == 0 and hS in (1, Om - 1) and hS == (1 if (S // 2) % 2 == 0 else Om - 1)148        det.append(f"Ω={Om}: ħ={h}, ħ^S={'1' if hS == 1 else '−1'}")149    ok &= _conjugate(13) and _conjugate(29)150    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: "151            "(g⁻¹)^κ = i, g⁻¹ has order p − 1, the conjugate transform is −F J and its projectors are Π_{ℓ+2}", ok, "; ".join(det))152    # O2 every prime p = 4κ + 1 below SWEEP: the conjugate frame153    bad = [p for p in _shells(5, SWEEP) if not _conjugate(p)]154    R.check("O2", f"every prime p = 4κ + 1 below {SWEEP}: the conjugate frame's quarter-turn, transform and projectors", not bad,155            f"{len(_shells(5, SWEEP))} shells; exceptions {bad}")156    # O3 every prime Ω = 4S + 1 below CHARTS: ħ^S = ±1 exactly when S is even (for S odd, ħ^S = ±ħ)157    bad = []158    for Om in _shells(5, CHARTS):159        S = (Om - 1) // 4; h = quarter_turn(Om); hS = pow(h, S, Om)160        if (hS in (1, Om - 1)) != (S % 2 == 0) or (S % 2 == 1 and hS not in (h, Om - h)): bad.append(Om)161    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,162            f"{len(_shells(5, CHARTS))} charts; exceptions {bad[:5]}")163164165if __name__ == "__main__":166    blocks = [a for a in sys.argv[1:] if a in R.blocks]167    if blocks:168        for b in blocks: R.run_block(b)169        sys.exit(0 if R.summary(write=False) else 1)170    sys.exit(0 if R.verify_all() else 1)171