The ledger file frc/ledgers/master/foundation.py of the master's block of the foundation theme, rendered with an anchor per line: the marked lines (# 00:B5 (p00015): a row and its accession key) are the checks that decide the rows; the rows' theorems are the keys of Keys.Foundation. ▶ run the rows on Google Colab.
1"""master/foundation — the ledger file of the master's block A, the Foundation (ledger migration, task LM23, 5 October 2026).23The master predicate ledger (00-ledger/predicates/index.md, published as docs/00-ledger.json) states block A. This file4binds its theorem rows to the framework: the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py),5the Lean proofs each key conjoins (PROOFS, written here), the shells, and the checks, which call the foundation theme6(frc/foundation.py). Each check names the rows it decides or corroborates (LEDGER), under a `# 00:A5 (p00188)` marker on7the check that decides the row (PREDICATES).89The rows are A2, A3 and A4 (the three former pillars, theorems since 9 October 2026: the registered Universe of any10totality is finite and no reading registers an unlimited supply, with the agent's bound; the registration of any11totality is onto its registered Universe, and two totalities each registered whole within the other have one count;12the incompleteness of observation — every reading of a part identifies two members, complete only at the whole count,13and no frame sees more, the Carrier a translation torsor; until 9 October two rows, the bounded observer A4 and14Registration A5, merged that day; retitled with A3, Completeness of the totality, on 13 October), A5,15A10, A11 and A12, the block's T rows, proved in16lean/FrcCore/Theme/Foundation.lean and lean/FrcCore/Theme/Drive.lean with no generator assumed. A9, the trusted base, is17a D row: gate G19 enforces its clause on unboundedness, and every key's empty axiom list (gate G08) its kernel clause.18The checks run on the three Carriers of the Carrier's block file, Ω = 233, 30 089 and 2 408 561, with their Subjects1913, 173 and 1 373, and as sweeps over every modulus or prime below a bound. The Lean side is the key file20lean/FrcCore/Keys/Foundation.lean and the certificate lean/FrcCore/Ledgers/Master/Foundation.lean.2122 python3 -m frc.ledgers.master.foundation every block, the census; exit 1 if a check fails (≈ 15 s)23 python3 -m frc.ledgers.master.foundation M one block (F, V, U, W, Q, I, H or M)24 from frc.ledgers.master.foundation import R; R.predicate("00:A12") one row: its blocks run once per session2526Blocks: F the registered Universe is finite; the agent's bound EXACT (00:A2)27 V the registration is onto; mutual registration is one count EXACT (00:A3)28 U every reading of a proper part identifies two members EXACT (00:A4)29 W a complete reading needs the whole; the torsor EXACT (00:A4)30 Q counting closes by return EXACT (00:A5)31 I completeness is primality EXACT (00:A10)32 H the quarter-turn exists iff p ≡ 1 (mod 4) EXACT (00:A11)33 M every prime carries a frame EXACT (00:A12)3435The notebook frc/ledgers/master/foundation.ipynb runs one row per cell, the cell's id its key (gate G13).36"""37import itertools38import sys3940from frc import arith41from frc.registry import Registry42from frc.foundation import (half_power, quarter_turn, quarter_turns, successor_orbit, principal_ideal, is_complete,43 zero_divisors, element_order, drive, collision)44from frc.formation import records4546# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----47BLOCK = "A"48KEYS = {"A1": "p00001", "A2": "p00004", "A3": "p00003", "A4": "p00197", "A5": "p00188", "A6": "p00008", "A7": "p00009", "A8": "p00010", "A9": "p00161", "A10": "p00162", "A11": "p00163", "A12": "p00164", "A13": "p00196"} # every row of the block: its label and its accession key49LEAN = {"A2": "core", "A3": "core", "A4": "core", "A5": "core", "A10": "core", "A11": "core", "A12": "core"} # the rows with a Lean declaration: the libraries whose key files prove them50# ---- end of the generated table ----5152# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys53# 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.54PROOFS = {55 "A2": ["FRC.Foundation.registered_finite", "FRC.Foundation.no_unlimited_supply", "FRC.Foundation.agent_bound"],56 "A3": ["FRC.Foundation.registration_onto", "FRC.Foundation.mutual_registration_count"],57 "A4": ["FRC.Foundation.observer_part", "FRC.Foundation.complete_needs_whole", "FRC.Foundation.translation_torsor"],58 "A5": ["FRC.Foundation.successor_cycle"],59 "A10": ["FRC.Shell.Prime.isPrime_iff_complete"],60 "A11": ["FRC.Shell.Prime.quarter_turn_iff"],61 "A12": ["FRC.Shell.Prime.exists_drive"],62}6364LEAN_ONLY = () # the rows with a Lean declaration and no python check (gate G12): none6566# The Carriers (Ω, the Subject p), as in the Carrier's block file: Ω = 4S + 1 prime, p prime with p² < Ω.67SHELLS = [(233, 13), (30089, 173), (2408561, 1373)]68SWEEP = 5000 # the sweeps over primes run below it69SMALL = 6 # the exhaustive readings run over every total of at most SMALL points7071# The rows each check decides or corroborates.72LEDGER = {73 "F1": "00:A2", "F2": "00:A2", "F3": "00:A2", "F4": "00:A2",74 "V1": "00:A3", "V2": "00:A3", "V3": "00:A3",75 "U1": "00:A4", "U2": "00:A4", "U3": "00:A4",76 "W1": "00:A4", "W2": "00:A4",77 "Q1": "00:A5", "Q2": "00:A5",78 "I1": "00:A10", "I2": "00:A10",79 "H1": "00:A11", "H2": "00:A11",80 "M1": "00:A12", "M2": "00:A12", "M3": "00:A12",81}8283BLOCKS = {"F": "the registered Universe of any totality is finite; no reading registers an unlimited supply; the agent's bound",84 "V": "the registration is onto its registered Universe; mutual registration is one count",85 "U": "every reading of a proper part identifies two members (a bounded observer is a proper part)",86 "W": "a complete reading needs the whole count; the Carrier is a translation torsor", "Q": "counting closes by return", "I": "completeness is primality",87 "H": "the quarter-turn exists iff p ≡ 1 (mod 4)", "M": "every prime carries a frame"}8889# the deciding check of each row; the sweeps corroborate90PREDICATES = {"00:A2": "F1", "00:A3": "V3", "00:A4": "U1", "00:A5": "Q1", "00:A10": "I2", "00:A11": "H1", "00:A12": "M1"}9192R = Registry("00", "foundation", LEDGER, PREDICATES, sources=[__file__])9394for _Om, _p in SHELLS:95 assert arith.is_prime(_Om) and _Om % 4 == 1 and arith.is_prime(_p) and _p * _p < _Om, (_Om, _p)969798def _primes(lo, hi):99 return [n for n in range(lo, hi) if arith.is_prime(n)]100101102# ------------------------------------------------------------------------------------------------------------103# block F: the registered Universe is finite (00:A2)104# what a reading of capacity R registers of any totality — its residues — has at most R members, whatever the totality105# (Foundation.lean, registered_finite: the registered Universe embeds in the shell of R points); among any R + 1 members106# two share a residue (no_unlimited_supply); an agent of capacity K over s symbols has records(s, K) < s^(K+1) records,107# so a shell read whole into them has at most that many members (agent_bound, 5:C2).108def _injective(rho, n):109 return collision(rho, n) is None110111112def _registered(rho, members):113 """The registered Universe of the members under the reading rho: the set of residues (Foundation.lean, Registered)."""114 return sorted({rho(u) for u in members})115116117@R.block("F", BLOCKS["F"])118def block_F():119 """Block F — the registered Universe is finite; the agent's bound (EXACT): F1–F4."""120 # 00:A2 (p00004)121 bad, det = [], []122 totalities = {"[0, 10^5)": range(10 ** 5), "the odd naturals below 2·10^5": range(1, 2 * 10 ** 5, 2),123 "the squares below 10^10": (k * k for k in range(10 ** 5))}124 for name, members in totalities.items():125 members = list(members)126 for R_ in (1, 2, 7, 13, 233):127 readings = {"u mod R": lambda u, R_=R_: u % R_, "u mod R, squared": lambda u, R_=R_: (u * u) % R_,128 "min(u, R−1)": lambda u, R_=R_: min(u, R_ - 1)}129 for rname, rho in readings.items():130 reg = _registered(rho, members)131 emb = [r % R_ for r in reg] # the embedding into the shell of R points, by ofNat132 if not (len(reg) <= R_ and all(0 <= r < R_ for r in reg) and len(set(emb)) == len(reg)): bad.append((name, R_, rname, len(reg)))133 # among any R + 1 members two share a residue: the first R + 1 members, and R + 1 members spread out134 for sample in (members[:R_ + 1], members[::max(1, len(members) // (R_ + 1))][:R_ + 1]):135 if len(sample) == R_ + 1 and _injective(lambda i, s=sample, rho=rho: rho(s[i]), R_ + 1): bad.append((name, R_, rname, "no collision"))136 det.append(f"{name}: under every reading into R ∈ {{1, 2, 7, 13, 233}} records the residues number ≤ R and embed in the shell of R points")137 R.check("F1", "three totalities of 10^5 members, three readings each into R ∈ {1, 2, 7, 13, 233} records: the registered Universe (the "138 "residues) has at most R members and embeds in the shell of R points; among any R + 1 members two share a residue",139 not bad, "; ".join(det) + f"; exceptions {bad[:3]}")140 # F2 the same on the three Carriers as totalities read by their Subjects' capacities, and on an unbounded totality: the141 # naturals read into R records have exactly R residues, found below R, and every R + 1 of them collide142 bad, det = [], []143 for Om, p in SHELLS:144 reg = _registered(lambda u: u % p, range(Om))145 c = collision(lambda i: i % p, p + 1)146 if not (len(reg) == p and c is not None): bad.append((Om, p))147 det.append(f"Ω={Om} read into p={p} records: {len(reg)} residues; {c} collide among the first p + 1")148 for R_ in (3, 10, 1000):149 reg = _registered(lambda u: u % R_, range(10 * R_))150 if not (len(reg) == R_ and max(reg) == R_ - 1): bad.append(("naturals", R_))151 R.check("F2", "the three Carriers read into their Subjects' p records: exactly p residues, a collision among the first p + 1 "152 "members; the naturals read into R ∈ {3, 10, 1000} records: R residues, all below R", not bad, "; ".join(det))153 # F3 the agent's bound154 bad, det = [], []155 for s in (2, 3):156 for K in range(0, 3):157 rc = records(s, K)158 if not (rc == sum(s ** l for l in range(K + 1)) and rc < s ** (K + 1)): bad.append((s, K, rc))159 for n in range(1, min(rc, SMALL) + 3): # every reading of n members into rc records160 whole = any(_injective(lambda u: rho[u], n) for rho in itertools.product(range(rc), repeat=n))161 if whole != (n <= rc): bad.append((s, K, n))162 det.append(f"s={s}, K={K}: records {rc} < {s ** (K + 1)}; read whole iff n ≤ {rc}")163 R.check("F3", f"s ∈ {{2, 3}}, K ≤ 2: records(s, K) = Σ_{{l≤K}} s^l < s^(K+1), and a shell of n members is read whole (an injective "164 "reading, exhaustive over the readings) into records(s, K) records iff n ≤ records(s, K): the agent's bound",165 not bad, "; ".join(det[:3]) + f"; exceptions {bad}")166 # F4 the count bound alone, wider: records(s, K) < s^(K+1) for s ≤ 7 and K ≤ 12, and on the three Carriers an agent of167 # capacity K with records(2, K) < Ω reads the Carrier incompletely (a collision found by search)168 bad, det = [], []169 for s in range(2, 8):170 for K in range(0, 13):171 if not records(s, K) < s ** (K + 1): bad.append((s, K))172 for Om, p in SHELLS:173 K = max(k for k in range(60) if records(2, k) < Om)174 rc = records(2, K)175 c = collision(lambda x: x % rc, Om)176 if c is None or c[0] == c[1] or (c[0] % rc) != (c[1] % rc): bad.append((Om, K))177 det.append(f"Ω={Om}: K={K}, records(2, K)={rc} < Ω, x mod records identifies {c}")178 R.check("F4", "s ≤ 7, K ≤ 12: records(s, K) < s^(K+1); on the three Carriers, the largest K with records(2, K) < Ω: a reading "179 "into those records identifies two members (by search)", not bad, "; ".join(det))180# ------------------------------------------------------------------------------------------------------------181# block V: mutual registration is one count (00:A3)182# injections both ways between shells force equal counts (the pigeonhole both ways; Foundation.lean,183# mutual_registration_count); a larger shell registers a smaller, so the theorem is silent on a host.184@R.block("V", BLOCKS["V"])185def block_V():186 """Block V — the registration is onto; mutual registration is one count (EXACT): V1–V3."""187 # 00:A3 (p00003)188 bad = []189 for m in range(1, SMALL + 1):190 for n in range(1, SMALL + 1):191 inj_mn = any(_injective(lambda x: f[x], m) for f in itertools.product(range(n), repeat=m))192 inj_nm = any(_injective(lambda x: g[x], n) for g in itertools.product(range(m), repeat=n))193 if (inj_mn and inj_nm) != (m == n) or inj_mn != (m <= n): bad.append((m, n))194 R.check("V1", f"every m, n ≤ {SMALL}: an injective reading of m members into n exists iff m ≤ n (exhaustive), so injections both "195 "ways exist iff m = n: two totalities each registered whole within the other have one count", not bad, f"exceptions {bad}")196 # V2 on the three Carriers: the Subject's p members are registered injectively in the Carrier (the identity), the Carrier's197 # Ω are not registered injectively in p states (a collision found by search): the larger shell hosts the smaller198 ok, det = True, []199 for Om, p in SHELLS:200 c = collision(lambda x: x % p, Om)201 ok &= _injective(lambda x: x, p) and c is not None and (c[0] % p) == (c[1] % p) and c[0] != c[1]202 det.append(f"Ω={Om}, p={p}: x ↦ x identifies no two of the p; x mod p identifies {c} of the Ω")203 R.check("V2", "on the three Carriers: the Subject is registered injectively within the Carrier and the Carrier is not within "204 "the Subject (collision by search): a larger shell registers a smaller, the theorem silent on a host", ok, "; ".join(det))205 # V3 the registration is onto: every residue of the registered Universe is some member's, and every member has its residue —206 # on the three Carriers read into p records and on the naturals read into R records207 bad, det = [], []208 for Om, p in SHELLS:209 reg = _registered(lambda u: u % p, range(Om))210 preimages = {r: next(u for u in range(Om) if u % p == r) for r in reg}211 if not (all(preimages[r] % p == r for r in reg) and all((u % p) in set(reg) for u in range(0, Om, max(1, Om // 1000)))): bad.append(Om)212 det.append(f"Ω={Om}, p={p}: each of the {len(reg)} residues is a member's, each sampled member's residue is registered")213 for R_ in (3, 10, 1000):214 reg = _registered(lambda u: u % R_, range(10 * R_))215 if not all(any(u % R_ == r for u in range(10 * R_)) for r in reg): bad.append(("naturals", R_))216 R.check("V3", "the registration is onto its registered Universe: on the three Carriers read into p records and on the naturals "217 "read into R ∈ {3, 10, 1000} records, every registered residue is a member's and every member's residue is registered",218 not bad, "; ".join(det))219220221# ------------------------------------------------------------------------------------------------------------222# block U: every reading of a proper part identifies two members — a bounded observer is a proper part (00:A4)223# an observer with o < Ω states holds no injective encoding of the Ω points: every reading identifies two distinct points224# (Foundation.lean, observer_part; the pigeonhole). The row's other clauses are block W.225@R.block("U", BLOCKS["U"])226def block_U():227 """Block U — a bounded observer is a proper part (EXACT): U1–U3."""228 # 00:A4 (p00197)229 total, bad = 0, []230 for n in range(1, SMALL + 1):231 for o in range(n):232 for rho in itertools.product(range(o), repeat=n):233 total += 1234 if collision(lambda x: rho[x], n) is None: bad.append((n, o, rho))235 R.check("U1", f"every total of n ≤ {SMALL} points and every observer of o < n states: each of the o^n readings identifies two "236 "distinct points (exhaustive)", not bad, f"{total} readings; injective ones {bad[:3]}")237 # U2 the bound is sharp: o = n states admit an injective reading238 ok = all(collision(lambda x: x, n) is None for n in range(1, SMALL + 1)) and all(239 all(collision(lambda x: rho[x], n) is None for rho in itertools.permutations(range(n))) for n in range(1, SMALL + 1))240 R.check("U2", f"the bound is sharp: for every n ≤ {SMALL}, an observer of n states reads the n points injectively (each of the n! "241 "bijections, the identity among them)", ok, "o < n forces a collision, o = n does not")242 # U3 on the three Carriers, an observer of Ω − 1 states: three readings, each with two distinct points found by search243 ok, det = True, []244 for Om, p in SHELLS:245 o = Om - 1246 readings = {"x mod (Ω−1)": lambda x: x % o, "min(x, Ω−2)": lambda x: min(x, o - 1),247 "p x mod (Ω−1)": lambda x: p * x % o}248 for name, rho in readings.items():249 c = collision(rho, Om)250 ok &= c is not None and c[0] != c[1] and rho(c[0]) == rho(c[1]) and all(0 <= rho(x) < o for x in (c[0], c[1]))251 det.append(f"Ω={Om}: x mod (Ω−1) identifies {collision(readings['x mod (Ω−1)'], Om)}")252 R.check("U3", "on the three Carriers, an observer of Ω − 1 states: the readings x mod (Ω−1), min(x, Ω−2) and p·x mod (Ω−1) each "253 "identify two distinct points, found by search", ok, "; ".join(det))254255256# ------------------------------------------------------------------------------------------------------------257# block W: a complete reading needs the whole count; the Carrier is a translation torsor (00:A4, with block U)258# a reading of the Ω members into o records that identifies no two has Ω ≤ o (the contrapositive of observer_part);259# exactly one translation carries each member to each (Foundation.lean, complete_needs_whole, translation_torsor).260@R.block("W", BLOCKS["W"])261def block_W():262 """Block W — a complete reading needs the whole count; the translation torsor (EXACT): W1, W2."""263 # the row's second and third clauses (the marker of 00:A4 is on block U's deciding check U1)264 bad = []265 for n in range(1, SMALL + 1):266 for o in range(1, n + 2):267 complete = [rho for rho in itertools.product(range(o), repeat=n) if _injective(lambda u: rho[u], n)]268 if (len(complete) > 0) != (n <= o): bad.append((n, o, len(complete)))269 R.check("W1", f"every n ≤ {SMALL} and o ≤ n + 1: a reading of the n members into o records that identifies no two exists iff "270 "n ≤ o (exhaustive): a complete reading needs the whole count (the contrapositive of U1), a part of o < n states reads incompletely",271 not bad, f"exceptions {bad}")272 # W2 the translation torsor: on every q ≤ 40 and every pair (x, y), exactly one t with x + t = y; on the three Carriers and273 # their Subjects, sampled pairs274 bad, det = [], []275 for q in range(1, 41):276 for x in range(q):277 for y in range(q):278 if [t for t in range(q) if (x + t) % q == y] != [(y - x) % q]: bad.append((q, x, y))279 for Om, p in SHELLS:280 for q in (Om, p):281 pairs = ((0, 1), (1, 0), (q - 1, q // 2), (q // 3, q - 2)) if q < 10 ** 5 else ((1, 0), (q // 3, q - 2))282 for x, y in pairs:283 sols = sum(1 for t in range(q) if (x + t) % q == y) # every t, exhaustively284 if sols != 1 or (x + (y - x) % q) % q != y: bad.append((q, x, y, sols))285 det.append(f"q={q}: one t per pair, counted over all {q} translations")286 R.check("W2", "every q ≤ 40 and every pair (x, y): exactly one translation t with x + t = y (exhaustive); on the three Carriers "287 "and their Subjects, sampled pairs with every translation tried: exactly one. The origin is frame data (A6)", not bad, "; ".join(det[:3]))288289290# ------------------------------------------------------------------------------------------------------------291# block Q: counting closes by return (00:A5)292# on q ≥ 2 points the successor x ↦ x + 1 has no fixed point, returns after exactly the multiples of q steps and293# reaches every point (Foundation.lean, successor_cycle).294@R.block("Q", BLOCKS["Q"])295def block_Q():296 """Block Q — counting closes by return (EXACT): Q1, Q2."""297 # 00:A5 (p00188)298 ok, det = True, []299 for Om, p in SHELLS:300 for q in (Om, p):301 orb = successor_orbit(q, 0)302 ok &= len(orb) == q and sorted(orb) == list(range(q)) and all((x + 1) % q != x for x in (0, 1, q - 1))303 det.append(f"Ω={Om}: one cycle of {Om}; p={p}: one cycle of {p}")304 R.check("Q1", "on the three Carriers and their Subjects: the orbit of 0 under x ↦ x + 1 returns after exactly q steps and "305 "visits every point; x + 1 ≠ x", ok, "; ".join(det))306 # Q2 every q in [2, 400): the k-th iterate fixes a point iff q | k (k < 3q), every orbit is all of [0, q), no fixed point307 bad = []308 for q in range(2, 400):309 for x in (0, q // 2, q - 1):310 y, ret = x, []311 for k in range(1, 3 * q):312 y = (y + 1) % q313 if y == x: ret.append(k)314 if ret != [q, 2 * q] or sorted(successor_orbit(q, x)) != list(range(q)): bad.append((q, x))315 if any((x + 1) % q == x for x in range(q)): bad.append((q, "fixed point"))316 R.check("Q2", "every q in [2, 400) and x ∈ {0, ⌊q/2⌋, q−1}: C_q^k x = x for 0 < k < 3q exactly at k = q, 2q (by iteration); every "317 "orbit is all of [0, q); no point is fixed", not bad, f"exceptions {bad[:5]}")318319320# ------------------------------------------------------------------------------------------------------------321# block I: completeness is primality (00:A10)322# for q ≥ 2, every ideal of Z/q holding a nonzero residue holds every residue iff q is prime (Foundation.lean,323# isPrime_iff_complete): forward by the Fermat inverse a^(q−2), backward by the annihilator of a zero divisor.324@R.block("I", BLOCKS["I"])325def block_I():326 """Block I — completeness is primality (EXACT): I1, I2."""327 # I1 the forward construction on the Carriers and the Subjects: a^(q−2) inverts every nonzero a328 ok, det = True, []329 for Om, p in SHELLS[:2]:330 for q in (Om, p):331 ok &= all(a * pow(a, q - 2, q) % q == 1 for a in range(1, q))332 det.append(f"q={Om} and q={p}: a·a^(q−2) = 1 for every a ≠ 0")333 Om = SHELLS[2][0]334 ok &= all(a * pow(a, Om - 2, Om) % Om == 1 for a in range(1, 200001))335 det.append(f"q={Om}: for a < 200 001")336 R.check("I1", "on the Carriers and their Subjects: the Fermat inverse a^(q−2) of every nonzero a, so 1 lies in every ideal holding "337 "a, and with it every residue", ok, "; ".join(det))338 # 00:A10 (p00162)339 bad, det = [], []340 for q in range(2, 260):341 comp, prime, zd = is_complete(q), arith.is_prime(q), zero_divisors(q)342 if not (comp == prime == (not zd)): bad.append(q)343 if not prime:344 a, b = zd[0]345 ann = [x for x in range(q) if x * b % q == 0] # the annihilator of b, an ideal holding a346 if not (a in ann and 1 not in ann and principal_ideal(a, q) != list(range(q))): bad.append((q, "annihilator"))347 R.check("I2", "every q in [2, 260): Z/q has no proper nonzero ideal (every residue's ideal holds 1, by search) iff q is prime iff "348 "no zero divisors; for composite q the annihilator of a zero divisor b is a proper ideal holding a ≠ 0", not bad,349 f"258 moduli, {sum(1 for q in range(2, 260) if arith.is_prime(q))} prime; exceptions {bad[:5]}")350351352# ------------------------------------------------------------------------------------------------------------353# block H: the quarter-turn exists iff p ≡ 1 (mod 4) (00:A11)354# for an odd prime p, x² = −1 is solvable iff p ≡ 1 (mod 4) (Foundation.lean, quarter_turn_iff): backward ħ = a^((p−1)/4)355# with a^((p−1)/2) = −1; forward ħ⁴ = 1 and Fermat leave (p − 1) mod 4 = 0.356@R.block("H", BLOCKS["H"])357def block_H():358 """Block H — the quarter-turn exists iff p ≡ 1 (mod 4) (EXACT): H1, H2."""359 # 00:A11 (p00163)360 primes = _primes(3, SWEEP)361 bad = [p for p in primes if bool(quarter_turns(p)) != (p % 4 == 1)]362 built = [p for p in primes if p % 4 == 1 and quarter_turn(p) ** 2 % p != p - 1]363 R.check("H1", f"every odd prime p < {SWEEP}: x² = −1 has a root (by search) iff p ≡ 1 (mod 4); on p ≡ 1 (mod 4) the generator-free "364 "ħ = a^((p−1)/4) is one", not bad and not built, f"{len(primes)} primes; exceptions {bad + built}")365 # H2 the Carriers and their Subjects: ħ = a^S, ħ² = −1, and the two roots ±ħ366 ok, det = True, []367 for Om, p in SHELLS:368 for q in (Om, p):369 h = quarter_turn(q); a = half_power(q)370 ok &= q % 4 == 1 and pow(a, (q - 1) // 2, q) == q - 1 and h == pow(a, (q - 1) // 4, q) and h * h % q == q - 1371 if q < 10 ** 5: ok &= sorted(quarter_turns(q)) == sorted({h, q - h})372 det.append(f"Ω={Om}: ħ={quarter_turn(Om)}; p={p}: ħ={quarter_turn(p)}")373 R.check("H2", "on the three Carriers and their Subjects (all ≡ 1 mod 4): ħ = a^S with a^(2S) = −1 solves x² = −1, and below 10⁵ the "374 "roots are exactly ±ħ (by search)", ok, "; ".join(det))375376377# ------------------------------------------------------------------------------------------------------------378# block M: every prime carries a frame (00:A12)379# every prime field has a primitive root, and its powers reach every nonzero residue (Drive.lean, exists_drive): the380# proof's construction is the product over the prime powers qᵉ ∥ p − 1 of a^((p−1)/qᵉ), a the least with a^((p−1)/q) ≠ 1.381@R.block("M", BLOCKS["M"])382def block_M():383 """Block M — every prime carries a frame (EXACT): M1–M3."""384 # 00:A12 (p00164)385 ok, det = True, []386 for Om, p in SHELLS:387 for q in (Om, p):388 g = drive(q)389 n = element_order(g, q) # by iteration390 powers, y = set(), 1391 for _ in range(q - 1):392 powers.add(y); y = y * g % q393 ok &= n == q - 1 and arith.is_primitive_root(g, q) and powers == set(range(1, q))394 det.append(f"Ω={Om}: g={drive(Om)}; p={p}: g={drive(p)}")395 R.check("M1", "on the three Carriers and their Subjects: the drive g built by the proof's construction has order p − 1 (by iteration "396 "and by the factorisation of p − 1), and g⁰, …, g^(p−2) are all p − 1 nonzero residues", ok, "; ".join(det))397 # M2 every prime below SWEEP: the construction gives a primitive root, each factor z_q of order exactly qᵉ398 bad = []399 for p in _primes(2, SWEEP):400 n = p - 1401 for q, e in arith.factorize(n).items():402 a = next(a for a in range(1, p) if pow(a, n // q, p) != 1)403 z = pow(a, n // q ** e, p)404 if not (pow(z, q ** e, p) == 1 and pow(z, q ** (e - 1), p) != 1): bad.append((p, q))405 if arith.order(drive(p), p) != n: bad.append(p)406 R.check("M2", f"every prime p < {SWEEP}: for each qᵉ ∥ p − 1 the factor z_q = a^((p−1)/qᵉ) has order exactly qᵉ, and their product "407 "is a primitive root", not bad, f"{len(_primes(2, SWEEP))} primes; exceptions {bad[:5]}")408 # M3 every prime below 400: the elements of order p − 1, by iteration, number φ(p − 1), the drive among them409 bad = []410 for p in _primes(2, 400):411 prim = [x for x in range(1, p) if element_order(x, p) == p - 1]412 if len(prim) != arith.phi(p - 1) or drive(p) not in prim: bad.append(p)413 R.check("M3", "every prime p < 400: the elements of order p − 1, found by iteration, number φ(p − 1) and include the drive", not bad,414 f"{len(_primes(2, 400))} primes; exceptions {bad}")415416417if __name__ == "__main__":418 blocks = [a for a in sys.argv[1:] if a in R.blocks]419 if blocks:420 for b in blocks: R.run_block(b)421 sys.exit(0 if R.summary(write=False) else 1)422 sys.exit(0 if R.verify_all() else 1)423