"""master/projective — a ledger file of the master's block C, the Subject: the rows the projective theme proves (ledger migration, task LM25, 6 October 2026). Block C is bound by one file per theme whose key file proves its rows (subject.py, fourier.py and this file). This file binds C19, the Hopf section of PGL₂(F_p): 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 projective theme (frc/projective.py). The Lean side is lean/FrcCore/Theme/Projective.lean, the key file lean/FrcCore/Keys/Projective.lean and the certificate lean/FrcCore/Ledgers/Master/Projective.lean. python3 -m frc.ledgers.master.projective every block, the census; exit 1 if a check fails Blocks: H the Hopf section of PGL₂ EXACT (00:C19) The notebook frc/ledgers/master/projective.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.projective import mul, det, act, normal, pclass, line, boost, borel, pgl2, factor # ---- 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 = {"C19": "core"} # the rows with a Lean declaration: the libraries whose key files prove them # ---- end of the generated table ---- PROOFS = { "C19": ["FRC.Shell.Frame.hopf_section", "FRC.Shell.Frame.hopf_counts"], } LEAN_ONLY = () # the rows with a Lean declaration and no python check (gate G12): none SHELLS = [5, 13, 17, 29] # exhaustive over PGL₂(F_p); the Subject 13 decides SAMPLE = 173 # the Subject 173: the factorization on random matrices LEDGER = {"H1": "00:C19", "H2": "00:C19", "H3": "00:C19"} BLOCKS = {"H": "the Hopf section of PGL₂"} PREDICATES = {"00:C19": "H1"} R = Registry("00", "projective", LEDGER, PREDICATES, sources=[__file__]) def _hopf(p, nu): """The clauses of C19 on PGL₂(F_p), by search: the boosts fix no point, meet the Borel trivially, and the products (Borel class) × (boost class) are every class exactly once, p(p − 1) × (p + 1) = p(p² − 1); the factorization formula.""" G = pgl2(p) P1 = line(p) T = sorted({pclass(boost(nu, a, b, p), p) for a in range(p) for b in range(p) if (a or b)}) B = sorted({pclass(borel(a, b, 1, p), p) for a in range(1, p) for b in range(p)}) I = (1, 0, 0, 1) ok = len(G) == p * (p * p - 1) and len(T) == p + 1 and len(B) == p * (p - 1) 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 point ok &= set(T) & set(B) == {I} # (2) T ∩ B = 1 prods = [pclass(mul(b, t, p), p) for b in B for t in T] ok &= len(set(prods)) == len(G) and set(prods) == set(G) # (3), (4) a bijection for M in G: # the Lean proof's formula N, (a, b, e), (al, be) = factor(M, nu, p) 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) return ok def _spin(p, nu): """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₂.""" 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] Tsl = [boost(nu, a, b, p) for a in range(p) for b in range(p) if (a * a - nu * b * b) % p == 1] Bsl = [borel(a, b, pow(a, -1, p), p) for a in range(1, p) for b in range(p)] neg = lambda M: tuple((-v) % p for v in M) I = (1, 0, 0, 1); mI = neg(I) ok = len(SL) == p * (p * p - 1) and len(Tsl) == p + 1 and mI in Tsl and mI in Bsl ok &= set(Tsl) & set(Bsl) == {I, mI} psl = {min(M, neg(M)) for M in SL} img = {min(mul(b, t, p), neg(mul(b, t, p))) for b in Bsl for t in Tsl} ok &= len(psl) == p * (p * p - 1) // 2 and 2 * len(img) == len(psl) ok &= all(mul(neg(b), neg(t), p) == mul(b, t, p) for b in Bsl[:20] for t in Tsl) return ok, len(img), len(psl) # ------------------------------------------------------------------------------------------------------------ # block H: the Hopf section (00:C19) # the boost torus is fixed-point-free on ℙ¹ and meets the Borel trivially; every frame is uniquely (cone chart) × (boost), # p(p − 1) fibres of p + 1; on SL₂ the section obstructs at −1 (Projective.lean, hopf_section). @R.block("H", BLOCKS["H"]) def block_H(): """Block H — the Hopf section (EXACT): H1–H3.""" # 00:C19 (p00039) p = 13 nus = [arith.nonresidue(p), drive(p)] ok = all(_hopf(p, nu) for nu in nus) sp, img, psl = _spin(p, nus[0]) 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 " "boosts fix none of the 14 points; T ∩ B = 1; the 156 × 14 products (chart) × (boost) are every class exactly once; " "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 " "the products cover half of PSL₂", ok and sp, f"PSL₂: {img} of {psl} classes") # H2 the shells 5, 17, 29 exhaustive; the Subject 173 on random matrices bad = [q for q in (5, 17, 29) if not _hopf(q, arith.nonresidue(q))] q, nu = SAMPLE, arith.nonresidue(SAMPLE) rng = random.Random(173) for _ in range(3000): M = tuple(rng.randrange(q) for _ in range(4)) if det(M, q) == 0: continue N, (a, b, e), (al, be) = factor(M, nu, q) 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) 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 " "formula", not bad, f"exceptions {bad[:3]}") # H3 the spin cover at p = 5 and 17: half of PSL₂ out = [(q,) + _spin(q, arith.nonresidue(q)) for q in (5, 17)] 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)", all(o[1] for o in out), "; ".join(f"p={o[0]}: {o[2]} of {o[3]}" for o in out)) 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)