master.projective.py — py

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; C22 and C27 bound 20 October 2026).34Block C is bound by one file per theme whose key file proves its rows (subject.py, fourier.py, extension.py, frame.py and5this file). This file binds C19, the Hopf section of PGL₂(F_p); C22, the frame variety and its two fibrations (38-s13's6A7, A9, X4 reproduced through the theme, and PGL₂ ≅ SO₃ by the adjoint action); and C27, the frame group's one form7(SU₂(𝔽_{p²}/𝔽_p) = SL₂(𝔽_p), every element of finite order, the sphere and ad − bc = 1 one quadric through the8quarter-turn): the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs each key9conjoins (PROOFS), the shells, and the checks, which call the projective theme (frc/projective.py). The Lean side is10lean/FrcCore/Theme/Projective.lean and lean/FrcCore/Theme/Spin.lean, the key file lean/FrcCore/Keys/Projective.lean and11the certificate lean/FrcCore/Ledgers/Master/Projective.lean.1213    python3 -m frc.ledgers.master.projective        every block, the census; exit 1 if a check fails (≈ 25 s)1415Blocks:  H  the Hopf section of PGL₂                                                  EXACT  (00:C19)16         V  the frame variety: the counts, the spin cover, the triple, the two fibrations, SO₃   EXACT  (00:C22)17         U  the frame group has one form: SU₂ = SL₂, the census, the quadric identity   EXACT  (00:C27)1819The notebook frc/ledgers/master/projective.ipynb runs one row per cell, the cell's id its key (gate G13).20"""21import random22import sys2324from frc import arith25from frc.registry import Registry26from frc.foundation import drive27from frc.projective import mul, det, act, normal, pclass, line, boost, borel, pgl2, factor28from frc import projective as PJ2930# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----31BLOCK = "C"32KEYS = {"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 key33LEAN = {"C19": "core", "C22": "core", "C27": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them34# ---- end of the generated table ----3536PROOFS = {37    "C19": ["FRC.Shell.Frame.hopf_section", "FRC.Shell.Frame.hopf_counts"],38    "C22": ["FRC.Shell.Frame.frame_triple", "FRC.Shell.Frame.unit_split", "FRC.Shell.Frame.hopf_section", "FRC.Shell.Frame.hopf_counts",39            "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)40            "FRC.Spin.ad_preserves", "FRC.Spin.ad_kernel"],                                                   # PGL₂ → SO₃: orthogonal, injective41    "C27": ["FRC.Spin.hermitian_wJ", "FRC.Spin.su2_eq_sl2", "FRC.Spin.finite_order",42            "FRC.Shell.Frame.sphere_det", "FRC.Spin.sphere_bijective"],                                       # the quadric clause43}4445LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none4647SHELLS = [5, 13, 17, 29]        # exhaustive over PGL₂(F_p); the Subject 13 decides48SAMPLE = 173                    # the Subject 173: the factorization on random matrices4950LEDGER = {"H1": "00:C19", "H2": "00:C19", "H3": "00:C19", "V1": "00:C22", "V2": "00:C22", "V3": "00:C22", "U1": "00:C27", "U2": "00:C27"}51BLOCKS = {"H": "the Hopf section of PGL₂",52          "V": "the frame variety: the counts, the spin cover, the triple, the two fibrations, SO₃",53          "U": "the frame group has one form: SU₂ = SL₂, the census, the quadric identity"}54PREDICATES = {"00:C19": "H1", "00:C22": "V1", "00:C27": "U1"}5556R = Registry("00", "projective", LEDGER, PREDICATES, sources=[__file__])575859def _hopf(p, nu):60    """The clauses of C19 on PGL₂(F_p), by search: the boosts fix no point, meet the Borel trivially, and the products61    (Borel class) × (boost class) are every class exactly once, p(p − 1) × (p + 1) = p(p² − 1); the factorization formula."""62    G = pgl2(p)63    P1 = line(p)64    T = sorted({pclass(boost(nu, a, b, p), p) for a in range(p) for b in range(p) if (a or b)})65    B = sorted({pclass(borel(a, b, 1, p), p) for a in range(1, p) for b in range(p)})66    I = (1, 0, 0, 1)67    ok = len(G) == p * (p * p - 1) and len(T) == p + 1 and len(B) == p * (p - 1)68    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 point69    ok &= set(T) & set(B) == {I}                                                                    # (2) T ∩ B = 170    prods = [pclass(mul(b, t, p), p) for b in B for t in T]71    ok &= len(set(prods)) == len(G) and set(prods) == set(G)                                        # (3), (4) a bijection72    for M in G:                                                                                     # the Lean proof's formula73        N, (a, b, e), (al, be) = factor(M, nu, p)74        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)75    return ok767778def _spin(p, nu):79    """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₂."""80    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]81    Tsl = [boost(nu, a, b, p) for a in range(p) for b in range(p) if (a * a - nu * b * b) % p == 1]82    Bsl = [borel(a, b, pow(a, -1, p), p) for a in range(1, p) for b in range(p)]83    neg = lambda M: tuple((-v) % p for v in M)84    I = (1, 0, 0, 1); mI = neg(I)85    ok = len(SL) == p * (p * p - 1) and len(Tsl) == p + 1 and mI in Tsl and mI in Bsl86    ok &= set(Tsl) & set(Bsl) == {I, mI}87    psl = {min(M, neg(M)) for M in SL}88    img = {min(mul(b, t, p), neg(mul(b, t, p))) for b in Bsl for t in Tsl}89    ok &= len(psl) == p * (p * p - 1) // 2 and 2 * len(img) == len(psl)90    ok &= all(mul(neg(b), neg(t), p) == mul(b, t, p) for b in Bsl[:20] for t in Tsl)91    return ok, len(img), len(psl)929394# ------------------------------------------------------------------------------------------------------------95# block H: the Hopf section (00:C19)96# the boost torus is fixed-point-free on ℙ¹ and meets the Borel trivially; every frame is uniquely (cone chart) × (boost),97# p(p − 1) fibres of p + 1; on SL₂ the section obstructs at −1 (Projective.lean, hopf_section).98@R.block("H", BLOCKS["H"])99def block_H():100    """Block H — the Hopf section (EXACT): H1–H3."""101    # 00:C19 (p00039)102    p = 13103    nus = [arith.nonresidue(p), drive(p)]104    ok = all(_hopf(p, nu) for nu in nus)105    sp, img, psl = _spin(p, nus[0])106    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 "107            "boosts fix none of the 14 points; T ∩ B = 1; the 156 × 14 products (chart) × (boost) are every class exactly once; "108            "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 "109            "the products cover half of PSL₂", ok and sp, f"PSL₂: {img} of {psl} classes")110    # H2 the shells 5, 17, 29 exhaustive; the Subject 173 on random matrices111    bad = [q for q in (5, 17, 29) if not _hopf(q, arith.nonresidue(q))]112    q, nu = SAMPLE, arith.nonresidue(SAMPLE)113    rng = random.Random(173)114    for _ in range(3000):115        M = tuple(rng.randrange(q) for _ in range(4))116        if det(M, q) == 0: continue117        N, (a, b, e), (al, be) = factor(M, nu, q)118        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)119    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 "120            "formula", not bad, f"exceptions {bad[:3]}")121    # H3 the spin cover at p = 5 and 17: half of PSL₂122    out = [(q,) + _spin(q, arith.nonresidue(q)) for q in (5, 17)]123    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)",124            all(o[1] for o in out), "; ".join(f"p={o[0]}: {o[2]} of {o[3]}" for o in out))125126127# ------------------------------------------------------------------------------------------------------------128# block V: the frame variety and its two fibrations (00:C22)129# PGL₂(𝔽_p) ≅ SO₃(𝔽_p) by the adjoint action; the norm-one sphere is SL₂ (sphere_det, quat_bijective), the spin cover of PSL₂130# (one involution against p²); every element is one direction × one shell cell × one drive phase (frame_triple); the131# 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) without132# (unit_split, the Sylow count) — Projective.lean, Spin.lean; the corpus script check_c22.py reproduced record for record.133@R.block("V", BLOCKS["V"])134def block_V():135    """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."""136    # 00:C22 (p00152)137    p = 13; nu = arith.nonresidue(p); r = PJ.unit(p)[0]138    G, SL = pgl2(p), PJ.sl2(p)139    inv = PJ.involutions(p); sph = PJ.sphere_is_sl2(p, r); psl = PJ.psl2_image(p, r)140    counts = len(G) == len(SL) == p ** 3 - p == 2184 and psl == (1092, 2184) and inv == (1, 169)141    counts &= sph[0] and sph[3] and sph[1] == sph[2] == p ** 3 - p142    n, d, b, bij = PJ.frame_triple(p, nu); ns = PJ.nonsplit_fibration(p, nu); sp = PJ.split_fibration(p); cen = PJ.centraliser(p)143    triple = bij and n == (p + 1) * p * (p - 1) and d == p + 1 and b == p * (p - 1)144    fibr = ns["orbit_is_quadric"] and ns["base"] == p * (p - 1) and ns["fibres"] and ns["section"]145    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]146    fibr &= PJ.sphere(p, 1) == p * (p + 1) and PJ.sphere(p, nu) == p * (p - 1) and len(PJ.circle(p)) == p - 1147    syl, nU, gen, tin = PJ.no_section_split(p)148    sylow = syl == p + 1 and nU == p * (p - 1) and gen == p * (p * p - 1) // 2 > p * (p + 1) and tin149    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 "150            "x² + y² + z² + w² = 1 is SL₂ through the quarter-turn r² = −1 (the quaternion matrix's determinant is the norm, the sphere's "151            "matrices exactly those of determinant one) and its image in PGL₂ is PSL₂, index 2 — the spin cover, with one involution "152            "against PGL₂'s 169; every class is one direction × one Borel class ((p + 1)·p·(p − 1), the frame triple); the non-split "153            "orbit of u (u² = ν) is the quadric a² + bc = ν of 156 points with fibres C₁₄ and the Borel a section; the split orbit of "154            "the unit i is the quadric a² + bc = −1 of 182 points (the unit sphere's count), the fibres the cosets of the diagonal "155            "centraliser C₁₂ inside the Borel, and no section: the 14 Sylow 13-subgroups have normaliser of order 156 and generate "156            "PSL₂ of order 1 092 > 182, so no subgroup of order p(p + 1) exists",157            counts and triple and fibr and sylow,158            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}")159    # 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 control160    ok, det_ = True, []161    for q in (5, 17, 29):162        nq = arith.nonresidue(q); n, d, b, bij = PJ.frame_triple(q, nq); ns = PJ.nonsplit_fibration(q, nq); sp = PJ.split_fibration(q)163        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"]164        ok &= sp["orbit_is_quadric"] and sp["base"] == q * (q + 1) and sp["fibres_are_cosets"] and sp["borel_whole_or_none"]165        if q <= 17:166            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 tin167            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)168        det_.append(f"p={q}: {n} = {d}·{b}")169    for q in (7, 11):170        nq = arith.nonresidue(q); n, d, b, bij = PJ.frame_triple(q, nq); ns = PJ.nonsplit_fibration(q, nq)171        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"]172        det_.append(f"p={q} (≡ 3 mod 4): {n} = {d}·{b}, non-split base {ns['base']}")173    G3 = pgl2(3); PSL3 = {pclass(M, 3) for M in PJ.sl2(3)}174    closed = all(pclass(mul(A, B, 3), 3) in PSL3 for A in PSL3 for B in PSL3)175    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)}) == 1176    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 "177            "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 "178            "controls 7 and 11: the triple and the non-split fibration (the split one needs i² = −1); the p = 3 control: PSL₂(𝔽₃) = A₄, "179            "a subgroup of order 12 = p(p + 1) meeting the split torus trivially — a section, which is why the clause reads p = 4κ + 1",180            ok and control, "; ".join(det_))181    # V3 the adjoint action: PGL₂ ≅ SO₃182    out = {q: PJ.so3(q) for q in (5, 13, 17)}183    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())184    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 "185            "3 × 3 matrices (injective: the kernel is the centre, Spin.lean ad_kernel), each of determinant 1 and preserving the form "186            "a² + bc = −det X (ad_preserves); the orthogonal group of the form counts 2p(p² − 1) by orthonormal frames, so the image is "187            "its index-2 subgroup SO₃", ok, "; ".join(f"p={q}: |Ad| = {v[0]}, |O₃| = {v[4]}" for q, v in out.items()))188189190# ------------------------------------------------------------------------------------------------------------191# block U: the frame group has one form (00:C27)192# SU₂(𝔽_{p²}/𝔽_p) = SL₂(𝔽_p) for the Hermitian form wJ, w^p = −w (Spin.lean su2_eq_sl2, hermitian_wJ); every element of finite order193# (finite_order); the sphere and ad − bc = 1 one quadric through the quarter-turn (sphere_det, quat_bijective) — the corpus194# script check_c23.py reproduced record for record.195@R.block("U", BLOCKS["U"])196def block_U():197    """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."""198    # 00:C27 (p00183)199    h5 = PJ.hermitian_wJ(5, arith.nonresidue(5))[1]; h13 = PJ.hermitian_wJ(13, arith.nonresidue(13))[1]200    full = PJ.su2_is_sl2(5, arith.nonresidue(5), full=True)201    sam = PJ.su2_is_sl2(13, arith.nonresidue(13))202    su = all(PJ.su2_identity_count(q, arith.nonresidue(q)) == q ** 3 - q for q in (5, 13))203    Q5, shape5, n5 = PJ.hermitian_congruence(5, arith.nonresidue(5))204    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 == 120205    cen = {q: PJ.element_census(q) for q in (5, 13)}206    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"])207                 and all((q + 1) % k == 0 for k in o["nonsplit"]) for q, (c, e, o, inv) in cen.items())208    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 "209            "(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 — "210            "SU₂(𝔽₂₅/𝔽₅) = SL₂(𝔽₅) on the nose; at p = 13 none of 400 random non-rational elements of SL₂(𝔽₁₆₉) is unitary (the general "211            "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 "212            "conjugates SL₂(𝔽₅) onto the quaternion shape [[a, b], [−b̄, ā]], 120 elements: the two Hermitian forms are one form; the "213            "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 — "214            "with the orders p, 2p, dividing p − 1, dividing p + 1 on the sampled elements, every element of finite order, and "215            "exactly one involution, −I",216            unit and census,217            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())}")218    # U2 the quadric identity at p = 5, 13, 17 and the controls 7, 11219    ok, det_ = True, []220    for q in (5, 13, 17):221        nq = arith.nonresidue(q); s4, s31, h3, s22, fr, ci, hy = PJ.quadric_counts(q, nq); rq = PJ.unit(q)[0]222        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]223        det_.append(f"p={q}: {s4}")224    for q in (7, 11):225        nq = arith.nonresidue(q); s4, s31, h3, s22, fr, ci, hy = PJ.quadric_counts(q, nq)226        ok &= s4 == s22 == fr == q ** 3 - q and s31 == h3 == q ** 3 + q and ci == q + 1 and hy == q + 1227        det_.append(f"p={q} (≡ 3 mod 4): (4,0) {s4}, (3,1) {s31}")228    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 "229            "frame quadric ad − bc = 1 all have p³ − p points and the sphere's matrices through the quarter-turn are exactly SL₂; the "230            "circle x² + y² = 1 has p − 1 points (the split torus), the hyperbola x² − νy² = 1 has p + 1 (the non-split); at the "231            "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 "232            "quadric stays", ok, "; ".join(det_))233234235if __name__ == "__main__":236    blocks = [a for a in sys.argv[1:] if a in R.blocks]237    if blocks:238        for b in blocks: R.run_block(b)239        sys.exit(0 if R.summary(write=False) else 1)240    sys.exit(0 if R.verify_all() else 1)241