"""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; C22 and C27 bound 20 October 2026). Block C is bound by one file per theme whose key file proves its rows (subject.py, fourier.py, extension.py, frame.py and this file). This file binds C19, the Hopf section of PGL₂(F_p); C22, the frame variety and its two fibrations (38-s13's A7, A9, X4 reproduced through the theme, and PGL₂ ≅ SO₃ by the adjoint action); and C27, the frame group's one form (SU₂(𝔽_{p²}/𝔽_p) = SL₂(𝔽_p), every element of finite order, the sphere and ad − bc = 1 one quadric through the quarter-turn): 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 projective theme (frc/projective.py). The Lean side is lean/FrcCore/Theme/Projective.lean and lean/FrcCore/Theme/Spin.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 (≈ 25 s) Blocks: H the Hopf section of PGL₂ EXACT (00:C19) V the frame variety: the counts, the spin cover, the triple, the two fibrations, SO₃ EXACT (00:C22) U the frame group has one form: SU₂ = SL₂, the census, the quadric identity EXACT (00:C27) 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 from frc import projective as PJ # ---- 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", "C22": "core", "C27": "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"], "C22": ["FRC.Shell.Frame.frame_triple", "FRC.Shell.Frame.unit_split", "FRC.Shell.Frame.hopf_section", "FRC.Shell.Frame.hopf_counts", "FRC.Shell.Frame.sphere_det", "FRC.Spin.sphere_bijective", "FRC.Shell.Frame.frame_counts", # 38:A7, A9, X4's theorems (the bijection in the projective theme's statement) "FRC.Spin.ad_preserves", "FRC.Spin.ad_kernel"], # PGL₂ → SO₃: orthogonal, injective "C27": ["FRC.Spin.hermitian_wJ", "FRC.Spin.su2_eq_sl2", "FRC.Spin.finite_order", "FRC.Shell.Frame.sphere_det", "FRC.Spin.sphere_bijective"], # the quadric clause } 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", "V1": "00:C22", "V2": "00:C22", "V3": "00:C22", "U1": "00:C27", "U2": "00:C27"} BLOCKS = {"H": "the Hopf section of PGL₂", "V": "the frame variety: the counts, the spin cover, the triple, the two fibrations, SO₃", "U": "the frame group has one form: SU₂ = SL₂, the census, the quadric identity"} PREDICATES = {"00:C19": "H1", "00:C22": "V1", "00:C27": "U1"} 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)) # ------------------------------------------------------------------------------------------------------------ # block V: the frame variety and its two fibrations (00:C22) # PGL₂(𝔽_p) ≅ SO₃(𝔽_p) by the adjoint action; the norm-one sphere is SL₂ (sphere_det, quat_bijective), the spin cover of PSL₂ # (one involution against p²); every element is one direction × one shell cell × one drive phase (frame_triple); the # non-split fibration C_{p+1} over p(p − 1) with the Borel a section (hopf_section), the split C_{p−1} over p(p + 1) without # (unit_split, the Sylow count) — Projective.lean, Spin.lean; the corpus script check_c22.py reproduced record for record. @R.block("V", BLOCKS["V"]) def block_V(): """Block V — the frame variety (EXACT): V1 the counts, the sphere and the two fibrations on the Subject 13; V2 the shells 5, 17, 29 and the controls; V3 the adjoint action.""" # 00:C22 (p00152) p = 13; nu = arith.nonresidue(p); r = PJ.unit(p)[0] G, SL = pgl2(p), PJ.sl2(p) inv = PJ.involutions(p); sph = PJ.sphere_is_sl2(p, r); psl = PJ.psl2_image(p, r) counts = len(G) == len(SL) == p ** 3 - p == 2184 and psl == (1092, 2184) and inv == (1, 169) counts &= sph[0] and sph[3] and sph[1] == sph[2] == p ** 3 - p n, d, b, bij = PJ.frame_triple(p, nu); ns = PJ.nonsplit_fibration(p, nu); sp = PJ.split_fibration(p); cen = PJ.centraliser(p) triple = bij and n == (p + 1) * p * (p - 1) and d == p + 1 and b == p * (p - 1) fibr = ns["orbit_is_quadric"] and ns["base"] == p * (p - 1) and ns["fibres"] and ns["section"] fibr &= sp["orbit_is_quadric"] and sp["base"] == p * (p + 1) and sp["fibres_are_cosets"] and sp["borel_whole_or_none"] and cen[1] == p - 1 and cen[2] fibr &= PJ.sphere(p, 1) == p * (p + 1) and PJ.sphere(p, nu) == p * (p - 1) and len(PJ.circle(p)) == p - 1 syl, nU, gen, tin = PJ.no_section_split(p) sylow = syl == p + 1 and nU == p * (p - 1) and gen == p * (p * p - 1) // 2 > p * (p + 1) and tin R.check("V1", "the Subject p = 13, by search: PGL₂ and SL₂ both of 2 184 = 14·13·12 elements, PSL₂ the half 1 092; the norm-one sphere " "x² + y² + z² + w² = 1 is SL₂ through the quarter-turn r² = −1 (the quaternion matrix's determinant is the norm, the sphere's " "matrices exactly those of determinant one) and its image in PGL₂ is PSL₂, index 2 — the spin cover, with one involution " "against PGL₂'s 169; every class is one direction × one Borel class ((p + 1)·p·(p − 1), the frame triple); the non-split " "orbit of u (u² = ν) is the quadric a² + bc = ν of 156 points with fibres C₁₄ and the Borel a section; the split orbit of " "the unit i is the quadric a² + bc = −1 of 182 points (the unit sphere's count), the fibres the cosets of the diagonal " "centraliser C₁₂ inside the Borel, and no section: the 14 Sylow 13-subgroups have normaliser of order 156 and generate " "PSL₂ of order 1 092 > 182, so no subgroup of order p(p + 1) exists", counts and triple and fibr and sylow, f"|PGL₂| = {len(G)}, PSL₂ {psl[0]}, involutions {inv}; triple {n} = {d}·{b}; bases {ns['base']}, {sp['base']}; Sylow {syl}, |N(U)| = {nU}, ⟨U⟩ = {gen}") # V2 the shells 5, 17, 29 by search, the odd-p controls 7 and 11 (the non-split fibration alone: the split one needs i² = −1), the p = 3 control ok, det_ = True, [] for q in (5, 17, 29): nq = arith.nonresidue(q); n, d, b, bij = PJ.frame_triple(q, nq); ns = PJ.nonsplit_fibration(q, nq); sp = PJ.split_fibration(q) ok &= bij and n == (q + 1) * q * (q - 1) and ns["orbit_is_quadric"] and ns["base"] == q * (q - 1) and ns["fibres"] and ns["section"] ok &= sp["orbit_is_quadric"] and sp["base"] == q * (q + 1) and sp["fibres_are_cosets"] and sp["borel_whole_or_none"] if q <= 17: syl, nU, gen, tin = PJ.no_section_split(q); ok &= syl == q + 1 and nU == q * (q - 1) and gen == q * (q * q - 1) // 2 > q * (q + 1) and tin rq = PJ.unit(q)[0]; sph = PJ.sphere_is_sl2(q, rq); ok &= sph[0] and sph[3] and PJ.involutions(q) == (1, q * q) det_.append(f"p={q}: {n} = {d}·{b}") for q in (7, 11): nq = arith.nonresidue(q); n, d, b, bij = PJ.frame_triple(q, nq); ns = PJ.nonsplit_fibration(q, nq) ok &= bij and n == (q + 1) * q * (q - 1) and ns["orbit_is_quadric"] and ns["base"] == q * (q - 1) and ns["fibres"] and ns["section"] det_.append(f"p={q} (≡ 3 mod 4): {n} = {d}·{b}, non-split base {ns['base']}") G3 = pgl2(3); PSL3 = {pclass(M, 3) for M in PJ.sl2(3)} closed = all(pclass(mul(A, B, 3), 3) in PSL3 for A in PSL3 for B in PSL3) control = len(G3) == 24 and len(PSL3) == 12 == 3 * (3 + 1) and closed and len(PSL3 & {pclass((a, 0, 0, 1), 3) for a in (1, 2)}) == 1 R.check("V2", "the shells 5, 17, 29 by search: the frame triple, both fibrations with their fibres, the Borel a section of the non-split " "one and of the split one none (the Sylow count at 5 and 17), the sphere SL₂ with one involution against p²; the odd-p " "controls 7 and 11: the triple and the non-split fibration (the split one needs i² = −1); the p = 3 control: PSL₂(𝔽₃) = A₄, " "a subgroup of order 12 = p(p + 1) meeting the split torus trivially — a section, which is why the clause reads p = 4κ + 1", ok and control, "; ".join(det_)) # V3 the adjoint action: PGL₂ ≅ SO₃ out = {q: PJ.so3(q) for q in (5, 13, 17)} ok = all(v[0] == v[1] == q * (q * q - 1) and v[2] == {1} and v[3] and v[4] == 2 * q * (q * q - 1) for q, v in out.items()) R.check("V3", "PGL₂(𝔽_p) ≅ SO₃(𝔽_p) at p = 5, 13, 17: the adjoint action X ↦ M X M⁻¹ on the trace-zero matrices gives p(p² − 1) distinct " "3 × 3 matrices (injective: the kernel is the centre, Spin.lean ad_kernel), each of determinant 1 and preserving the form " "a² + bc = −det X (ad_preserves); the orthogonal group of the form counts 2p(p² − 1) by orthonormal frames, so the image is " "its index-2 subgroup SO₃", ok, "; ".join(f"p={q}: |Ad| = {v[0]}, |O₃| = {v[4]}" for q, v in out.items())) # ------------------------------------------------------------------------------------------------------------ # block U: the frame group has one form (00:C27) # SU₂(𝔽_{p²}/𝔽_p) = SL₂(𝔽_p) for the Hermitian form wJ, w^p = −w (Spin.lean su2_eq_sl2, hermitian_wJ); every element of finite order # (finite_order); the sphere and ad − bc = 1 one quadric through the quarter-turn (sphere_det, quat_bijective) — the corpus # script check_c23.py reproduced record for record. @R.block("U", BLOCKS["U"]) def block_U(): """Block U — the frame group has one form (EXACT): U1 the unitary form and the census on 5 and 13; U2 the quadric identity on the shells.""" # 00:C27 (p00183) h5 = PJ.hermitian_wJ(5, arith.nonresidue(5))[1]; h13 = PJ.hermitian_wJ(13, arith.nonresidue(13))[1] full = PJ.su2_is_sl2(5, arith.nonresidue(5), full=True) sam = PJ.su2_is_sl2(13, arith.nonresidue(13)) su = all(PJ.su2_identity_count(q, arith.nonresidue(q)) == q ** 3 - q for q in (5, 13)) Q5, shape5, n5 = PJ.hermitian_congruence(5, arith.nonresidue(5)) unit = h5 and h13 and full == (True, 120, 15600, 120) and sam[0] and sam[1] == 2184 and sam[3] == 0 and su and Q5 is not None and shape5 and n5 == 120 cen = {q: PJ.element_census(q) for q in (5, 13)} census = all(c == e and inv == 1 and o["unip+"] == {q} and o["unip-"] == {2 * q} and all((q - 1) % k == 0 for k in o["split"]) and all((q + 1) % k == 0 for k in o["nonsplit"]) for q, (c, e, o, inv) in cen.items()) R.check("U1", "the unitary form: wJ is Hermitian ((wJ)† = wJ, since w^p = −w) at p = 5 and 13; every element of SL₂(𝔽_p) is wJ-unitary " "(120 at p = 5, 2 184 at p = 13); at p = 5, of SL₂(𝔽₂₅)'s 15 600 elements exactly the 120 rational ones are unitary — " "SU₂(𝔽₂₅/𝔽₅) = SL₂(𝔽₅) on the nose; at p = 13 none of 400 random non-rational elements of SL₂(𝔽₁₆₉) is unitary (the general " "converse is Spin.lean's su2_eq_sl2); |SU₂(I)| = #{N(a) + N(b) = 1} = p³ − p and an invertible Q with Qᵀ conj(Q) = wJ " "conjugates SL₂(𝔽₅) onto the quaternion shape [[a, b], [−b̄, ā]], 120 elements: the two Hermitian forms are one form; the " "census of SL₂ at 5 and 13 — I, −I, p² − 1 unipotents of each sign, (p − 3)p(p + 1)/2 split, (p − 1)²p/2 non-split — " "with the orders p, 2p, dividing p − 1, dividing p + 1 on the sampled elements, every element of finite order, and " "exactly one involution, −I", unit and census, f"SL₂(𝔽₂₅): {full[2]}, unitary {full[3]}; Q = {Q5}; census at 13: {tuple(cen[13][0].values())}, orders {dict((k, sorted(v)) for k, v in cen[13][2].items())}") # U2 the quadric identity at p = 5, 13, 17 and the controls 7, 11 ok, det_ = True, [] for q in (5, 13, 17): nq = arith.nonresidue(q); s4, s31, h3, s22, fr, ci, hy = PJ.quadric_counts(q, nq); rq = PJ.unit(q)[0] ok &= s4 == s31 == h3 == s22 == fr == q ** 3 - q and ci == q - 1 and hy == q + 1 and PJ.sphere_is_sl2(q, rq)[3] det_.append(f"p={q}: {s4}") for q in (7, 11): nq = arith.nonresidue(q); s4, s31, h3, s22, fr, ci, hy = PJ.quadric_counts(q, nq) ok &= s4 == s22 == fr == q ** 3 - q and s31 == h3 == q ** 3 + q and ci == q + 1 and hy == q + 1 det_.append(f"p={q} (≡ 3 mod 4): (4,0) {s4}, (3,1) {s31}") R.check("U2", "the quadric identity: at p = 5, 13, 17 the sphere x² + y² + z² + w² = 1, the (3, 1) forms = ±1, the (2, 2) form and the " "frame quadric ad − bc = 1 all have p³ − p points and the sphere's matrices through the quarter-turn are exactly SL₂; the " "circle x² + y² = 1 has p − 1 points (the split torus), the hyperbola x² − νy² = 1 has p + 1 (the non-split); at the " "controls 7 and 11 the (3, 1) forms move to p³ + p and the circle to p + 1 — the signature labels follow η(−1), the frame " "quadric stays", ok, "; ".join(det_)) 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)