The ledger file py/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, and of the dilation rigidity theorem of block C: the rows2the gravity theme proves (ledger migration, task LM27, 6 October 2026; C21 bound 20 October 2026, BLOCK = "CE").34The master's block E is bound by this file (the gravity theme), and C21, the dilation rigidity theorem, whose character5clauses the theme's Theme/Drift.lean proves (the master's witnesses, group C). It binds E1, the uniqueness lemma, E3, the linear6layer, E4, the nonlinear completion, E5, the floor's faces, E6, the horizon count, E7, the horizon triple, and E10, the7fold, E12, the chart count beside the declared chart E11, and E14, the eikonal pair and the phase mode beside the declared wave8operator 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 conjoins9(PROOFS; the realisations E4 and E5 carry a key for their exact clauses, G08 as amended on 12 October 2026), the shells, and10the checks, which call the gravity theme11(frc/gravity.py, frc/drift.py, frc/lattice.py) and, for the chart faces of E5 and the ringdown of E14, the chart theme12(frc/chart_gravity.py; those checks are CHART, and E14's key conjoins Mathlib theorems, CHART below). Each check names the rows it decides13or corroborates (LEDGER), under a `# 00:E6 (p00176)` marker on the check that decides the row (PREDICATES). The Lean side14is lean/FrcCore/Theme/Gravity.lean, Theme/Drift.lean, Theme/Symbol.lean and Theme/Shift.lean, the key file15lean/FrcCore/Keys/Gravity.lean and the certificate lean/FrcCore/Ledgers/Master/Gravity.lean.1617 python3 -m frc.ledgers.master.gravity every block, the census; exit 1 if a check fails18 python3 -m frc.ledgers.master.gravity W one block (W or U)1920Blocks: N the uniqueness lemma: the Maxwell and Fierz–Pauli lines by the symbol method EXACT (00:E1)21 L the linear layer: the Gauss law, the Green's function's sign, the single arrow EXACT (00:E3)22 C the completion: the character, no self-source, the cover triangle, the PN series EXACT (00:E4)23 F the floor's faces: the operational cut, the slip core's content, the dragging EXACT, CHART (00:E5)24 W the horizon count: the registration sphere, the record, the merger law EXACT (00:E6)25 U the horizon triple: the record on the rate face, the response, Smarr EXACT (00:E7)26 P the fold: the two branches, the cut current, the fold return EXACT (00:E10)27 K the chart count: the balls of Z^d against the Ω residues, the Subject shell's three bounds EXACT (00:E12)28 M the ringdown: the eikonal pair, the ℓ = 2 mode of the chart's wave operator, the (2,2,0) exposure CHART (00:E14)29 R the dilation rigidity theorem: the character, the PPN defect, the cover halving the angle EXACT, CHART (00:C21)3031The notebook frc/ledgers/master/gravity.ipynb runs one row per cell, the cell's id its key (gate G13).32"""33import sys34from fractions import Fraction3536import random3738from frc import arith39from frc import chart as C40from frc import chart_gravity as CG41from frc import drift as D42from frc.foundation import drive43from frc import lattice as LT44from frc.registry import Registry45from frc.gravity import (squares, conic_points, sphere_points, sphere_brute, record, area, rate_mass, temperature,46 response, merger_area)4748# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----49BLOCK = "CE"50KEYS = {"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", "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 blocks: its label and its accession key51LEAN = {"C21": "core", "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 them52# ---- end of the generated table ----5354# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys55# 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.56PROOFS = {57 "E1": ["FRC.Symbol.maxwell_unique", "FRC.Symbol.fierz_pauli_unique", "FRC.Symbol.vec_invariant", "FRC.Symbol.fierz_pauli_invariant"],58 "E3": ["FRC.Drift.gauss_law", "FRC.Symbol.fierz_pauli_unique", "FRC.Drift.conj_pow", "FRC.Drift.conj_branch"],59 "E4": ["FRC.Drift.gauss_law", "FRC.Drift.character_composition", "FRC.Drift.character_unique", "FRC.Drift.cover_triangle",60 "FRC.Drift.cover_deviation", "FRC.Drift.pn_coefficients"], # a realisation's key proves its exact clauses (G08 as amended on 12 October 2026)61 "E5": ["FRC.Drift.compression", "FRC.Cycle.cyc_add_n", "FRC.Drift.cut_ordering"],62 "E6": ["FRC.Grav.sphere_area", "FRC.Grav.sphere_area_rung", "FRC.Grav.count_identity", "FRC.Grav.merger_area"],63 "E7": ["FRC.Grav.count_identity", "FRC.Grav.record_mass", "FRC.Grav.record_response", "FRC.Grav.temperature_rate",64 "FRC.Grav.smarr", "FRC.Grav.record_response_rate"],65 "E10": ["FRC.Drift.fold_return", "FRC.Drift.fold_collision", "FRC.Drift.cut_area_monotone", "FRC.Drift.cut_ordering",66 "FRC.Cycle.cyc_add_n"],67 "E12": ["FRC.Grav.chart_plane_overflows", "FRC.Grav.chart_space_overflows", "FRC.Grav.chart_line_fits",68 "FRC.Grav.chart_lab_instance"], # the chart count beside the declared chart E11 (master T1 ill-posed, 15 October 2026)69 "C21": ["FRC.Drift.character_composition", "FRC.Drift.character_unique", "FRC.Drift.ppn_defect", "FRC.Drift.ppn_no_character",70 "FRC.Subject.horizon_generator"], # the dilation rigidity theorem: the character and its uniqueness, the PPN defect 4ab, the cover's horizon station (20 October 2026)71}72# The Mathlib theorems of E14's key (lean/FrcMathlib/Theme/Strong.lean): the eikonal pair of the exponential reading and the73# shadow–ringdown bracket; the row's ℓ = 2 mode is the chart check M2 (master T5 ill-posed, 16 October 2026).74CHART = {75 "E14": ["FRC.Strong.eikonal_pair", "FRC.Strong.shadow_bracket"],76}7778LEAN_ONLY = () # the rows with a Lean declaration and no python check (gate G12): none7980SWEEP = 200 # the sphere sweep runs over every prime p = 4κ + 1 below it81BRUTE = [5, 13, 17, 29, 37] # the shells enumerated point by point82IDENT = 10000 # the identities run over every prime p = 4κ + 1 below it83MERGER = (27811, 1596) # the merger instance of 21-gravity and 37-sim8485LEDGER = {"N1": "00:E1", "N2": "00:E1", "L1": "00:E3", "L2": "00:E3", "C1": "00:E4", "C2": "00:E4", "F1": "00:E5", "F2": "00:E5",86 "W1": "00:E6", "W2": "00:E6", "W3": "00:E6", "U1": "00:E7", "U2": "00:E7", "P1": "00:E10", "P2": "00:E10",87 "K1": "00:E12", "K2": "00:E12", "K3": "00:E12", "M1": "00:E14", "M2": "00:E14",88 "R1": "00:C21", "R2": "00:C21", "R3": "00:C21"}89BLOCKS = {"N": "the uniqueness lemma: the Maxwell and Fierz–Pauli lines by the symbol method",90 "L": "the linear layer: the Gauss law, the Green's function's sign, the single arrow",91 "C": "the completion: the character, no self-source, the cover triangle, the PN series",92 "F": "the floor's faces: the operational cut, the slip core's content, the dragging",93 "W": "the horizon count: the registration sphere, the record, the merger law",94 "U": "the horizon triple: the record on the rate face, the response, Smarr",95 "P": "the fold: the two branches, the cut current, the fold return",96 "K": "the chart count: the balls of Z^d against the Ω residues, the Subject shell's three bounds",97 "M": "the ringdown: the eikonal pair, the ℓ = 2 mode of the chart's wave operator, the (2,2,0) exposure",98 "R": "the dilation rigidity theorem: the character, the PPN defect, the cover halving the angle"}99PREDICATES = {"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",100 "00:C21": "R1"}101102R = Registry("00", "gravity", LEDGER, PREDICATES, sources=[__file__])103104105def _shells(lo, hi):106 return [n for n in range(lo, hi) if n % 4 == 1 and arith.is_prime(n)]107108109def near(x, y, rel=None, abs_=None):110 """|x − y| within the stated tolerance, the chart's float x read as a Fraction against rational bounds."""111 d = abs(Fraction(x) - Fraction(y))112 return (rel is not None and d <= Fraction(rel) * abs(Fraction(y))) or (abs_ is not None and d <= Fraction(abs_))113114115# ------------------------------------------------------------------------------------------------------------116# block N: the uniqueness lemma (00:E1)117# in every gauge sector the gauge-invariant adjacency-local quadratic action is one line: spin 1 the Maxwell line118# a₁ + a₂ = 0, the symbol of F², and spin 2 the Fierz–Pauli line (−1, 2, −2, 1), the nullspace of the gauge variation at119# random rational symbols (Symbol.lean: vec_invariant, maxwell_unique, fierz_pauli_invariant, fierz_pauli_unique); the120# discrete Fierz–Pauli functional on ℤ_N⁴ is invariant under the gauge shift with central differences and not with121# one-sided ones. The quadratic sector of Tr F² is the Maxwell line in every colour component; the non-abelian completion122# is 27-fields' (27:C2). The same functions decide 21:C9 (checks B1, B2 of frc/ledgers/p21_gravity.py).123@R.block("N", BLOCKS["N"])124def block_N():125 """Block N — the uniqueness lemma (EXACT): N1–N2."""126 # 00:E1 (p00052)127 lines = [LT.fierz_pauli_line(samples=k) for k in (12, 16)]128 ok = all(l[0] and l[1] for l in lines)129 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)130 ok &= not LT.fp_gauge_invariant(3, 4, seed=7, kind="forward")131 ns1, ns2 = lines[0][2], lines[0][3]132 R.check("N1", "the uniqueness lemma: by the symbol method over ℚ (the gauge variation at 12 and 16 random rational symbols in "133 "Minkowski signature) the gauge-invariant quadratic forms are one line in each sector — spin 1 the Maxwell line a₁ + a₂ = 0, "134 "the symbol of F², and spin 2 the Fierz–Pauli line (−1, 2, −2, 1), the symbol of the linearised Einstein–Hilbert action; "135 "the discrete Fierz–Pauli functional on ℤ₃⁴ (two seeds) and ℤ₄⁴ with random integer fields is invariant under the gauge "136 "shift h ↦ h + Dξ + (Dξ)ᵀ for central differences and fails for one-sided ones (the control); the quadratic sector of "137 "Tr F² is the Maxwell line in every colour component", ok,138 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")139 # N2 the lines do not depend on the dimension: d = 3, 5 (the lemma is dimension-free and metric-free)140 ok = True; det = []141 for d in (3, 5):142 n1 = LT.symbol_nullspace(1, samples=12, d=d, seed=9); n2 = LT.symbol_nullspace(2, samples=14, d=d, seed=9)143 fp = [Fraction(-1), Fraction(2), Fraction(-2), Fraction(1)]144 ok &= len(n1) == 1 and n1[0][0] + n1[0][1] == 0145 ok &= len(n2) == 1 and all(n2[0][i] * fp[0] == n2[0][0] * fp[i] for i in range(4))146 det.append(f"d={d}: spin-1 {len(n1)} line, spin-2 {len(n2)} line")147 R.check("N2", "the same two lines in dimensions 3 and 5 at fresh random symbols: the uniqueness lemma reads the symbol alone, "148 "in every dimension", ok, "; ".join(det))149150151# ------------------------------------------------------------------------------------------------------------152# block L: the linear layer (00:E3)153# the Coulomb law as the lattice Green's function: the Gauss law (the flux through a region's boundary equals the154# enclosed divergence, Drift.lean: gauss_law) and the exact Green's function of the Dirichlet grid, entrywise positive,155# so the pair energy's cross term lowers the energy exactly for like signs; the single arrow: the time-reversed clock is156# the Frobenius branch, the conjugate orbit of the drive (Drift.lean: conj_pow, conj_branch). The same functions decide157# 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.158@R.block("L", BLOCKS["L"])159def block_L():160 """Block L — the linear layer (EXACT): L1–L2."""161 # 00:E3 (p00154)162 rng = random.Random(154)163 gauss = True164 for _ in range(20):165 m = rng.randint(4, 12)166 J = [[0] * m for _ in range(m)]167 for x in range(m):168 for y in range(x + 1, m):169 v = rng.randint(-5, 5); J[x][y], J[y][x] = v, -v170 gauss &= D.gauss_law(J, {x for x in range(m) if rng.randrange(2) == 0})171 signs = [D.pair_energy_sign(k) for k in (3, 4)]172 arrows = [D.single_arrow(p, nu) for p, nu in ((13, 2), (17, 3), (37, 2))]173 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))))174 R.check("L1", "the Coulomb law as the lattice Green's function: on 20 random graphs with antisymmetric integer link currents the "175 "divergence over a random region equals the flux through its boundary (the Gauss law); over ℚ the Green's function of the "176 "Dirichlet grids 3³ and 4³ is entrywise positive, so the pair energy's cross term −m₁m₂G_ab lowers the energy exactly for "177 "like signs; the single arrow: on 𝔽_{p²}, p = 13, 17, 37, the Frobenius is the conjugation, the conjugate orbit of the "178 "norm-one circle's generator is its orbit reversed, and the conjugation is no translation of the circle (it fixes ±1 alone)",179 ok, f"G_ab = {signs[0][1]} (3³), {signs[1][1]} (4³); circles of order {[a[1] for a in arrows]}")180 # L2 the cross term's sign is the product of the source signs, on the 3³ grid181 ok, Gab, Gaa = D.pair_energy_sign(3)182 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 "183 "positive for (1, −1), (2, −3), (−1, 1); G_ab = 5/5712 at the opposite corners", ok, f"G_ab = {Gab}, G_aa = {Gaa}")184185186# ------------------------------------------------------------------------------------------------------------187# block C: the nonlinear completion (00:E4)188# the exponential reading is the character and the unique function with the composition law (Drift.lean:189# character_composition, character_unique); what gravitates is transfer, antisymmetric link currents whose diagonal is190# zero, so a region's divergence is its boundary flux and the static potential of a source is harmonic off the source,191# the field of two sources their sum (gauss_law); the cover triangle 2γ − β = 1, γ = 1 forces β = 1 (cover_triangle,192# cover_deviation); the exponential metric against the isotropic Schwarzschild form, β = γ = 1 and the classical tests193# exact through first order (pn_coefficients). The same functions decide 21:C11, C25, C7, C8 (checks C4, C5, D1).194@R.block("C", BLOCKS["C"])195def block_C():196 """Block C — the nonlinear completion (EXACT): C1–C2."""197 # 00:E4 (p00055)198 ok = all(D.exponential_reading(p) for p in (13, 17, 29))199 rng = random.Random(55)200 for _ in range(20):201 m = rng.randint(4, 12)202 J = [[0] * m for _ in range(m)]203 for x in range(m):204 for y in range(x + 1, m):205 v = rng.randint(-5, 5); J[x][y], J[y][x] = v, -v206 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})207 ok &= D.cover_triangle(Fraction(1), Fraction(1)) and not D.cover_triangle(Fraction(1), Fraction(2))208 pn = D.pn_coefficients(6)209 ok &= pn["ok"] and pn["beta"] == 1 and pn["gamma"] == 1 and Fraction(2 + 2 * pn["gamma"] - pn["beta"], 3) == 1210 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)211 R.check("C1", "the nonlinear completion: on 𝔽₁₃, 𝔽₁₇, 𝔽₂₉ every nonzero residue composes, c^(a+b) = c^a c^b below the full cycle, "212 "and a function with the composition law is rebuilt from f(1) alone as c^a — the exponential reading is the character, "213 "the unique scale-covariant one; on 20 random graphs the link currents are antisymmetric with zero diagonal (no self-link), "214 "and the divergence over a random region equals its boundary flux; the cover triangle 2γ − β = 1 with γ = 1 forces "215 "β = 1 and a second β fails it; the exponential metric read against the isotropic Schwarzschild form gives β = γ = 1, "216 "the perihelion factor (2 + 2γ − β)/3 = 1, and deviations δA = U³/6, δB = U²/2 and nothing lower: the classical tests exact",217 ok, f"β = {pn['beta']}, γ = {pn['gamma']}, δA = {[str(x) for x in pn['dA'][:5]]}, δB = {[str(x) for x in pn['dB'][:4]]}")218 # C2 the static potential is harmonic off its source and sources superpose: the exact Dirichlet potential219 okc, currents = LT.cut_current(2)220 R.check("C2", "the static potential of a unit source on the Dirichlet box {−2..2}³, solved exactly over ℚ, is harmonic off the "221 "source: the flux through the cut of every graph ball r = 0, 1, 2 is the enclosed charge 1 — the potential sources nothing "222 "of its own, and the field of two sources is the sum (the system is linear)", okc,223 f"currents {[str(c) for c in currents]} on the areas 6, 30, 78")224225226# ------------------------------------------------------------------------------------------------------------227# block F: the floor's faces (00:E5)228# the operational cut r_f = r_s/ln Ω between the slip core and the mass in the chart's own numbers (Drift.lean:229# cut_ordering); the slip core's content confined by the drive, the compression identity and the finite order of the230# shift (compression, Shift.lean: cyc_add_n); the floor's coupling m²/Ω on Ω = s². The chart faces (CHART): the exact231# profile horizonless, the round trip e^{2u(r_f)} = Ω, the preferred-frame scale 1/√Ω, the dragging at the Lense–Thirring232# value. The same functions decide 21:X3, X8, C12, C10, C17, P2 (checks C13, A6, E5, E7, E13 of the paper's ledger file).233@R.block("F", BLOCKS["F"])234def block_F():235 """Block F — the floor's faces (EXACT, CHART): F1–F2."""236 # 00:E5 (p00056)237 high, thr = D.cut_ordering(C.LN_OMEGA, 10 ** 6)238 low, _ = D.cut_ordering(C.LN_OMEGA, 100)239 ok = high and not low and thr == Fraction("321489") / 16240 returns = [D.offset_return(n, sec) for n, sec in ((8, {1, 2, 3}), (12, {0, 5, 6, 7, 11}), (9, {4}))]241 ok &= all(r[0] and r[1] == n for r, (n, _) in zip(returns, ((8, 0), (12, 0), (9, 0))))242 ok &= all(D.compression_identity(n, sec) for n, sec in ((8, {1, 2, 3}), (9, {4})))243 ok &= all(D.dilution(m, s) for m in (1, 3, 1000) for s in (5, 1552, 10 ** 61))244 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 "245 "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 "246 "(the threshold (ln Ω/2)² = 20 093.06); on the cycles ℤ₈, ℤ₁₂, ℤ₉ with a sector the drive's step splits the sector's "247 "weight into what stays and what leaks to the offset sector, conserves the whole, and returns it after n steps — the "248 "slip core's content is confined, nothing lost; the floor's coupling of two masses m is (m/√Ω)² = m²/Ω exactly on Ω = s²",249 ok, f"threshold {thr}; orders {[r[1] for r in returns]}")250 # F2 the chart faces251 u0, floor_rate, bound, low_rate = CG.horizonless()252 cut = CG.operational_cut(10 ** 6)253 scale = CG.preferred_frame_scale()254 drag = CG.dragging_field(J=Fraction(3, 10), r=10)255 ok = Fraction(u0) < Fraction(bound) and Fraction(floor_rate) > 0 and near(low_rate, floor_rate, rel=Fraction(1, 10 ** 9))256 ok &= cut["ordered"] and near(cut["round_trip"], CG.OMEGA, rel=Fraction(1, 10 ** 6))257 ok &= near(scale, Fraction("2.74e-62"), rel=Fraction(1, 100)) and Fraction(scale) < Fraction(1, 10 ** 61)258 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))259 R.check("F2", "the floor's chart faces [chart]: the exact profile is horizonless, u(0) = 2.622 Gm finite below π r_* and the "260 "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)} = Ω; "261 "the preferred-frame scale is the floor 1/√Ω = 2.7 × 10⁻⁶² at ln Ω = 283.5, far below every bound; the gravitomagnetic "262 "dipole's curl is 2J/r³ on the axis, the Lense–Thirring rate, and −J/r³ on the equator", ok,263 f"u(0) = {u0:.4f}, 1/√Ω = {scale:.3e}, axis {drag['axis']:.4e}", kind="CHART")264265266# ------------------------------------------------------------------------------------------------------------267# block W: the horizon count (00:E6)268# the registration sphere x² + y² + z² = κ² has p(p + 1) points, at every nonzero square rung; the record S = κ(p + 1)269# with 4S + 1 = p² and S/A = κ/p; the merger law ΔA = 2 M₁ M₂ on A = M(M + 1) (Gravity.lean: sphere_area,270# sphere_area_rung, count_identity, merger_area).271@R.block("W", BLOCKS["W"])272def block_W():273 """Block W — the horizon count (EXACT): W1–W3."""274 # 00:E6 (p00176)275 bad = []276 for p in _shells(5, SWEEP):277 k = (p - 1) // 4278 r = squares(p)279 ok = sphere_points(p, k * k % p) == area(p)280 ok &= all(sphere_points(p, a) == p * p + p * (r[a] - 1) for a in range(1, p)) # p² + p χ(a), χ(a) = r[a] − 1281 ok &= all(conic_points(p, c) == (p - 1 if c else 2 * p - 1) for c in range(p))282 S, A = record(p), area(p)283 ok &= 4 * S + 1 == p * p and Fraction(S, A) == Fraction(k, p) and 4 * S * p == A * (p - 1)284 if not ok: bad.append(p)285 mbad = [(a, b) for a in range(1, 120) for b in range(1, 120) if merger_area(a, b) != 2 * a * b]286 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 "287 "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 "288 "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) "289 "for all M₁, M₂ < 120", not bad and not mbad,290 f"{len(_shells(5, SWEEP))} shells; exceptions {bad} {mbad[:2]}")291 # W2 a second method: the spheres enumerated point by point292 bad = [p for p in BRUTE if sphere_brute(p, ((p - 1) // 4) ** 2) != area(p)]293 R.check("W2", f"the shells {', '.join(map(str, BRUTE))} enumerated point by point: the sphere at the capacity has p(p + 1) "294 "points (30 at p = 5, the rate 30/125 = 6/25 of 37-sim)", not bad and temperature(5) == Fraction(6, 25),295 f"exceptions {bad}")296 # W3 the record law closes at the coherence horizon: S = (Ω − 1)/4 at Ω = p²; the merger instance297 bad = [p for p in _shells(5, IDENT) if (p * p - 1) % 4 or (p * p - 1) // 4 != record(p)]298 m1, m2 = MERGER299 ok = not bad and merger_area(m1, m2) == 88772712 == 2 * m1 * m2300 R.check("W3", f"every prime p = 4κ + 1 below {IDENT}: at Ω = p² the record S = κ(p + 1) is (Ω − 1)/4; the merger "301 "27 811 + 1 596 → 29 407 gives ΔA = 88 772 712 = 2 · 27 811 · 1 596", ok, f"exceptions {bad}")302303304# ------------------------------------------------------------------------------------------------------------305# block U: the horizon triple (00:E7)306# 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); Smarr307# 2 T_resp S = M(1 − 1/p) and 2 T S = M(1 − 1/p²) (Gravity.lean: count_identity, record_mass, record_response,308# temperature_rate, smarr).309@R.block("U", BLOCKS["U"])310def block_U():311 """Block U — the horizon triple (EXACT): U1–U2."""312 # 00:E7 (p00058)313 bad = []314 for p in _shells(5, IDENT):315 S, A, M, T, Tr = record(p), area(p), rate_mass(p), temperature(p), response(p)316 Sf = lambda m: m * (m - 1)317 ok = Fraction(S) == Fraction(A, 4) * (1 - Fraction(1, p)) and S == M * (M - 1)318 ok &= Fraction(Sf(M + 3) - Sf(M - 3), 6) == p and Sf(M + 1) - Sf(M) == p + 1 # dS/dM = 2M − 1 = p319 ok &= T == Fraction(p + 1, p * p) and Tr == Fraction(1, p) and T == Tr * (1 + Fraction(1, p))320 ok &= 2 * Tr * S == M * (1 - Fraction(1, p)) and 2 * T * S == M * (1 - Fraction(1, p * p))321 if not ok: bad.append(p)322 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 "323 "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) "324 "and 2 T S = M(1 − 1/p²), in exact fractions", not bad, f"{len(_shells(5, IDENT))} shells; exceptions {bad}")325 # U2 the Subjects 13, 173, 1373: the values326 det = []327 for p in (13, 173, 1373):328 det.append(f"p={p}: S={record(p)}, M={rate_mass(p)}, T={temperature(p)}")329 ok = record(13) == 42 == rate_mass(13) * (rate_mass(13) - 1) and temperature(13) == Fraction(14, 169)330 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",331 ok, "; ".join(det))332333334# ------------------------------------------------------------------------------------------------------------335# block P: the fold (00:E10)336# the two chart branches are two Carrier data: on a frame the residue products r₁g^Δ, r₂ coincide at exactly one lift,337# the pairs never (Drift.lean: fold_collision); the cut area of the graph balls of ℤ³ is 6(2r² + 2r + 1) and grows at every338# step, so the cut current Q/A_r of the enclosed charge recovers r (cut_area_monotone, the exact Dirichlet potential); the339# fold return through an interior chart is the bare return term by term, its period sum the uniform floor and the full340# period the identity (fold_return, Shift.lean: cyc_add_n); the cut ordered in the substrate coordinate (cut_ordering).341# The DFT fold of the paper's toy (21:P7, check C10) is one interior chart among all.342@R.block("P", BLOCKS["P"])343def block_P():344 """Block P — the fold (EXACT): P1–P2."""345 # 00:E10 (p00147)346 gens = {p: arith.primitive_root(p) for p in (13, 17, 29)}347 coll = {p: D.fold_collision(p, g) for p, g in gens.items()}348 ok = all(c[0] and c[1] == (p - 1) * (p - 2) for p, c in coll.items())349 areas = [LT.ball_cut_area(r) for r in range(7)]350 ok &= all(c == f for c, f in areas) and all(areas[i][0] < areas[i + 1][0] for i in range(6))351 ok &= all(areas[r + 1][1] == areas[r][1] + 24 * (r + 1) for r in range(6))352 okc, currents = LT.cut_current(2)353 ok &= okc and currents == [Fraction(1, 6), Fraction(1, 30), Fraction(1, 78)]354 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)355 ok &= D.cut_ordering(C.LN_OMEGA, 10 ** 6)[0]356 R.check("P1", "the fold is a chart projection: on 𝔽₁₃, 𝔽₁₇, 𝔽₂₉ (exhaustive) every ordered pair of distinct nonzero positions "357 "has exactly one lift Δ with r₁g^Δ = r₂ — the residue product collides, the pair (r, g^{−Δ}) never; the cut area of the "358 "graph balls of ℤ³, counted, is 6(2r² + 2r + 1) for r ≤ 6, growing by 24(r + 1) at each step, and the exact Dirichlet "359 "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 "360 "chains C₈, C₉, C₁₀ over 𝔽₁₇, 𝔽₁₃, 𝔽₂₉ with a random invertible interior chart (and the paper's DFT fold) the exterior "361 "return through the fold equals the bare return term by term, the period sum is the all-ones block on the exterior and the "362 "full period is the identity; the cut is ordered, r_* < r_f < M, at M = 10⁶", ok,363 "; ".join(f"p={p}: {c[1]} pairs" for p, c in coll.items()) + f"; areas {[a[0] for a in areas]}")364 # P2 the paper's instance: the period-averaged exterior return through the DFT fold is the uniform floor operator365 ok = D.fold_return(17, 8, 4) and D.fold_return(13, 12, 4) and D.fold_return(29, 8, 4)366 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 "367 "period-averaged exterior return P_E F Uⁿ F⁻¹ P_E is the uniform floor operator, every nonzero entry equal — no prompt "368 "echo structure", ok, "")369370371# ------------------------------------------------------------------------------------------------------------372# block K: the chart count (00:E12; master T1 ill-posed under Q20, reports/daily-push/t1-push-20261015.md)373# 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,374# (4R^3+6R^2+8R+3)/3 cells; at the horizon radius R = floor(sqrt Omega) on the Omega residues the planar and spatial375# balls overflow and the linear one fits (Gravity.lean: chart_plane_overflows, chart_space_overflows, chart_line_fits,376# chart_lab_instance). A Subject shell p inside Omega has three bounds, read on the roots: nesting p^4 < Omega (00:B8),377# the frame variety p^3 <= Omega (SL_2's elements are frame moves, not registrations: C22), the plane p^2 < Omega (A4).378# On SL_2(F_p) commuting generators lie in an abelian subgroup of order at most 2p (the centralisers of the non-central379# elements, exhaustive on 5, 7, 13), and on SL_2(F_5) no triple of generators reproduces the radius-2 ball of Z^3380# (exhaustive). No count above Omega is formed.381def _ball(d, R):382 if d == 1: return 2 * R + 1383 if d == 2: return 2 * R * R + 2 * R + 1384 n = 4 * R ** 3 + 6 * R ** 2 + 8 * R + 3385 return n // 3386387def _flat_radius(d, N):388 R = 0389 while _ball(d, R + 1) <= N: R += 1390 return R391392def _sl2(p):393 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]394395def _mul(x, y, p):396 a, b, c, d = x; e, f, g, h = y397 return ((a * e + b * g) % p, (a * f + b * h) % p, (c * e + d * g) % p, (c * f + d * h) % p)398399def _inv(x, p):400 a, b, c, d = x401 return (d % p, (-b) % p, (-c) % p, a % p)402403@R.block("K", BLOCKS["K"])404def block_K():405 """Block K — the chart count (EXACT): K1–K3."""406 import itertools407 from math import isqrt408 # 00:E12 (p00199)409 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)410 ok = all(_ball(d, r) == brute(d, r) for d in (1, 2, 3) for r in range(0, 7))411 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))412 shells = [13, 17, 29, 37, 157, 233, 641, 1373, 30089, 2408561]413 r3 = {Om: _flat_radius(3, Om) for Om in shells}414 ok &= r3[2408561] == 121 and _ball(3, 122) == 2451225 and isqrt(2408561) == 1551 and _flat_radius(2, 2408561) == 1096415 ok &= all(3 * r3[Om] <= isqrt(Om) for Om in shells if Om >= 157)416 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 "417 "horizon radius R = ⌊√Ω⌋ the planar and spatial balls hold more than Ω cells and the linear ball fits, for every Ω in "418 "[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, "419 "at most ⌊√Ω⌋/3 from 157 on, 121 against 1551 on the laboratory Carrier (the planar radius 1096)", ok,420 "; ".join(f"{Om}: R3 {r3[Om]}, sqrt {isqrt(Om)}" for Om in shells))421 # K2 the frame space: abelian subgroups of SL_2(F_p) have order <= 2p; the commuting-chart radius422 ok = True; det = []423 for p in (5, 7, 13):424 els = _sl2(p); I = (1, 0, 0, 1); mI = (p - 1, 0, 0, p - 1)425 orders = set(); reps = {}426 for x in els:427 if x in (I, mI): continue428 Cx = [y for y in els if _mul(x, y, p) == _mul(y, x, p)]429 orders.add(len(Cx)); reps.setdefault(len(Cx), Cx)430 abelian = all(_mul(u, v, p) == _mul(v, u, p) for Cx in reps.values() for u in Cx for v in Cx)431 ok &= len(els) == p * (p * p - 1) and abelian and orders == {2 * p, p - 1, p + 1}432 det.append(f"p={p}: centralisers {sorted(orders)}, flat radius {_flat_radius(3, 2 * p)}")433 ok &= _flat_radius(3, 2 * 1373) == 12434 # the three bounds of a Subject shell p = 4k+1 inside the laboratory Carrier, read on the roots (no power above Omega is formed)435 Om = 2408561436 c2 = isqrt(Om); c3 = 0437 while (c3 + 1) ** 3 <= Om: c3 += 1438 c4 = max(q for q in range(1, 100) if q ** 4 < Om)439 shells = [p for p in range(5, 1600, 4) if arith.is_prime(p)]440 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))441 ok &= (c2, c3, c4) == (1551, 134, 39) and bounds == (37, 113, 1549) and all(p > c3 for p in (157, 233, 641, 1373))442 det.append(f"laboratory bounds: nesting p ≤ {bounds[0]}, variety p ≤ {bounds[1]}, plane p ≤ {bounds[2]}")443 R.check("K2", "the frame variety: on SL₂(𝔽₅), SL₂(𝔽₇), SL₂(𝔽₁₃) (exhaustive) every centraliser of a non-central element is abelian "444 "of order 2p, p − 1 or p + 1, so every abelian subgroup has order at most 2p and a chart with commuting generators is "445 "ℤ³-flat to radius 1, 1, 2 — and 12 on the Subject shell 1373 against p = 1373; a Subject shell inside the laboratory "446 "Carrier has three bounds, read on the roots 39, 134, 1551 of Ω: nesting p ≤ 37, frame variety p ≤ 113 (SL₂'s elements are "447 "frame moves, not registrations), plane p ≤ 1549 — the shells 157, 233, 641, 1373 lie above the cube root", ok, "; ".join(det))448 # K3 exhaustive on SL_2(F_5): no triple of generators gives the radius-2 ball of Z^3449 p = 5; els = _sl2(p); I = (1, 0, 0, 1)450 def invariants(gens):451 G = list(gens) + [_inv(g, p) for g in gens]452 dist = {I: 0}; frontier = [I]; layers = [1]453 for r in (1, 2, 3):454 nxt = []455 for x in frontier:456 for g in G:457 y = _mul(x, g, p)458 if y not in dist: dist[y] = r; nxt.append(y)459 layers.append(len(nxt)); frontier = nxt460 L1 = [x for x in dist if dist[x] == 1]; L2 = [x for x in dist if dist[x] == 2]461 back = sorted(sum(1 for g in G if dist.get(_mul(x, g, p)) == 1) for x in L2)462 n4 = 0463 for i in range(len(L1)):464 for j in range(i + 1, len(L1)):465 Nu = {_mul(L1[i], g, p) for g in G}; Nv = {_mul(L1[j], g, p) for g in G}466 n4 += len((Nu & Nv) - {I})467 return layers, n4, back468 z3back = sorted([1] * 6 + [2] * 12); total = 0; matches = 0469 cand = [x for x in els if x != I and x != _inv(x, p)]470 for trip in itertools.combinations(cand, 3):471 if any(_inv(trip[i], p) == trip[j] for i in range(3) for j in range(3) if i != j): continue472 G = list(trip) + [_inv(g, p) for g in trip]473 if len(set(G)) != 6: continue474 total += 1475 layers, n4, back = invariants(trip)476 if layers[:3] == [1, 6, 18] and n4 == 12 and back == z3back: matches += 1477 R.check("K3", "SL₂(𝔽₅), exhaustive over every generator triple of degree 6: no Cayley ball of radius 2 carries the invariants of "478 "ℤ³'s (layers 1, 6, 18; twelve 4-cycles through the identity; back-degrees 1 ×6, 2 ×12) — the frame space of the smallest "479 "shell carries no locally three-dimensional homogeneous chart", total == 260072 and matches == 0,480 f"{total} triples, {matches} matches")481482# ------------------------------------------------------------------------------------------------------------483# block M: the ringdown of the exponential reading (00:E14; master T5 ill-posed under Q20, reports/daily-push/t5-push-20261016.md)484# 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 WKB3485@R.block("M", BLOCKS["M"])486def block_M():487 """Block M — the ringdown (CHART): M1–M2. The floats live in frc/chart_gravity.ringdown_table; this file reads them as Fractions."""488 T = CG.ringdown_table()489 tol = Fraction(1, 10 ** 9)490 # 00:E14 (p00201)491 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)492 ok &= near(T["h1"], 0, abs_=tol) and near(T["h2"], T["h2_closed"], rel=tol)493 ok &= Fraction("0.9557") < Fraction(T["ratio"]) < Fraction("0.9558")494 R.check("M1", "the eikonal pair of the exponential reading [chart]: the potential e^{−4u}/r² along the tortoise coordinate peaks at "495 "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 "496 "√(−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 "497 "0.9557 and 0.9558: the −4.4 % on frequency and damping alike", ok,498 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")499 # M2 the ℓ = 2 mode and the (2,2,0) exposure500 ok = Fraction(T["control_error"]) < Fraction(1, 1000) and Fraction(T["mode_error"]) < Fraction(1, 1000) and Fraction(T["rw_error"]) < Fraction(2, 1000)501 ok &= Fraction("1.007") < Fraction(T["mode_over_eikonal"]) < Fraction("1.009")502 sh, hw = T["shifts"], T["half_widths"]503 ok &= Fraction("0.241") < Fraction(sh["phase"]) < Fraction("0.243") and Fraction("-0.078") < Fraction(sh["rw"]) < Fraction("-0.076")504 ok &= Fraction(11) < Fraction(hw["phase"]) < Fraction("11.2") and Fraction("-3.3") < Fraction(hw["eikonal"]) < Fraction("-3.1")505 ok &= Fraction("-4.9") < Fraction(hw["rw"]) < Fraction("-4.8")506 R.check("M2", "the ℓ = 2 mode of the chart's wave operator [chart]: third-order WKB along the tortoise coordinate reproduces Leaver's "507 "Schwarzschild scalar and axial ℓ = 2 modes [import] to 10⁻³ and gives 0.4636 − 0.0924i (in 1/M) on the exponential "508 "reading, within 10⁻³ of the time-domain value 0.464149 − 0.092253i, 0.8 % above the eikonal (ℓ + ½)/(2eM); the "509 "Regge–Wheeler-type coupling [import] gives 0.3454 − 0.0866i, within 2 × 10⁻³ of 0.344778 − 0.085086i. Against Kerr's "510 "(2,2,0) = 0.373672 [import] the three numbers are +24.2 %, −4.4 % (the eikonal ratio) and −7.7 %, and GW250114's "511 "δf̂₂₂₀ = 0.02 ± 0.02 [data] excludes them by 11, 3.2 and 4.9 half-widths", ok,512 f"controls {T['controls'][0]:.5f}, {T['controls'][2]:.5f}; mode {T['mode']:.5f}; RW {T['rw']:.5f}; half-widths "513 + ", ".join(f"{k} {v:+.1f}" for k, v in hw.items()), kind="CHART")514515# ------------------------------------------------------------------------------------------------------------516# block R: the dilation rigidity theorem (00:C21)517# static clock comparison is the register character g^{−Δn}; characters compose exactly and a function with the composition518# law is the character of its first value (Drift.lean character_composition, character_unique: zero coefficient freedom);519# the PPN temporal form admits no register character — its transitivity defect is exactly 4ab (ppn_defect, ppn_no_character);520# the spinor cover halves the angle at every tick and reaches the horizon station −1 at (p + 1)/2 base ticks521# (Subject.lean horizon_generator) — the corpus script check_c21.py reproduced record for record.522@R.block("R", BLOCKS["R"])523def block_R():524 """Block R — the dilation rigidity theorem: R1 the character and the PPN form on the shells (EXACT), R2 the continuum chart (CHART), R3 the cover (EXACT)."""525 # 00:C21 (p00041)526 chan = {q: D.quarter_channel(q, drive(q)) for q in (13, 29, 173)}527 channel = all(v[0] == 4 and v[2] and v[3] and v[4] for v in chan.values())528 compose = D.exponential_reading(13)529 ppn = D.ppn_no_character(13) == [(1, 0)] and D.ppn_no_character(173) == [(1, 0)] and D.ppn_defect(13) and D.ppn_defect(173, trials=2000)530 R.check("R1", "the dilation rigidity theorem on the register: the Q₄ channel at the three instances 13, 29, 173 — gcd(p − 1, 2(p + 1)) = 4, "531 "the quarter i = g^{−κ} has i² = −1 and N(i) = i^{p+1} = −1 with (p + 1)/2 odd; on 𝔽₁₃ every nonzero c composes exactly over "532 "the full cycle, c^{a+b} = c^a c^b, and a function with the composition law and f(0) = 1 is the character of f(1) "533 "(zero coefficient freedom); the PPN/Schwarzschild temporal form admits no register character: over every c and u₁ of 𝔽₁₃ and "534 "𝔽₁₇₃ the only character matching 1 − 2nu₁ through n = 2 is the trivial u₁ = 0, and the transitivity defect "535 "(1 − 2a)(1 − 2b) − (1 − 2(a + b)) is 4ab on every pair of 𝔽₁₃ and on 2 000 random pairs of 𝔽₁₇₃",536 channel and compose and ppn, f"channel {dict((q, (v[0], v[1])) for q, v in chan.items())}; PPN solutions {D.ppn_no_character(13)}")537 # R2 the continuum chart: the functional equation's regular solution is e^{−s}, the GR form's defect 4ab, in exact rationals538 c, efac, law, defect = D.composition_series(6)539 R.check("R2", "[chart] the continuum reading: the regular solution of R(a + b) = R(a)R(b), R(s) = 1 − s + c₂s² + …, solved coefficientwise "540 "in exact rationals, is e^{−s} through order 6 (cₙ = (−1)ⁿ/n!), the composition law holding identically through total order 6; "541 "the GR form √(1 − 2s) read at first order, 1 − s·2, violates the law by exactly +4ab at second order — the strong-field "542 "dilation law is the exponential reading alone", c == efac and law and defect == {(1, 1): Fraction(4)},543 f"coefficients {[str(x) for x in c]}; defect {dict((k, str(v)) for k, v in defect.items())}", kind="CHART")544 # R3 the two-face cover at all orders, exhaustive on C_{2(p+1)} ⊂ 𝔽_{p²} at p = 13 and 173545 cov = {q: D.spinor_cover(q, arith.nonresidue(q)) for q in (13, 173)}546 R.check("R3", "the cover halves the angle at every tick (C20): in 𝔽_{p²} a generator w of the spinor cover C_{2(p+1)} has w^{2n} = (w²)ⁿ at "547 "every n < 2(p + 1), the cover's half w^{p+1} = −1, and the base generator w² reaches the horizon station −1 at exactly "548 "(p + 1)/2 ticks (finitely many, not asymptotic; the base quarter (p + 1)/4 is no lattice point), exhaustively at p = 13 (28 ticks) "549 "and p = 173 (348 ticks)", all(all(v) for v in cov.values()), f"{cov}")550551552if __name__ == "__main__":553 blocks = [a for a in sys.argv[1:] if a in R.blocks]554 if blocks:555 for b in blocks: R.run_block(b)556 sys.exit(0 if R.summary(write=False) else 1)557 sys.exit(0 if R.verify_all() else 1)558