The ledger file frc/ledgers/master/subject.py of the master's block of the subject 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.Subject. ▶ run the rows on Google Colab.
1"""master/subject — the ledger file of the master's block C, the Subject (ledger migration, task LM24, 5 October 2026).23The master predicate ledger (00-ledger/predicates/index.md, published as docs/00-ledger.json) states block C. 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 subject theme6(frc/subject.py). Each check names the rows it decides or corroborates (LEDGER), under a `# 00:C1 (p00021)` marker on7the check that decides the row (PREDICATES).89The rows are C1, C3, C8, C14, C16, C20 and C25, proved in lean/FrcCore/Theme/Subject.lean on the Subject's frame10(τ; 0, 1, g) and on the prime field of lean/FrcCore/Theme/Field.lean. C13 is an X row: its parts are 10:G2 (p10038) and1110:E9 (p10032), paper 10's keys; the theme proves 10:G2 on every capacity (`FRC.Subject.exponent_ladder`), and paper 10's12migration (LM36) binds it. The checks run on the three Subjects p = 13, 173 and 1 373 with their Carriers Ω = 233,1330 089 and 2 408 561, and as sweeps over every prime p = 4κ + 1 below a bound. The Lean side is the key file14lean/FrcCore/Keys/Subject.lean and the certificate lean/FrcCore/Ledgers/Master/Subject.lean.1516 python3 -m frc.ledgers.master.subject every block, the census; exit 1 if a check fails (≈ 20 s)17 python3 -m frc.ledgers.master.subject V one block (K, I, Q, O, V, M or H)18 from frc.ledgers.master.subject import R; R.predicate("00:C16") one row: its blocks run once per session1920Blocks: K the frame's web EXACT (00:C1)21 I the Euclidean–Lorentzian dichotomy EXACT (00:C3)22 Q the square class is chronon parity EXACT (00:C8)23 O the quarter-turn is the odd member EXACT (00:C14)24 V the spinor dichotomy EXACT (00:C16)25 M the mass–energy channel EXACT (00:C20)26 H the horizon is the origin's antipode EXACT (00:C25)2728The notebook frc/ledgers/master/subject.ipynb runs one row per cell, the cell's id its key (gate G13).29"""30import sys3132from frc import arith33from frc.registry import Registry34from frc.extension import Ext35from frc.foundation import quarter_turn, quarter_turns, element_order36from frc.carrier import octant, tsirelson37from frc.subject import (frame, frames, euler, chirality, fold_image, fold_solutions, two_parts, channel,38 projective_line, torsor, boost_act)3940# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----41BLOCK = "C"42KEYS = {"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 key43LEAN = {"C1": "core", "C3": "core", "C8": "core", "C14": "core", "C16": "core", "C20": "core", "C25": "core"} # the rows with a Lean declaration: the libraries whose key files prove them44# ---- end of the generated table ----4546# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys47# 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.48PROOFS = {49 "C1": ["FRC.Subject.frame_web"],50 "C3": ["FRC.Subject.signature", "FRC.Subject.half_class"],51 "C8": ["FRC.Subject.square_class", "FRC.Subject.half_class", "FRC.Shell.Prime.tsirelson", "FRC.Extension.Ext.norm_scale"],52 "C14": ["FRC.Subject.quarter_turn_odd",53 "FRC.Shell.Frame.euler_identity"], # 6:B2 (p06009), the Euler identity as a chart-class property (6-fourier's propagation list, row 5; 9 October 2026)54 "C16": ["FRC.Subject.spinor", "FRC.Subject.no_iso", "FRC.Subject.two_part"],55 "C20": ["FRC.Subject.channel", "FRC.Subject.channel_233"],56 "C25": ["FRC.Subject.horizon_antipode", "FRC.Subject.horizon_generator", "FRC.Subject.boost_unique"],57}5859LEAN_ONLY = () # the rows with a Lean declaration and no python check (gate G12): none6061# The Subjects p = 4κ + 1 with their Carriers Ω = 4S + 1, as in the Carrier's block file: p² < Ω.62SHELLS = [(13, 233), (173, 30089), (1373, 2408561)]63SWEEP = 5000 # the sweeps run over every prime p = 4κ + 1 below it64SMALL = 400 # the sweeps over every drive of p run below it6566# The rows each check decides or corroborates.67LEDGER = {68 "K1": "00:C1", "K2": "00:C1",69 "I1": "00:C3", "I2": "00:C3", "I3": "00:C3, 00:C8",70 "Q1": "00:C8", "Q2": "00:C8", "Q3": "00:C8",71 "O1": "00:C14", "O2": "00:C14",72 "V1": "00:C16", "V2": "00:C16", "V3": "00:C16",73 "M1": "00:C20", "M2": "00:C20", "M3": "00:C20",74 "H1": "00:C25", "H2": "00:C25", "H3": "00:C25",75}7677BLOCKS = {"K": "the frame's web", "I": "the Euclidean–Lorentzian dichotomy", "Q": "the square class is chronon parity",78 "O": "the quarter-turn is the odd member", "V": "the spinor dichotomy", "M": "the mass–energy channel",79 "H": "the horizon is the origin's antipode"}8081# the deciding check of each row: the three Subjects (C16: the sweep, which decides the four-way equivalence); the rest82# corroborate83PREDICATES = {"00:C1": "K1", "00:C3": "I1", "00:C8": "Q1", "00:C14": "O1", "00:C16": "V1", "00:C20": "M1",84 "00:C25": "H1"}8586R = Registry("00", "subject", LEDGER, PREDICATES, sources=[__file__])8788for _p, _Om in SHELLS:89 assert arith.is_prime(_p) and _p % 4 == 1 and arith.is_prime(_Om) and _Om % 4 == 1 and _p * _p < _Om, (_p, _Om)909192def squares(p):93 """Every square x² mod p, 0 included, by search: a set."""94 return {x * x % p for x in range(p)}959697def _shells(lo, hi):98 """The primes p = 4κ + 1 in [lo, hi)."""99 return [n for n in range(lo, hi) if n % 4 == 1 and arith.is_prime(n)]100101102def _web(p, g):103 """The frame's web on (p, g): 2π ≡ −1, g^π ≡ −1, −π·2 ≡ 1, i² ≡ −1 (C1)."""104 k = (p - 1) // 4105 pi, i = 2 * k, (-pow(g, k, p)) % p106 return 2 * pi % p == p - 1 and pow(g, pi, p) == p - 1 and (-pi) * 2 % p == 1 and i * i % p == p - 1107108109# ------------------------------------------------------------------------------------------------------------110# block K: the frame's web (00:C1)111# on every frame π = 2κ and i = −g^κ: 2π ≡ −1, g^π ≡ −1, −π = 2⁻¹, i² = −1; 0 and 1 are squares and the drive is not112# (Subject.lean, frame_web).113@R.block("K", BLOCKS["K"])114def block_K():115 """Block K — the frame's web (EXACT): K1, K2."""116 # 00:C1 (p00021)117 ok, det = True, []118 for p, Om in SHELLS:119 for q in (p, Om):120 g = frame(q)[1]121 ok &= _web(q, g)122 if q < 10 ** 5:123 sq = squares(q)124 ok &= g not in sq and 0 in sq and 1 in sq and element_order(g, q) == q - 1125 else:126 ok &= pow(g, (q - 1) // 2, q) == q - 1127 det.append(f"p={p}: (κ, g, π, i) = {frame(p)}; Ω={Om}: g={frame(Om)[1]}, i={frame(Om)[3]}")128 R.check("K1", "on the three Subjects and their Carriers, with the drive g the generator-free proof builds: 2π ≡ −1, g^π ≡ −1, "129 "−π·2 ≡ 1 and i² ≡ −1 for π = 2κ, i = −g^κ; 0 and 1 are squares and g is not (by search below 10⁵, by Euler's "130 "criterion on Ω = 2 408 561)", ok, "; ".join(det))131 # K2 every prime p = 4κ + 1 below SWEEP with its drive, and every drive below SMALL: the web holds132 bad = [p for p in _shells(5, SWEEP) if not _web(p, frame(p)[1])]133 bad += [(p, g) for p in _shells(5, SMALL) for g in frames(p) if not (_web(p, g) and g not in squares(p))]134 R.check("K2", f"every prime p = 4κ + 1 below {SWEEP} with its drive, and every drive of every such p below {SMALL} (by "135 "iteration): the web closes and the drive is a nonsquare", not bad,136 f"{len(_shells(5, SWEEP))} shells; exceptions {bad[:5]}")137138139# ------------------------------------------------------------------------------------------------------------140# block I: the Euclidean–Lorentzian dichotomy (00:C3)141# ν = g is a nonsquare; x² − ν t² has a zero with t ≠ 0 iff ν is a square; ν = 2⁻¹·(2g), 2⁻¹ a square iff κ is even and142# 2g a square iff κ is odd (Subject.lean, signature; Field.lean, half_square_iff).143@R.block("I", BLOCKS["I"])144def block_I():145 """Block I — the Euclidean–Lorentzian dichotomy (EXACT): I1–I3."""146 # 00:C3 (p00150)147 ok, det = True, []148 for p, Om in SHELLS:149 k, g, _, _ = frame(p)150 sq = squares(p)151 iso = {nu for nu in range(p) if any(nu * t * t % p in sq for t in range(1, p))} # x² = ν t², t ≠ 0, by search152 h = pow(2, -1, p)153 ok &= iso == sq and g not in iso and h * (2 * g) % p == g and h == 2 * k + 1154 ok &= (h in sq) == (k % 2 == 0) and (2 * g % p in sq) == (k % 2 == 1)155 det.append(f"p={p} (κ={k}): 2⁻¹={h} {'square' if h in sq else 'nonsquare'}, 2g={2 * g % p} "156 f"{'square' if 2 * g % p in sq else 'nonsquare'}")157 R.check("I1", "on the three Subjects: the norm form x² − ν t² has a zero with t ≠ 0 exactly for the square ν (by search over every "158 "ν and t), so ν = g is non-split; ν = 2⁻¹·(2g) with 2⁻¹ = 2κ + 1, a square iff κ is even, and 2g a square iff κ is odd",159 ok, "; ".join(det))160 # I2 every prime p = 4κ + 1 below SWEEP: 2⁻¹ = 2κ + 1 is a square iff κ is even, and 2g iff κ is odd (by search)161 bad = []162 for p in _shells(5, SWEEP):163 k, g, _, _ = frame(p)164 sq = squares(p)165 if ((2 * k + 1) in sq) != (k % 2 == 0) or ((2 * g % p) in sq) != (k % 2 == 1): bad.append(p)166 R.check("I2", f"every prime p = 4κ + 1 below {SWEEP}: the classes of 2⁻¹ = 2κ + 1 and of 2g are fixed by the parity of κ (by search)",167 not bad, f"{len(_shells(5, SWEEP))} shells; exceptions {bad[:5]}")168 # I3 the Carriers: c² = 2⁻¹ = 2S + 1 is a square, S even169 ok, det = True, []170 for _, Om in SHELLS:171 S = (Om - 1) // 4172 ok &= S % 2 == 0 and (2 * S + 1) * 2 % Om == 1 and pow(2 * S + 1, (Om - 1) // 2, Om) == 1173 det.append(f"Ω={Om}: S={S}")174 R.check("I3", "on the three Carriers: S is even and c² = 2⁻¹ = 2S + 1 is a square (Euler's criterion), so η₀₀ = −c² carries the "175 "chart's class, not the frame's", ok, "; ".join(det))176177178# ------------------------------------------------------------------------------------------------------------179# block Q: the square class is chronon parity (00:C8)180# g^m is a square iff m is even; the inverse drive is a nonsquare; g² is a square (Subject.lean, square_class); on the181# Carrier [c²] = [2⁻¹] is even iff S is even (half_square_iff), and (ζ + ζ⁷)² = 2 for ζ⁴ = −1 (tsirelson).182@R.block("Q", BLOCKS["Q"])183def block_Q():184 """Block Q — the square class is chronon parity (EXACT): Q1–Q3."""185 # 00:C8 (p00028)186 ok, det = True, []187 for p, _ in SHELLS:188 _, g, _, _ = frame(p)189 sq = squares(p)190 par = all((pow(g, m, p) in sq) == (m % 2 == 0) for m in range(p - 1))191 ginv = pow(g, -1, p)192 ok &= par and ginv not in sq and g * g % p in sq193 det.append(f"p={p}: g={g}, g⁻¹={ginv}")194 R.check("Q1", "on the three Subjects: g^m is a square iff m is even, for every m < p − 1 (by search); the inverse drive g⁻¹ is a "195 "nonsquare and the registered transport g² a square", ok, "; ".join(det))196 # Q2 every prime Ω = 4S + 1 below SWEEP: [c²] = [2S + 1] is the even class iff S is even197 bad = [Om for Om in _shells(5, SWEEP) if ((2 * ((Om - 1) // 4) + 1) in squares(Om)) != (((Om - 1) // 4) % 2 == 0)]198 R.check("Q2", f"every prime Ω = 4S + 1 below {SWEEP}: c² = 2⁻¹ = 2S + 1 is a square iff S is even (by search)", not bad,199 f"{len(_shells(5, SWEEP))} charts; exceptions {bad[:5]}")200 # Q3 the Tsirelson square on the Carriers: ζ of order eight, (ζ + ζ⁷)² = 2201 ok, det = True, []202 for _, Om in SHELLS:203 z = octant(Om)204 ok &= z is not None and pow(z, 4, Om) == Om - 1 and tsirelson(z, Om) == 2205 det.append(f"Ω={Om}: ζ={z}")206 R.check("Q3", "on the three Carriers: ζ = a^((Ω−1)/8) has ζ⁴ = −1 and (ζ + ζ⁷)² = 2, the two-way symmetrisation √2", ok,207 "; ".join(det))208209210# ------------------------------------------------------------------------------------------------------------211# block O: the quarter-turn is the odd member of the ±√−1 pair (00:C14)212# e^{jπ} := (g^j)^{j·2κ} = (−1)^j; the roots h, −h of −1 have representatives of opposite parity, so e^{hπ} = −1 exactly213# on the odd one; the inverse drive is a frame with quarter-turn −i; every frame is g^u with u odd, its quarter-turn i214# when u ≡ 1 (mod 4) and −i when u ≡ 3, and the parity names the class (Subject.lean, quarter_turn_odd).215def _odd_member(p, g):216 k = (p - 1) // 4217 i = (-pow(g, k, p)) % p218 roots = quarter_turns(p)219 ok = all(euler(g, j, p) == (1 if j % 2 == 0 else p - 1) for j in range(p))220 ok &= len(roots) == 2 and roots[0] % 2 != roots[1] % 2221 ok &= all((euler(g, h, p) == p - 1) == (h % 2 == 1) for h in roots)222 gi = pow(g, -1, p)223 ok &= element_order(gi, p) == p - 1 and (-pow(gi, k, p)) % p == (p - i) % p224 for g2 in frames(p):225 u = chirality(g, g2, p)226 i2 = (-pow(g2, k, p)) % p227 ok &= u is not None and u % 2 == 1 and (i2 == i) == (u % 4 == 1) and (i2 == (p - i) % p) == (u % 4 == 3)228 ok &= ((i2 % 2) == (i % 2)) == (u % 4 == 1)229 return ok230231232@R.block("O", BLOCKS["O"])233def block_O():234 """Block O — the quarter-turn is the odd member (EXACT): O1, O2."""235 # 00:C14 (p00034)236 ok, det = True, []237 for p, _ in SHELLS:238 k, g, _, i = frame(p)239 ok &= _odd_member(p, g)240 odd = next(h for h in quarter_turns(p) if h % 2 == 1)241 det.append(f"p={p}: i={i}, the odd member {odd}, {len(frames(p))} frames")242 R.check("O1", "on the three Subjects: e^{jπ} = (g^j)^{2κj} = (−1)^j for every lift j < p; the roots of −1 have opposite parity and "243 "e^{hπ} = −1 exactly on the odd one; the inverse drive is a frame with quarter-turn −i; every frame g' = g^u has u "244 "odd, quarter-turn i iff u ≡ 1 (mod 4), −i iff u ≡ 3, and the same parity as i iff u ≡ 1", ok, "; ".join(det))245 # O2 every prime p = 4κ + 1 below SMALL, every drive as the reference frame246 bad = [(p, g) for p in _shells(5, SMALL) for g in frames(p)[:4] if not _odd_member(p, g)]247 R.check("O2", f"every prime p = 4κ + 1 below {SMALL}, the first four drives each as the reference frame: the same clauses", not bad,248 f"{len(_shells(5, SMALL))} shells; exceptions {bad[:5]}")249250251# ------------------------------------------------------------------------------------------------------------252# block V: the spinor dichotomy (00:C16)253# κ odd iff v₂(p − 1) = 2 iff the fold (r, s) ↦ iʳ (g⁴)ˢ is injective on C₄ × C_κ (and then onto F_p^×) iff254# 3κr + 4s ≡ 1 (mod 4κ) is solvable (Subject.lean, spinor); the shared 2-part 2^m, m = min(v₂(p−1), v₂(Ω−1)), the cover255# degree 2^{v₂(Ω−1)−m}, and the Carrier's 2-part 8 iff S ≡ 2 (mod 4) (two_part).256@R.block("V", BLOCKS["V"])257def block_V():258 """Block V — the spinor dichotomy (EXACT): V1–V3."""259 # 00:C16 (p00151)260 bad, odd = [], 0261 for p in _shells(5, SWEEP):262 k, g, _, _ = frame(p)263 img = fold_image(p, g)264 inj, onto = len(set(img)) == 4 * k, set(img) == set(range(1, p))265 odd += k % 2266 if not ((k % 2 == 1) == ((p - 1) % 8 != 0) == inj == bool(fold_solutions(k)) and (inj <= onto)): bad.append(p)267 R.check("V1", f"every prime p = 4κ + 1 below {SWEEP}: κ odd ⟺ 8 ∤ p − 1 ⟺ the fold iʳ (g⁴)ˢ, r < 4, s < κ, is injective (by "268 "listing its 4κ values) ⟺ 3κr + 4s ≡ 1 (mod 4κ) has a solution (by search); an injective fold is onto F_p^×", not bad,269 f"{len(_shells(5, SWEEP))} shells, {odd} with κ odd; exceptions {bad[:5]}")270 # V2 the three pairs: the 2-parts271 ok, det = True, []272 for p, Om in SHELLS:273 a, b, m, cover, car = two_parts(p, Om)274 S = (Om - 1) // 4275 both = (p - 1) % 2 ** m == 0 and (Om - 1) % 2 ** m == 0276 ok &= both and not ((p - 1) % 2 ** (m + 1) == 0 and (Om - 1) % 2 ** (m + 1) == 0) and 2 ** m * cover == car277 ok &= (car == 8) == (S % 4 == 2) and a == 2 and ((p - 1) // 4) % 2 == 1278 det.append(f"(p, Ω)=({p}, {Om}): v₂ = {a}, {b}; shared C_{2 ** m}, cover degree {cover}, Carrier 2-part {car}, S mod 4 = {S % 4}")279 R.check("V2", "on the three pairs (κ = 3, 43, 343, all odd): 2^m divides p − 1 and Ω − 1 and 2^(m+1) not both, m = min of the "280 "2-adic valuations; the shared order 2^m times the cover degree is the Carrier's 2-part, 8 exactly when S ≡ 2 (mod 4)",281 ok, "; ".join(det))282 # V3 every pair of primes ≡ 1 (mod 4) below 600: the same arithmetic283 bad, n = [], 0284 for p in _shells(5, 600):285 for Om in _shells(5, 600):286 a, b, m, cover, car = two_parts(p, Om)287 n += 1288 if not ((p - 1) % 2 ** m == 0 and (Om - 1) % 2 ** m == 0 and 2 ** m * cover == car289 and not ((p - 1) % 2 ** (m + 1) == 0 and (Om - 1) % 2 ** (m + 1) == 0)290 and (car == 8) == (((Om - 1) // 4) % 4 == 2)): bad.append((p, Om))291 R.check("V3", "every pair of primes ≡ 1 (mod 4) below 600: the shared 2-part, the cover degree and the Carrier's 2-part as in V2",292 not bad, f"{n} pairs; exceptions {bad[:5]}")293294295# ------------------------------------------------------------------------------------------------------------296# block M: the mass–energy channel (00:C20)297# on a prime p with h² = −1: x^{p+1} = 1 iff x = ±1, x^{2(p+1)} = 1 iff x ∈ Q₄ = {±1, ±h}, h^{p+1} = −1 (Subject.lean,298# channel); the Carrier instance 78^58 = 89 = h on Ω = 233 (channel_233).299@R.block("M", BLOCKS["M"])300def block_M():301 """Block M — the mass–energy channel (EXACT): M1–M3."""302 # 00:C20 (p00040)303 ok, det = True, []304 for p, _ in SHELLS:305 h = quarter_turn(p)306 sign, q4 = channel(p, h)307 ok &= sign == [1, p - 1] and sorted(q4) == sorted({1, p - 1, h, p - h}) and pow(h, p + 1, p) == p - 1308 det.append(f"p={p}: h={h}, Q₄={sorted(q4)}")309 for p in (13, 173): # the same inside F_{p²}, by search over every element310 K = Ext(p, frame(p)[1])311 h = quarter_turn(p)312 units = [z for z in K.elements() if z != (0, 0)]313 base = [z for z in units if K.pow(z, p - 1) == (1, 0)]314 boost = {z for z in units if K.pow(z, p + 1) == (1, 0)}315 cover = {z for z in units if K.pow(z, 2 * (p + 1)) == (1, 0)}316 ok &= sorted(base) == [(x, 0) for x in range(1, p)] and len(boost) == p + 1 and len(cover) == 2 * (p + 1)317 ok &= set(base) & boost == {(1, 0), (p - 1, 0)} and set(base) & cover == {(1, 0), (p - 1, 0), (h, 0), (p - h, 0)}318 ok &= K.norm((h, 0)) == p - 1319 R.check("M1", "on the three Subjects with h = ħ: the nonzero x with x^(p+1) = 1 are ±1 and those with x^(2(p+1)) = 1 are Q₄ = {±1, ±h} "320 "(by search), h^(p+1) = −1; inside F_{p²} for p = 13 and 173 (every element): C_{p−1} = F_p^×, it meets C_{p+1} in ±1 "321 "and C_{2(p+1)} in Q₄, and N(h) = h² = −1", ok, "; ".join(det))322 # M2 the Carrier instance323 R.check("M2", "the Carrier instance on Ω = 233: 78^58 = 89 and 89² = −1 (38:A4)", pow(78, 58, 233) == 89 and 89 * 89 % 233 == 232,324 f"78^58 mod 233 = {pow(78, 58, 233)}")325 # M3 every prime p = 4κ + 1 below SWEEP: the channel326 bad = []327 for p in _shells(5, SWEEP):328 h = quarter_turn(p)329 sign, q4 = channel(p, h)330 if not (sign == [1, p - 1] and sorted(q4) == sorted({1, p - 1, h, p - h})): bad.append(p)331 R.check("M3", f"every prime p = 4κ + 1 below {SWEEP}: the sign ±1 and Q₄ as in M1 (by search)", not bad,332 f"{len(_shells(5, SWEEP))} shells; exceptions {bad[:5]}")333334335# ------------------------------------------------------------------------------------------------------------336# block H: the horizon is the origin's antipode on the boost torus (00:C25)337# for w² = ν a nonsquare, the torsor map P ↦ u_P/ū_P from P¹(F_p) to C_{p+1} is an equivariant bijection, origin ↦ 1,338# horizon ↦ −1; ±1 are the rational norm-one elements; w acts as q ↦ ν/q and swaps origin and horizon; the additive339# antipode is no residue, the seam 2κ + 1 = 2⁻¹ = −2κ (Subject.lean, horizon_antipode).340def _horizon(p, nu, boosts=None):341 K = Ext(p, nu)342 P1 = projective_line(p)343 tors = {P: torsor(P, nu, p) for P in P1}344 torus = set(K.norm_one()) if p < 2000 else None345 ok = len(set(tors.values())) == p + 1 and all(K.norm(t) == 1 for t in tors.values())346 if torus is not None: ok &= set(tors.values()) == torus347 ok &= tors[(0, 1)] == (1, 0) and tors[(1, 0)] == (p - 1, 0)348 vs = boosts if boosts is not None else [z for z in K.elements() if K.norm(z) != 0]349 for v in vs:350 rv = K.mul(K.scalar(pow(K.norm(v), -1, p)), K.mul(v, v))351 ok &= all(tors[boost_act(v, P, nu, p)] == K.mul(rv, tors[P]) for P in P1)352 w = (0, 1)353 ok &= all(boost_act(w, (x, 1), nu, p) == ((nu * pow(x, -1, p) % p, 1) if x else (1, 0)) for x in range(p))354 ok &= boost_act(w, (0, 1), nu, p) == (1, 0) and boost_act(w, (1, 0), nu, p) == (0, 1)355 if torus is not None:356 ok &= {t for t in torus if K.mul(t, t) == (1, 0)} == {(1, 0), (p - 1, 0)}357 ok &= {t for t in torus if t[1] == 0} == {(1, 0), (p - 1, 0)}358 k = (p - 1) // 4359 ok &= [s for s in range(p) if 2 * s % p == 0] == [0] and 2 * (2 * k + 1) % p == 1 and (-2 * k) % p == 2 * k + 1360 return ok361362363@R.block("H", BLOCKS["H"])364def block_H():365 """Block H — the horizon is the origin's antipode (EXACT): H1–H3."""366 # 00:C25 (p00139)367 nus13 = [nu for nu in range(1, 13) if nu not in squares(13)]368 ok = all(_horizon(13, nu) for nu in nus13)369 nu173 = [arith.nonresidue(173), frame(173)[1]]370 for nu in nu173:371 K = Ext(173, nu)372 sample = [z for z in K.elements() if K.norm(z) != 0][::97]373 ok &= _horizon(173, nu, sample)374 R.check("H1", "the torsor map P ↦ u_P/ū_P (u_P = ν y + x w) bijects P¹(F_p) onto the norm-one torus C_{p+1}, origin ↦ 1 and horizon ↦ −1, "375 "and is equivariant, tors(v·P) = (v/v̄)·tors(P); ±1 are the torus's rational elements and its only square roots of 1; w "376 "acts as q ↦ ν/q and swaps origin and horizon; 2s = 0 forces s = 0 and 2κ + 1 = 2⁻¹ = −2κ. On p = 13 for every "377 "nonsquare ν and every boost; on p = 173 for ν the least nonsquare and ν = g, every 97th boost", ok,378 f"p=13: {len(nus13)} values of ν; p=173: ν ∈ {nu173}, {len(sample)} boosts")379 # H2 the Subject 1373, ν the least nonsquare: the bijection, the two points, the swap, 40 boosts380 p, nu = 1373, arith.nonresidue(1373)381 K = Ext(p, nu)382 boosts = [(a, b) for a in range(0, p, 97) for b in range(1, p, 211) if K.norm((a, b)) != 0][:40]383 R.check("H2", f"the Subject p = 1373 with ν = {nu}: the torsor map is a bijection onto p + 1 norm-one elements with origin ↦ 1 and "384 "horizon ↦ −1, equivariant under 40 boosts, w swaps origin and horizon", _horizon(p, nu, boosts), f"{len(boosts)} boosts")385 # H3 every prime p = 4κ + 1 below SMALL, ν the least nonsquare: the full statement on every boost below 100, a sample above386 bad = []387 for p in _shells(5, SMALL):388 nu = arith.nonresidue(p)389 Kp = Ext(p, nu)390 vs = None if p < 100 else [z for z in Kp.elements() if Kp.norm(z) != 0][::max(1, p // 3)]391 if not _horizon(p, nu, vs): bad.append(p)392 R.check("H3", f"every prime p = 4κ + 1 below {SMALL} with ν the least nonsquare: the same clauses (every boost below 100, a sample "393 "of boosts above)", not bad, f"{len(_shells(5, SMALL))} shells; exceptions {bad[:5]}")394395396if __name__ == "__main__":397 blocks = [a for a in sys.argv[1:] if a in R.blocks]398 if blocks:399 for b in blocks: R.run_block(b)400 sys.exit(0 if R.summary(write=False) else 1)401 sys.exit(0 if R.verify_all() else 1)402