The ledger file frc/ledgers/master/gravity.py of the master's block of the gravity 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.Gravity. ▶ run the rows on Google Colab.
1"""master/gravity — a ledger file of the master's block E, gravity: the rows the gravity theme proves (ledger migration,2task LM27, 6 October 2026).34The master's block E is bound by this file (the gravity theme). It binds E1, the uniqueness lemma, E3, the linear5layer, E4, the nonlinear completion, E5, the floor's faces, E6, the horizon count, E7, the horizon triple, and E10, the6fold, E12, the chart count beside the declared chart E11, and E14, the eikonal pair and the phase mode beside the declared wave7operator E13 (E1, E4, E5 and E10 since 12 October 2026, E12 since 15 October 2026, E14 since 16 October 2026): the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs each key conjoins8(PROOFS; the realisations E4 and E5 carry a key for their exact clauses, G08 as amended on 12 October 2026), the shells, and9the checks, which call the gravity theme10(frc/gravity.py, frc/drift.py, frc/lattice.py) and, for the chart faces of E5 and the ringdown of E14, the chart theme11(frc/chart_gravity.py; those checks are CHART, and E14's key conjoins Mathlib theorems, CHART below). Each check names the rows it decides12or corroborates (LEDGER), under a `# 00:E6 (p00176)` marker on the check that decides the row (PREDICATES). The Lean side13is lean/FrcCore/Theme/Gravity.lean, Theme/Drift.lean, Theme/Symbol.lean and Theme/Shift.lean, the key file14lean/FrcCore/Keys/Gravity.lean and the certificate lean/FrcCore/Ledgers/Master/Gravity.lean.1516 python3 -m frc.ledgers.master.gravity every block, the census; exit 1 if a check fails17 python3 -m frc.ledgers.master.gravity W one block (W or U)1819Blocks: N the uniqueness lemma: the Maxwell and Fierz–Pauli lines by the symbol method EXACT (00:E1)20 L the linear layer: the Gauss law, the Green's function's sign, the single arrow EXACT (00:E3)21 C the completion: the character, no self-source, the cover triangle, the PN series EXACT (00:E4)22 F the floor's faces: the operational cut, the slip core's content, the dragging EXACT, CHART (00:E5)23 W the horizon count: the registration sphere, the record, the merger law EXACT (00:E6)24 U the horizon triple: the record on the rate face, the response, Smarr EXACT (00:E7)25 P the fold: the two branches, the cut current, the fold return EXACT (00:E10)26 K the chart count: the balls of Z^d against the Ω residues, the Subject shell's three bounds EXACT (00:E12)27 M the ringdown: the eikonal pair, the ℓ = 2 mode of the chart's wave operator, the (2,2,0) exposure CHART (00:E14)2829The notebook frc/ledgers/master/gravity.ipynb runs one row per cell, the cell's id its key (gate G13).30"""31import sys32from fractions import Fraction3334import random3536from frc import arith37from frc import chart as C38from frc import chart_gravity as CG39from frc import drift as D40from frc import lattice as LT41from frc.registry import Registry42from frc.gravity import (squares, conic_points, sphere_points, sphere_brute, record, area, rate_mass, temperature,43 response, merger_area)4445# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----46BLOCK = "E"47KEYS = {"E1": "p00052", "E3": "p00154", "E4": "p00055", "E5": "p00056", "E6": "p00176", "E7": "p00058", "E10": "p00147", "E11": "p00198", "E12": "p00199", "E13": "p00200", "E14": "p00201"} # every row of the block: its label and its accession key48LEAN = {"E1": "core", "E3": "core", "E4": "core", "E5": "core", "E6": "core", "E7": "core", "E10": "core", "E12": "core", "E14": "ml"} # the rows with a Lean declaration: the libraries whose key files prove them49# ---- end of the generated table ----5051# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys52# 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.53PROOFS = {54 "E1": ["FRC.Symbol.maxwell_unique", "FRC.Symbol.fierz_pauli_unique", "FRC.Symbol.vec_invariant", "FRC.Symbol.fierz_pauli_invariant"],55 "E3": ["FRC.Drift.gauss_law", "FRC.Symbol.fierz_pauli_unique", "FRC.Drift.conj_pow", "FRC.Drift.conj_branch"],56 "E4": ["FRC.Drift.gauss_law", "FRC.Drift.character_composition", "FRC.Drift.character_unique", "FRC.Drift.cover_triangle",57 "FRC.Drift.cover_deviation", "FRC.Drift.pn_coefficients"], # a realisation's key proves its exact clauses (G08 as amended on 12 October 2026)58 "E5": ["FRC.Drift.compression", "FRC.Cycle.cyc_add_n", "FRC.Drift.cut_ordering"],59 "E6": ["FRC.Grav.sphere_area", "FRC.Grav.sphere_area_rung", "FRC.Grav.count_identity", "FRC.Grav.merger_area"],60 "E7": ["FRC.Grav.count_identity", "FRC.Grav.record_mass", "FRC.Grav.record_response", "FRC.Grav.temperature_rate",61 "FRC.Grav.smarr", "FRC.Grav.record_response_rate"],62 "E10": ["FRC.Drift.fold_return", "FRC.Drift.fold_collision", "FRC.Drift.cut_area_monotone", "FRC.Drift.cut_ordering",63 "FRC.Cycle.cyc_add_n"],64 "E12": ["FRC.Grav.chart_plane_overflows", "FRC.Grav.chart_space_overflows", "FRC.Grav.chart_line_fits",65 "FRC.Grav.chart_lab_instance"], # the chart count beside the declared chart E11 (master T1 ill-posed, 15 October 2026)66}67# The Mathlib theorems of E14's key (lean/FrcLedger/Theme/Strong.lean): the eikonal pair of the exponential reading and the68# shadow–ringdown bracket; the row's ℓ = 2 mode is the chart check M2 (master T5 ill-posed, 16 October 2026).69CHART = {70 "E14": ["FRC.Strong.eikonal_pair", "FRC.Strong.shadow_bracket"],71}7273LEAN_ONLY = () # the rows with a Lean declaration and no python check (gate G12): none7475SWEEP = 200 # the sphere sweep runs over every prime p = 4κ + 1 below it76BRUTE = [5, 13, 17, 29, 37] # the shells enumerated point by point77IDENT = 10000 # the identities run over every prime p = 4κ + 1 below it78MERGER = (27811, 1596) # the merger instance of 21-gravity and 37-sim7980LEDGER = {"N1": "00:E1", "N2": "00:E1", "L1": "00:E3", "L2": "00:E3", "C1": "00:E4", "C2": "00:E4", "F1": "00:E5", "F2": "00:E5",81 "W1": "00:E6", "W2": "00:E6", "W3": "00:E6", "U1": "00:E7", "U2": "00:E7", "P1": "00:E10", "P2": "00:E10",82 "K1": "00:E12", "K2": "00:E12", "K3": "00:E12", "M1": "00:E14", "M2": "00:E14"}83BLOCKS = {"N": "the uniqueness lemma: the Maxwell and Fierz–Pauli lines by the symbol method",84 "L": "the linear layer: the Gauss law, the Green's function's sign, the single arrow",85 "C": "the completion: the character, no self-source, the cover triangle, the PN series",86 "F": "the floor's faces: the operational cut, the slip core's content, the dragging",87 "W": "the horizon count: the registration sphere, the record, the merger law",88 "U": "the horizon triple: the record on the rate face, the response, Smarr",89 "P": "the fold: the two branches, the cut current, the fold return",90 "K": "the chart count: the balls of Z^d against the Ω residues, the Subject shell's three bounds",91 "M": "the ringdown: the eikonal pair, the ℓ = 2 mode of the chart's wave operator, the (2,2,0) exposure"}92PREDICATES = {"00:E1": "N1", "00:E3": "L1", "00:E4": "C1", "00:E5": "F1", "00:E6": "W1", "00:E7": "U1", "00:E10": "P1", "00:E12": "K1", "00:E14": "M1"}9394R = Registry("00", "gravity", LEDGER, PREDICATES, sources=[__file__])959697def _shells(lo, hi):98 return [n for n in range(lo, hi) if n % 4 == 1 and arith.is_prime(n)]99100101def near(x, y, rel=None, abs_=None):102 """|x − y| within the stated tolerance, the chart's float x read as a Fraction against rational bounds."""103 d = abs(Fraction(x) - Fraction(y))104 return (rel is not None and d <= Fraction(rel) * abs(Fraction(y))) or (abs_ is not None and d <= Fraction(abs_))105106107# ------------------------------------------------------------------------------------------------------------108# block N: the uniqueness lemma (00:E1)109# in every gauge sector the gauge-invariant adjacency-local quadratic action is one line: spin 1 the Maxwell line110# a₁ + a₂ = 0, the symbol of F², and spin 2 the Fierz–Pauli line (−1, 2, −2, 1), the nullspace of the gauge variation at111# random rational symbols (Symbol.lean: vec_invariant, maxwell_unique, fierz_pauli_invariant, fierz_pauli_unique); the112# discrete Fierz–Pauli functional on ℤ_N⁴ is invariant under the gauge shift with central differences and not with113# one-sided ones. The quadratic sector of Tr F² is the Maxwell line in every colour component; the non-abelian completion114# is 27-fields' (27:C2). The same functions decide 21:C9 (checks B1, B2 of frc/ledgers/p21_gravity.py).115@R.block("N", BLOCKS["N"])116def block_N():117 """Block N — the uniqueness lemma (EXACT): N1–N2."""118 # 00:E1 (p00052)119 lines = [LT.fierz_pauli_line(samples=k) for k in (12, 16)]120 ok = all(l[0] and l[1] for l in lines)121 ok &= LT.fp_gauge_invariant(3, 4, seed=7) and LT.fp_gauge_invariant(3, 4, seed=11) and LT.fp_gauge_invariant(4, 4, seed=7)122 ok &= not LT.fp_gauge_invariant(3, 4, seed=7, kind="forward")123 ns1, ns2 = lines[0][2], lines[0][3]124 R.check("N1", "the uniqueness lemma: by the symbol method over ℚ (the gauge variation at 12 and 16 random rational symbols in "125 "Minkowski signature) the gauge-invariant quadratic forms are one line in each sector — spin 1 the Maxwell line a₁ + a₂ = 0, "126 "the symbol of F², and spin 2 the Fierz–Pauli line (−1, 2, −2, 1), the symbol of the linearised Einstein–Hilbert action; "127 "the discrete Fierz–Pauli functional on ℤ₃⁴ (two seeds) and ℤ₄⁴ with random integer fields is invariant under the gauge "128 "shift h ↦ h + Dξ + (Dξ)ᵀ for central differences and fails for one-sided ones (the control); the quadratic sector of "129 "Tr F² is the Maxwell line in every colour component", ok,130 f"spin-1 line {[str(x) for x in ns1[0]]}, spin-2 line {[str(x) for x in ns2[0]]}" if ns1 and ns2 else "no line")131 # N2 the lines do not depend on the dimension: d = 3, 5 (the lemma is dimension-free and metric-free)132 ok = True; det = []133 for d in (3, 5):134 n1 = LT.symbol_nullspace(1, samples=12, d=d, seed=9); n2 = LT.symbol_nullspace(2, samples=14, d=d, seed=9)135 fp = [Fraction(-1), Fraction(2), Fraction(-2), Fraction(1)]136 ok &= len(n1) == 1 and n1[0][0] + n1[0][1] == 0137 ok &= len(n2) == 1 and all(n2[0][i] * fp[0] == n2[0][0] * fp[i] for i in range(4))138 det.append(f"d={d}: spin-1 {len(n1)} line, spin-2 {len(n2)} line")139 R.check("N2", "the same two lines in dimensions 3 and 5 at fresh random symbols: the uniqueness lemma reads the symbol alone, "140 "in every dimension", ok, "; ".join(det))141142143# ------------------------------------------------------------------------------------------------------------144# block L: the linear layer (00:E3)145# the Coulomb law as the lattice Green's function: the Gauss law (the flux through a region's boundary equals the146# enclosed divergence, Drift.lean: gauss_law) and the exact Green's function of the Dirichlet grid, entrywise positive,147# so the pair energy's cross term lowers the energy exactly for like signs; the single arrow: the time-reversed clock is148# the Frobenius branch, the conjugate orbit of the drive (Drift.lean: conj_pow, conj_branch). The same functions decide149# 21:C11 (check C4) and 21:C3 (check C12) in frc/ledgers/p21_gravity.py; the paper's Green's function values are its E1.150@R.block("L", BLOCKS["L"])151def block_L():152 """Block L — the linear layer (EXACT): L1–L2."""153 # 00:E3 (p00154)154 rng = random.Random(154)155 gauss = True156 for _ in range(20):157 m = rng.randint(4, 12)158 J = [[0] * m for _ in range(m)]159 for x in range(m):160 for y in range(x + 1, m):161 v = rng.randint(-5, 5); J[x][y], J[y][x] = v, -v162 gauss &= D.gauss_law(J, {x for x in range(m) if rng.randrange(2) == 0})163 signs = [D.pair_energy_sign(k) for k in (3, 4)]164 arrows = [D.single_arrow(p, nu) for p, nu in ((13, 2), (17, 3), (37, 2))]165 ok = gauss and all(s[0] for s in signs) and all(a[0] and a[1] == p + 1 for a, (p, _) in zip(arrows, ((13, 2), (17, 3), (37, 2))))166 R.check("L1", "the Coulomb law as the lattice Green's function: on 20 random graphs with antisymmetric integer link currents the "167 "divergence over a random region equals the flux through its boundary (the Gauss law); over ℚ the Green's function of the "168 "Dirichlet grids 3³ and 4³ is entrywise positive, so the pair energy's cross term −m₁m₂G_ab lowers the energy exactly for "169 "like signs; the single arrow: on 𝔽_{p²}, p = 13, 17, 37, the Frobenius is the conjugation, the conjugate orbit of the "170 "norm-one circle's generator is its orbit reversed, and the conjugation is no translation of the circle (it fixes ±1 alone)",171 ok, f"G_ab = {signs[0][1]} (3³), {signs[1][1]} (4³); circles of order {[a[1] for a in arrows]}")172 # L2 the cross term's sign is the product of the source signs, on the 3³ grid173 ok, Gab, Gaa = D.pair_energy_sign(3)174 R.check("L2", "the 3³ grid: the cross term −m₁m₂G_ab of the pair energy is negative for (1, 1), (2, 3), (−1, −1), (−3, −2) and "175 "positive for (1, −1), (2, −3), (−1, 1); G_ab = 5/5712 at the opposite corners", ok, f"G_ab = {Gab}, G_aa = {Gaa}")176177178# ------------------------------------------------------------------------------------------------------------179# block C: the nonlinear completion (00:E4)180# the exponential reading is the character and the unique function with the composition law (Drift.lean:181# character_composition, character_unique); what gravitates is transfer, antisymmetric link currents whose diagonal is182# zero, so a region's divergence is its boundary flux and the static potential of a source is harmonic off the source,183# the field of two sources their sum (gauss_law); the cover triangle 2γ − β = 1, γ = 1 forces β = 1 (cover_triangle,184# cover_deviation); the exponential metric against the isotropic Schwarzschild form, β = γ = 1 and the classical tests185# exact through first order (pn_coefficients). The same functions decide 21:C11, C25, C7, C8 (checks C4, C5, D1).186@R.block("C", BLOCKS["C"])187def block_C():188 """Block C — the nonlinear completion (EXACT): C1–C2."""189 # 00:E4 (p00055)190 ok = all(D.exponential_reading(p) for p in (13, 17, 29))191 rng = random.Random(55)192 for _ in range(20):193 m = rng.randint(4, 12)194 J = [[0] * m for _ in range(m)]195 for x in range(m):196 for y in range(x + 1, m):197 v = rng.randint(-5, 5); J[x][y], J[y][x] = v, -v198 ok &= all(J[x][x] == 0 for x in range(m)) and D.gauss_law(J, {x for x in range(m) if rng.randrange(2) == 0})199 ok &= D.cover_triangle(Fraction(1), Fraction(1)) and not D.cover_triangle(Fraction(1), Fraction(2))200 pn = D.pn_coefficients(6)201 ok &= pn["ok"] and pn["beta"] == 1 and pn["gamma"] == 1 and Fraction(2 + 2 * pn["gamma"] - pn["beta"], 3) == 1202 ok &= pn["dA"][:3] == [0, 0, 0] and pn["dA"][3] == Fraction(1, 6) and pn["dB"][:2] == [0, 0] and pn["dB"][2] == Fraction(1, 2)203 R.check("C1", "the nonlinear completion: on 𝔽₁₃, 𝔽₁₇, 𝔽₂₉ every nonzero residue composes, c^(a+b) = c^a c^b below the full cycle, "204 "and a function with the composition law is rebuilt from f(1) alone as c^a — the exponential reading is the character, "205 "the unique scale-covariant one; on 20 random graphs the link currents are antisymmetric with zero diagonal (no self-link), "206 "and the divergence over a random region equals its boundary flux; the cover triangle 2γ − β = 1 with γ = 1 forces "207 "β = 1 and a second β fails it; the exponential metric read against the isotropic Schwarzschild form gives β = γ = 1, "208 "the perihelion factor (2 + 2γ − β)/3 = 1, and deviations δA = U³/6, δB = U²/2 and nothing lower: the classical tests exact",209 ok, f"β = {pn['beta']}, γ = {pn['gamma']}, δA = {[str(x) for x in pn['dA'][:5]]}, δB = {[str(x) for x in pn['dB'][:4]]}")210 # C2 the static potential is harmonic off its source and sources superpose: the exact Dirichlet potential211 okc, currents = LT.cut_current(2)212 R.check("C2", "the static potential of a unit source on the Dirichlet box {−2..2}³, solved exactly over ℚ, is harmonic off the "213 "source: the flux through the cut of every graph ball r = 0, 1, 2 is the enclosed charge 1 — the potential sources nothing "214 "of its own, and the field of two sources is the sum (the system is linear)", okc,215 f"currents {[str(c) for c in currents]} on the areas 6, 30, 78")216217218# ------------------------------------------------------------------------------------------------------------219# block F: the floor's faces (00:E5)220# the operational cut r_f = r_s/ln Ω between the slip core and the mass in the chart's own numbers (Drift.lean:221# cut_ordering); the slip core's content confined by the drive, the compression identity and the finite order of the222# shift (compression, Shift.lean: cyc_add_n); the floor's coupling m²/Ω on Ω = s². The chart faces (CHART): the exact223# profile horizonless, the round trip e^{2u(r_f)} = Ω, the preferred-frame scale 1/√Ω, the dragging at the Lense–Thirring224# value. The same functions decide 21:X3, X8, C12, C10, C17, P2 (checks C13, A6, E5, E7, E13 of the paper's ledger file).225@R.block("F", BLOCKS["F"])226def block_F():227 """Block F — the floor's faces (EXACT, CHART): F1–F2."""228 # 00:E5 (p00056)229 high, thr = D.cut_ordering(C.LN_OMEGA, 10 ** 6)230 low, _ = D.cut_ordering(C.LN_OMEGA, 100)231 ok = high and not low and thr == Fraction("321489") / 16232 returns = [D.offset_return(n, sec) for n, sec in ((8, {1, 2, 3}), (12, {0, 5, 6, 7, 11}), (9, {4}))]233 ok &= all(r[0] and r[1] == n for r, (n, _) in zip(returns, ((8, 0), (12, 0), (9, 0))))234 ok &= all(D.compression_identity(n, sec) for n, sec in ((8, {1, 2, 3}), (9, {4})))235 ok &= all(D.dilution(m, s) for m in (1, 3, 1000) for s in (5, 1552, 10 ** 61))236 R.check("F1", "the floor's faces, exact: at the import ln Ω = 283.5 the operational cut r_f = 2M/ln Ω lies between the slip core "237 "r_* = √M and the mass, r_*² < r_f² < M² as L²M < (2M)² and 2M < LM, for M = 10⁶ Planck masses and not for M = 100 "238 "(the threshold (ln Ω/2)² = 20 093.06); on the cycles ℤ₈, ℤ₁₂, ℤ₉ with a sector the drive's step splits the sector's "239 "weight into what stays and what leaks to the offset sector, conserves the whole, and returns it after n steps — the "240 "slip core's content is confined, nothing lost; the floor's coupling of two masses m is (m/√Ω)² = m²/Ω exactly on Ω = s²",241 ok, f"threshold {thr}; orders {[r[1] for r in returns]}")242 # F2 the chart faces243 u0, floor_rate, bound, low_rate = CG.horizonless()244 cut = CG.operational_cut(10 ** 6)245 scale = CG.preferred_frame_scale()246 drag = CG.dragging_field(J=Fraction(3, 10), r=10)247 ok = Fraction(u0) < Fraction(bound) and Fraction(floor_rate) > 0 and near(low_rate, floor_rate, rel=Fraction(1, 10 ** 9))248 ok &= cut["ordered"] and near(cut["round_trip"], CG.OMEGA, rel=Fraction(1, 10 ** 6))249 ok &= near(scale, Fraction("2.74e-62"), rel=Fraction(1, 100)) and Fraction(scale) < Fraction(1, 10 ** 61)250 ok &= near(drag["axis"], CG.lense_thirring(Fraction(3, 10), 10), rel=Fraction(1, 10 ** 6)) and near(drag["equator"], -Fraction(3, 10) / 1000, rel=Fraction(1, 10 ** 6))251 R.check("F2", "the floor's chart faces [chart]: the exact profile is horizonless, u(0) = 2.622 Gm finite below π r_* and the "252 "clock-rate factor e^{−2u} ≥ e^{−2u(0)} > 0 everywhere; at M = 10⁶ the cut is ordered and the round trip e^{2u(r_f)} = Ω; "253 "the preferred-frame scale is the floor 1/√Ω = 2.7 × 10⁻⁶² at ln Ω = 283.5, far below every bound; the gravitomagnetic "254 "dipole's curl is 2J/r³ on the axis, the Lense–Thirring rate, and −J/r³ on the equator", ok,255 f"u(0) = {u0:.4f}, 1/√Ω = {scale:.3e}, axis {drag['axis']:.4e}", kind="CHART")256257258# ------------------------------------------------------------------------------------------------------------259# block W: the horizon count (00:E6)260# the registration sphere x² + y² + z² = κ² has p(p + 1) points, at every nonzero square rung; the record S = κ(p + 1)261# with 4S + 1 = p² and S/A = κ/p; the merger law ΔA = 2 M₁ M₂ on A = M(M + 1) (Gravity.lean: sphere_area,262# sphere_area_rung, count_identity, merger_area).263@R.block("W", BLOCKS["W"])264def block_W():265 """Block W — the horizon count (EXACT): W1–W3."""266 # 00:E6 (p00176)267 bad = []268 for p in _shells(5, SWEEP):269 k = (p - 1) // 4270 r = squares(p)271 ok = sphere_points(p, k * k % p) == area(p)272 ok &= all(sphere_points(p, a) == p * p + p * (r[a] - 1) for a in range(1, p)) # p² + p χ(a), χ(a) = r[a] − 1273 ok &= all(conic_points(p, c) == (p - 1 if c else 2 * p - 1) for c in range(p))274 S, A = record(p), area(p)275 ok &= 4 * S + 1 == p * p and Fraction(S, A) == Fraction(k, p) and 4 * S * p == A * (p - 1)276 if not ok: bad.append(p)277 mbad = [(a, b) for a in range(1, 120) for b in range(1, 120) if merger_area(a, b) != 2 * a * b]278 R.check("W1", f"every prime p = 4κ + 1 below {SWEEP}: the sphere x² + y² + z² = κ² has p(p + 1) points, every rung a ≠ 0 "279 "p² + p χ(a), the conic x² + y² = c has p − 1 points (c ≠ 0) and 2p − 1 (c = 0); the record S = κ(p + 1) with "280 "4S + 1 = p², S/A = κ/p and 4Sp = A(p − 1); the merger law A(M₁ + M₂) − A(M₁) − A(M₂) = 2M₁M₂ on A = M(M + 1) "281 "for all M₁, M₂ < 120", not bad and not mbad,282 f"{len(_shells(5, SWEEP))} shells; exceptions {bad} {mbad[:2]}")283 # W2 a second method: the spheres enumerated point by point284 bad = [p for p in BRUTE if sphere_brute(p, ((p - 1) // 4) ** 2) != area(p)]285 R.check("W2", f"the shells {', '.join(map(str, BRUTE))} enumerated point by point: the sphere at the capacity has p(p + 1) "286 "points (30 at p = 5, the rate 30/125 = 6/25 of 37-sim)", not bad and temperature(5) == Fraction(6, 25),287 f"exceptions {bad}")288 # W3 the record law closes at the coherence horizon: S = (Ω − 1)/4 at Ω = p²; the merger instance289 bad = [p for p in _shells(5, IDENT) if (p * p - 1) % 4 or (p * p - 1) // 4 != record(p)]290 m1, m2 = MERGER291 ok = not bad and merger_area(m1, m2) == 88772712 == 2 * m1 * m2292 R.check("W3", f"every prime p = 4κ + 1 below {IDENT}: at Ω = p² the record S = κ(p + 1) is (Ω − 1)/4; the merger "293 "27 811 + 1 596 → 29 407 gives ΔA = 88 772 712 = 2 · 27 811 · 1 596", ok, f"exceptions {bad}")294295296# ------------------------------------------------------------------------------------------------------------297# block U: the horizon triple (00:E7)298# S = (A/4)(1 − 1/p) = M(M − 1) on M = (p + 1)/2; dS/dM = p; T = (p + 1)/p², T_resp = 1/p, T = T_resp(1 + 1/p); Smarr299# 2 T_resp S = M(1 − 1/p) and 2 T S = M(1 − 1/p²) (Gravity.lean: count_identity, record_mass, record_response,300# temperature_rate, smarr).301@R.block("U", BLOCKS["U"])302def block_U():303 """Block U — the horizon triple (EXACT): U1–U2."""304 # 00:E7 (p00058)305 bad = []306 for p in _shells(5, IDENT):307 S, A, M, T, Tr = record(p), area(p), rate_mass(p), temperature(p), response(p)308 Sf = lambda m: m * (m - 1)309 ok = Fraction(S) == Fraction(A, 4) * (1 - Fraction(1, p)) and S == M * (M - 1)310 ok &= Fraction(Sf(M + 3) - Sf(M - 3), 6) == p and Sf(M + 1) - Sf(M) == p + 1 # dS/dM = 2M − 1 = p311 ok &= T == Fraction(p + 1, p * p) and Tr == Fraction(1, p) and T == Tr * (1 + Fraction(1, p))312 ok &= 2 * Tr * S == M * (1 - Fraction(1, p)) and 2 * T * S == M * (1 - Fraction(1, p * p))313 if not ok: bad.append(p)314 R.check("U1", f"every prime p = 4κ + 1 below {IDENT}: S = (A/4)(1 − 1/p) = M(M − 1) on M = (p + 1)/2; the central difference "315 "of S(M) is p (dS/dM = p); T = A/p³ = (p + 1)/p², T_resp = 1/p and T = T_resp(1 + 1/p); 2 T_resp S = M(1 − 1/p) "316 "and 2 T S = M(1 − 1/p²), in exact fractions", not bad, f"{len(_shells(5, IDENT))} shells; exceptions {bad}")317 # U2 the Subjects 13, 173, 1373: the values318 det = []319 for p in (13, 173, 1373):320 det.append(f"p={p}: S={record(p)}, M={rate_mass(p)}, T={temperature(p)}")321 ok = record(13) == 42 == rate_mass(13) * (rate_mass(13) - 1) and temperature(13) == Fraction(14, 169)322 R.check("U2", "the Subject 13: S = 3 · 14 = 42 = 7 · 6 on M = 7, T = 14/169, T_resp = 1/13; and the Subjects 173 and 1373",323 ok, "; ".join(det))324325326# ------------------------------------------------------------------------------------------------------------327# block P: the fold (00:E10)328# the two chart branches are two Carrier data: on a frame the residue products r₁g^Δ, r₂ coincide at exactly one lift,329# the pairs never (Drift.lean: fold_collision); the cut area of the graph balls of ℤ³ is 6(2r² + 2r + 1) and grows at every330# step, so the cut current Q/A_r of the enclosed charge recovers r (cut_area_monotone, the exact Dirichlet potential); the331# fold return through an interior chart is the bare return term by term, its period sum the uniform floor and the full332# period the identity (fold_return, Shift.lean: cyc_add_n); the cut ordered in the substrate coordinate (cut_ordering).333# The DFT fold of the paper's toy (21:P7, check C10) is one interior chart among all.334@R.block("P", BLOCKS["P"])335def block_P():336 """Block P — the fold (EXACT): P1–P2."""337 # 00:E10 (p00147)338 gens = {p: arith.primitive_root(p) for p in (13, 17, 29)}339 coll = {p: D.fold_collision(p, g) for p, g in gens.items()}340 ok = all(c[0] and c[1] == (p - 1) * (p - 2) for p, c in coll.items())341 areas = [LT.ball_cut_area(r) for r in range(7)]342 ok &= all(c == f for c, f in areas) and all(areas[i][0] < areas[i + 1][0] for i in range(6))343 ok &= all(areas[r + 1][1] == areas[r][1] + 24 * (r + 1) for r in range(6))344 okc, currents = LT.cut_current(2)345 ok &= okc and currents == [Fraction(1, 6), Fraction(1, 30), Fraction(1, 78)]346 ok &= D.fold_return(17, 8, 4) and D.fold_return_general(17, 8, 4) and D.fold_return_general(13, 9, 5, seed=7) and D.fold_return_general(29, 10, 3)347 ok &= D.cut_ordering(C.LN_OMEGA, 10 ** 6)[0]348 R.check("P1", "the fold is a chart projection: on 𝔽₁₃, 𝔽₁₇, 𝔽₂₉ (exhaustive) every ordered pair of distinct nonzero positions "349 "has exactly one lift Δ with r₁g^Δ = r₂ — the residue product collides, the pair (r, g^{−Δ}) never; the cut area of the "350 "graph balls of ℤ³, counted, is 6(2r² + 2r + 1) for r ≤ 6, growing by 24(r + 1) at each step, and the exact Dirichlet "351 "potential's flux through every cut is the enclosed charge, so the cut current 1/A_r = 1/6, 1/30, 1/78 recovers r; on the "352 "chains C₈, C₉, C₁₀ over 𝔽₁₇, 𝔽₁₃, 𝔽₂₉ with a random invertible interior chart (and the paper's DFT fold) the exterior "353 "return through the fold equals the bare return term by term, the period sum is the all-ones block on the exterior and the "354 "full period is the identity; the cut is ordered, r_* < r_f < M, at M = 10⁶", ok,355 "; ".join(f"p={p}: {c[1]} pairs" for p, c in coll.items()) + f"; areas {[a[0] for a in areas]}")356 # P2 the paper's instance: the period-averaged exterior return through the DFT fold is the uniform floor operator357 ok = D.fold_return(17, 8, 4) and D.fold_return(13, 12, 4) and D.fold_return(29, 8, 4)358 R.check("P2", "the 4-point DFT fold (the quarter turn i of the shell as the kernel) of the chain C₈ over 𝔽₁₇ and 𝔽₂₉ and of C₁₂ over 𝔽₁₃: the "359 "period-averaged exterior return P_E F Uⁿ F⁻¹ P_E is the uniform floor operator, every nonzero entry equal — no prompt "360 "echo structure", ok, "")361362363# ------------------------------------------------------------------------------------------------------------364# block K: the chart count (00:E12; master T1 ill-posed under Q20, reports/daily-push/t1-push-20261015.md)365# a homogeneous chart on N cells that is Z^d-flat to radius R holds the l^1 ball of Z^d at R: 2R+1, 2R^2+2R+1,366# (4R^3+6R^2+8R+3)/3 cells; at the horizon radius R = floor(sqrt Omega) on the Omega residues the planar and spatial367# balls overflow and the linear one fits (Gravity.lean: chart_plane_overflows, chart_space_overflows, chart_line_fits,368# chart_lab_instance). A Subject shell p inside Omega has three bounds, read on the roots: nesting p^4 < Omega (00:B8),369# the frame variety p^3 <= Omega (SL_2's elements are frame moves, not registrations: C22), the plane p^2 < Omega (A4).370# On SL_2(F_p) commuting generators lie in an abelian subgroup of order at most 2p (the centralisers of the non-central371# elements, exhaustive on 5, 7, 13), and on SL_2(F_5) no triple of generators reproduces the radius-2 ball of Z^3372# (exhaustive). No count above Omega is formed.373def _ball(d, R):374 if d == 1: return 2 * R + 1375 if d == 2: return 2 * R * R + 2 * R + 1376 n = 4 * R ** 3 + 6 * R ** 2 + 8 * R + 3377 return n // 3378379def _flat_radius(d, N):380 R = 0381 while _ball(d, R + 1) <= N: R += 1382 return R383384def _sl2(p):385 return [(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]386387def _mul(x, y, p):388 a, b, c, d = x; e, f, g, h = y389 return ((a * e + b * g) % p, (a * f + b * h) % p, (c * e + d * g) % p, (c * f + d * h) % p)390391def _inv(x, p):392 a, b, c, d = x393 return (d % p, (-b) % p, (-c) % p, a % p)394395@R.block("K", BLOCKS["K"])396def block_K():397 """Block K — the chart count (EXACT): K1–K3."""398 import itertools399 from math import isqrt400 # 00:E12 (p00199)401 brute = lambda d, r: sum(1 for v in itertools.product(range(-r, r + 1), repeat=d) if sum(abs(x) for x in v) <= r)402 ok = all(_ball(d, r) == brute(d, r) for d in (1, 2, 3) for r in range(0, 7))403 ok &= all(_ball(2, isqrt(Om)) > Om and _ball(3, isqrt(Om)) > Om and _ball(1, isqrt(Om)) <= Om for Om in range(5, 200001))404 shells = [13, 17, 29, 37, 157, 233, 641, 1373, 30089, 2408561]405 r3 = {Om: _flat_radius(3, Om) for Om in shells}406 ok &= r3[2408561] == 121 and _ball(3, 122) == 2451225 and isqrt(2408561) == 1551 and _flat_radius(2, 2408561) == 1096407 ok &= all(3 * r3[Om] <= isqrt(Om) for Om in shells if Om >= 157)408 R.check("K1", "the chart count: the ℓ¹ balls of ℤ^d (2R+1, 2R²+2R+1, (4R³+6R²+8R+3)/3) agree with enumeration for R ≤ 6; at the "409 "horizon radius R = ⌊√Ω⌋ the planar and spatial balls hold more than Ω cells and the linear ball fits, for every Ω in "410 "[5, 2·10⁵]; the largest ℤ³-flat radius on the Ω residues is 1, 1, 2, 2, 4, 5, 7, 9, 27, 121 on the ten ledger shells, "411 "at most ⌊√Ω⌋/3 from 157 on, 121 against 1551 on the laboratory Carrier (the planar radius 1096)", ok,412 "; ".join(f"{Om}: R3 {r3[Om]}, sqrt {isqrt(Om)}" for Om in shells))413 # K2 the frame space: abelian subgroups of SL_2(F_p) have order <= 2p; the commuting-chart radius414 ok = True; det = []415 for p in (5, 7, 13):416 els = _sl2(p); I = (1, 0, 0, 1); mI = (p - 1, 0, 0, p - 1)417 orders = set(); reps = {}418 for x in els:419 if x in (I, mI): continue420 Cx = [y for y in els if _mul(x, y, p) == _mul(y, x, p)]421 orders.add(len(Cx)); reps.setdefault(len(Cx), Cx)422 abelian = all(_mul(u, v, p) == _mul(v, u, p) for Cx in reps.values() for u in Cx for v in Cx)423 ok &= len(els) == p * (p * p - 1) and abelian and orders == {2 * p, p - 1, p + 1}424 det.append(f"p={p}: centralisers {sorted(orders)}, flat radius {_flat_radius(3, 2 * p)}")425 ok &= _flat_radius(3, 2 * 1373) == 12426 # the three bounds of a Subject shell p = 4k+1 inside the laboratory Carrier, read on the roots (no power above Omega is formed)427 Om = 2408561428 c2 = isqrt(Om); c3 = 0429 while (c3 + 1) ** 3 <= Om: c3 += 1430 c4 = max(q for q in range(1, 100) if q ** 4 < Om)431 shells = [p for p in range(5, 1600, 4) if arith.is_prime(p)]432 bounds = (max(p for p in shells if p <= c4), max(p for p in shells if p <= c3), max(p for p in shells if p * p < Om))433 ok &= (c2, c3, c4) == (1551, 134, 39) and bounds == (37, 113, 1549) and all(p > c3 for p in (157, 233, 641, 1373))434 det.append(f"laboratory bounds: nesting p ≤ {bounds[0]}, variety p ≤ {bounds[1]}, plane p ≤ {bounds[2]}")435 R.check("K2", "the frame variety: on SL₂(𝔽₅), SL₂(𝔽₇), SL₂(𝔽₁₃) (exhaustive) every centraliser of a non-central element is abelian "436 "of order 2p, p − 1 or p + 1, so every abelian subgroup has order at most 2p and a chart with commuting generators is "437 "ℤ³-flat to radius 1, 1, 2 — and 12 on the Subject shell 1373 against p = 1373; a Subject shell inside the laboratory "438 "Carrier has three bounds, read on the roots 39, 134, 1551 of Ω: nesting p ≤ 37, frame variety p ≤ 113 (SL₂'s elements are "439 "frame moves, not registrations), plane p ≤ 1549 — the shells 157, 233, 641, 1373 lie above the cube root", ok, "; ".join(det))440 # K3 exhaustive on SL_2(F_5): no triple of generators gives the radius-2 ball of Z^3441 p = 5; els = _sl2(p); I = (1, 0, 0, 1)442 def invariants(gens):443 G = list(gens) + [_inv(g, p) for g in gens]444 dist = {I: 0}; frontier = [I]; layers = [1]445 for r in (1, 2, 3):446 nxt = []447 for x in frontier:448 for g in G:449 y = _mul(x, g, p)450 if y not in dist: dist[y] = r; nxt.append(y)451 layers.append(len(nxt)); frontier = nxt452 L1 = [x for x in dist if dist[x] == 1]; L2 = [x for x in dist if dist[x] == 2]453 back = sorted(sum(1 for g in G if dist.get(_mul(x, g, p)) == 1) for x in L2)454 n4 = 0455 for i in range(len(L1)):456 for j in range(i + 1, len(L1)):457 Nu = {_mul(L1[i], g, p) for g in G}; Nv = {_mul(L1[j], g, p) for g in G}458 n4 += len((Nu & Nv) - {I})459 return layers, n4, back460 z3back = sorted([1] * 6 + [2] * 12); total = 0; matches = 0461 cand = [x for x in els if x != I and x != _inv(x, p)]462 for trip in itertools.combinations(cand, 3):463 if any(_inv(trip[i], p) == trip[j] for i in range(3) for j in range(3) if i != j): continue464 G = list(trip) + [_inv(g, p) for g in trip]465 if len(set(G)) != 6: continue466 total += 1467 layers, n4, back = invariants(trip)468 if layers[:3] == [1, 6, 18] and n4 == 12 and back == z3back: matches += 1469 R.check("K3", "SL₂(𝔽₅), exhaustive over every generator triple of degree 6: no Cayley ball of radius 2 carries the invariants of "470 "ℤ³'s (layers 1, 6, 18; twelve 4-cycles through the identity; back-degrees 1 ×6, 2 ×12) — the frame space of the smallest "471 "shell carries no locally three-dimensional homogeneous chart", total == 260072 and matches == 0,472 f"{total} triples, {matches} matches")473474# ------------------------------------------------------------------------------------------------------------475# block M: the ringdown of the exponential reading (00:E14; master T5 ill-posed under Q20, reports/daily-push/t5-push-20261016.md)476# the one wave operator of the chart is the wave equation with the all-orders index e^{2u}; its eikonal pair Ω_c = λ = 1/(2eM) and its ℓ = 2 mode by WKB3477@R.block("M", BLOCKS["M"])478def block_M():479 """Block M — the ringdown (CHART): M1–M2. The floats live in frc/chart_gravity.ringdown_table; this file reads them as Fractions."""480 T = CG.ringdown_table()481 tol = Fraction(1, 10 ** 9)482 # 00:E14 (p00201)483 ok = near(T["r_c"], 2, abs_=tol) and near(T["omega_c"], T["closed"], rel=tol) and near(T["lambda"], T["closed"], rel=tol)484 ok &= near(T["h1"], 0, abs_=tol) and near(T["h2"], T["h2_closed"], rel=tol)485 ok &= Fraction("0.9557") < Fraction(T["ratio"]) < Fraction("0.9558")486 R.check("M1", "the eikonal pair of the exponential reading [chart]: the potential e^{−4u}/r² along the tortoise coordinate peaks at "487 "r_c = 2M, where the impact function h = r²e^{4u} has h′ = 0 and h″ = 2e²; the orbital rate √V₀ and the Lyapunov rate "488 "√(−V₂/2V₀) both equal 1/(2eM) to 10⁻⁹ (b_c = 2eM), and the ratio to Schwarzschild's pair 1/(3√3 M) is 3√3/(2e), between "489 "0.9557 and 0.9558: the −4.4 % on frequency and damping alike", ok,490 f"r_c = {T['r_c']:.9f}, Ω_c = {T['omega_c']:.9f}, λ = {T['lambda']:.9f}, 1/(2e) = {T['closed']:.9f}, h″ = {T['h2']:.6f}", kind="CHART")491 # M2 the ℓ = 2 mode and the (2,2,0) exposure492 ok = Fraction(T["control_error"]) < Fraction(1, 1000) and Fraction(T["mode_error"]) < Fraction(1, 1000) and Fraction(T["rw_error"]) < Fraction(2, 1000)493 ok &= Fraction("1.007") < Fraction(T["mode_over_eikonal"]) < Fraction("1.009")494 sh, hw = T["shifts"], T["half_widths"]495 ok &= Fraction("0.241") < Fraction(sh["phase"]) < Fraction("0.243") and Fraction("-0.078") < Fraction(sh["rw"]) < Fraction("-0.076")496 ok &= Fraction(11) < Fraction(hw["phase"]) < Fraction("11.2") and Fraction("-3.3") < Fraction(hw["eikonal"]) < Fraction("-3.1")497 ok &= Fraction("-4.9") < Fraction(hw["rw"]) < Fraction("-4.8")498 R.check("M2", "the ℓ = 2 mode of the chart's wave operator [chart]: third-order WKB along the tortoise coordinate reproduces Leaver's "499 "Schwarzschild scalar and axial ℓ = 2 modes [import] to 10⁻³ and gives 0.4636 − 0.0924i (in 1/M) on the exponential "500 "reading, within 10⁻³ of the time-domain value 0.464149 − 0.092253i, 0.8 % above the eikonal (ℓ + ½)/(2eM); the "501 "Regge–Wheeler-type coupling [import] gives 0.3454 − 0.0866i, within 2 × 10⁻³ of 0.344778 − 0.085086i. Against Kerr's "502 "(2,2,0) = 0.373672 [import] the three numbers are +24.2 %, −4.4 % (the eikonal ratio) and −7.7 %, and GW250114's "503 "δf̂₂₂₀ = 0.02 ± 0.02 [data] excludes them by 11, 3.2 and 4.9 half-widths", ok,504 f"controls {T['controls'][0]:.5f}, {T['controls'][2]:.5f}; mode {T['mode']:.5f}; RW {T['rw']:.5f}; half-widths "505 + ", ".join(f"{k} {v:+.1f}" for k, v in hw.items()), kind="CHART")506507if __name__ == "__main__":508 blocks = [a for a in sys.argv[1:] if a in R.blocks]509 if blocks:510 for b in blocks: R.run_block(b)511 sys.exit(0 if R.summary(write=False) else 1)512 sys.exit(0 if R.verify_all() else 1)513