projective.py — frc/ledgers/master

1"""master/projective — a ledger file of the master's block C, the Subject: the rows the projective theme proves (ledger2migration, task LM25, 6 October 2026).34Block C is bound by one file per theme whose key file proves its rows (subject.py, fourier.py and this file). This file5binds C19, the Hopf section of PGL₂(F_p): the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py),6the Lean proofs its key conjoins (PROOFS), the shells, and the checks, which call the projective theme7(frc/projective.py). The Lean side is lean/FrcCore/Theme/Projective.lean, the key file lean/FrcCore/Keys/Projective.lean8and the certificate lean/FrcCore/Ledgers/Master/Projective.lean.910    python3 -m frc.ledgers.master.projective        every block, the census; exit 1 if a check fails1112Blocks:  H  the Hopf section of PGL₂          EXACT  (00:C19)1314The notebook frc/ledgers/master/projective.ipynb runs one row per cell, the cell's id its key (gate G13).15"""16import random17import sys1819from frc import arith20from frc.registry import Registry21from frc.foundation import drive22from frc.projective import mul, det, act, normal, pclass, line, boost, borel, pgl2, factor2324# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----25BLOCK = "C"26KEYS = {"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 key27LEAN = {"C19": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them28# ---- end of the generated table ----2930PROOFS = {31    "C19": ["FRC.Shell.Frame.hopf_section", "FRC.Shell.Frame.hopf_counts"],32}3334LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none3536SHELLS = [5, 13, 17, 29]        # exhaustive over PGL₂(F_p); the Subject 13 decides37SAMPLE = 173                    # the Subject 173: the factorization on random matrices3839LEDGER = {"H1": "00:C19", "H2": "00:C19", "H3": "00:C19"}40BLOCKS = {"H": "the Hopf section of PGL₂"}41PREDICATES = {"00:C19": "H1"}4243R = Registry("00", "projective", LEDGER, PREDICATES, sources=[__file__])444546def _hopf(p, nu):47    """The clauses of C19 on PGL₂(F_p), by search: the boosts fix no point, meet the Borel trivially, and the products48    (Borel class) × (boost class) are every class exactly once, p(p − 1) × (p + 1) = p(p² − 1); the factorization formula."""49    G = pgl2(p)50    P1 = line(p)51    T = sorted({pclass(boost(nu, a, b, p), p) for a in range(p) for b in range(p) if (a or b)})52    B = sorted({pclass(borel(a, b, 1, p), p) for a in range(1, p) for b in range(p)})53    I = (1, 0, 0, 1)54    ok = len(G) == p * (p * p - 1) and len(T) == p + 1 and len(B) == p * (p - 1)55    ok &= all(normal(act(t, P, p), p) != normal(P, p) for t in T if t != I for P in P1)              # (1) no fixed point56    ok &= set(T) & set(B) == {I}                                                                    # (2) T ∩ B = 157    prods = [pclass(mul(b, t, p), p) for b in B for t in T]58    ok &= len(set(prods)) == len(G) and set(prods) == set(G)                                        # (3), (4) a bijection59    for M in G:                                                                                     # the Lean proof's formula60        N, (a, b, e), (al, be) = factor(M, nu, p)61        ok &= N != 0 and a * e % p != 0 and tuple(N * v % p for v in M) == mul(borel(a, b, e, p), boost(nu, al, be, p), p)62    return ok636465def _spin(p, nu):66    """On SL₂(F_p): −I is a boost and a chart, B ∩ T = {±I}, and the products B_SL · T_SL cover half of PSL₂."""67    SL = [(a, b, c, d) for a in range(p) for b in range(p) for c in range(p) for d in range(p) if (a * d - b * c) % p == 1]68    Tsl = [boost(nu, a, b, p) for a in range(p) for b in range(p) if (a * a - nu * b * b) % p == 1]69    Bsl = [borel(a, b, pow(a, -1, p), p) for a in range(1, p) for b in range(p)]70    neg = lambda M: tuple((-v) % p for v in M)71    I = (1, 0, 0, 1); mI = neg(I)72    ok = len(SL) == p * (p * p - 1) and len(Tsl) == p + 1 and mI in Tsl and mI in Bsl73    ok &= set(Tsl) & set(Bsl) == {I, mI}74    psl = {min(M, neg(M)) for M in SL}75    img = {min(mul(b, t, p), neg(mul(b, t, p))) for b in Bsl for t in Tsl}76    ok &= len(psl) == p * (p * p - 1) // 2 and 2 * len(img) == len(psl)77    ok &= all(mul(neg(b), neg(t), p) == mul(b, t, p) for b in Bsl[:20] for t in Tsl)78    return ok, len(img), len(psl)798081# ------------------------------------------------------------------------------------------------------------82# block H: the Hopf section (00:C19)83# the boost torus is fixed-point-free on ℙ¹ and meets the Borel trivially; every frame is uniquely (cone chart) × (boost),84# p(p − 1) fibres of p + 1; on SL₂ the section obstructs at −1 (Projective.lean, hopf_section).85@R.block("H", BLOCKS["H"])86def block_H():87    """Block H — the Hopf section (EXACT): H1–H3."""88    # 00:C19 (p00039)89    p = 1390    nus = [arith.nonresidue(p), drive(p)]91    ok = all(_hopf(p, nu) for nu in nus)92    sp, img, psl = _spin(p, nus[0])93    R.check("H1", "the Subject p = 13, ν the least nonsquare and ν = g, by search over all 2 184 classes of PGL₂: the 13 non-scalar "94            "boosts fix none of the 14 points; T ∩ B = 1; the 156 × 14 products (chart) × (boost) are every class exactly once; "95            "N M = borel · boost by the proof's formula for every class; on SL₂: −I is a boost and a chart, B ∩ T = {±I}, and "96            "the products cover half of PSL₂", ok and sp, f"PSL₂: {img} of {psl} classes")97    # H2 the shells 5, 17, 29 exhaustive; the Subject 173 on random matrices98    bad = [q for q in (5, 17, 29) if not _hopf(q, arith.nonresidue(q))]99    q, nu = SAMPLE, arith.nonresidue(SAMPLE)100    rng = random.Random(173)101    for _ in range(3000):102        M = tuple(rng.randrange(q) for _ in range(4))103        if det(M, q) == 0: continue104        N, (a, b, e), (al, be) = factor(M, nu, q)105        if not (N and a * e % q and tuple(N * v % q for v in M) == mul(borel(a, b, e, q), boost(nu, al, be, q), q)): bad.append(M)106    R.check("H2", "the shells 5, 17 and 29 by search over all of PGL₂; the Subject 173 on 3 000 random matrices: the factorization "107            "formula", not bad, f"exceptions {bad[:3]}")108    # H3 the spin cover at p = 5 and 17: half of PSL₂109    out = [(q,) + _spin(q, arith.nonresidue(q)) for q in (5, 17)]110    R.check("H3", "SL₂ at p = 5 and 17: −I is a boost and a chart, B ∩ T = {±I}, the products cover half of PSL₂ (30 of 60 at p = 5)",111            all(o[1] for o in out), "; ".join(f"p={o[0]}: {o[2]} of {o[3]}" for o in out))112113114if __name__ == "__main__":115    blocks = [a for a in sys.argv[1:] if a in R.blocks]116    if blocks:117        for b in blocks: R.run_block(b)118        sys.exit(0 if R.summary(write=False) else 1)119    sys.exit(0 if R.verify_all() else 1)120