residual_bounds
plain-language theorem explainer
The residual between the first-order RS inverse fine-structure constant and the CODATA 2022 anchor lies strictly in (−0.006, 0.0031). Anyone comparing the Alpha Genesis certified value to experiment cites this band. The proof unfolds the residual, imports the certified interval bounds on α⁻¹, pins the CODATA constant by reflexivity, and closes both sides by linear arithmetic.
Claim. Let $\alpha^{-1}_{\mathrm{RS}}$ be the certified first-order inverse fine-structure constant and $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$ the CODATA 2022 external anchor. Their signed residual $r = \alpha^{-1}_{\mathrm{RS}} - \alpha^{-1}_{\mathrm{CODATA}}$ satisfies $-0.006 < r < 0.0031$.
background
This lives in the Alpha Genesis M4 quarantine module: the only Alpha Genesis file allowed to mention the measured value. M1–M3 derive the structural α pipeline blind to CODATA; M4 states the comparison and the open residual target.
The residual is the signed gap α⁻¹_RS − α⁻¹_CODATA. The external anchor is the CODATA 2022 central value 137.035999177. Upstream interval lemmas supply a certified open band on the RS first-order value (strict lower and upper bounds from the Numerics AlphaBounds layer). The framework target band for α⁻¹ is roughly (137.030, 137.039); the residual band here is the fine comparison of the certified display against the anchor.
Downstream siblings use this residual only as a measured offset: any second-order fix must enter as additional spectral load in the exponent (not an additive display patch), and exactly one closing load equates the dressed value to CODATA.
proof idea
Unfold the residual to α⁻¹_RS − α⁻¹_CODATA. Bring in the two certified strict inequalities on the RS value (alphaInv_gt, alphaInv_lt from Numerics). Identify the CODATA symbol with the concrete real 137.035999177 by reflexivity. Split the conjunction and, on each side, rewrite the anchor and finish with linarith against the imported bounds. Pure interval arithmetic; no structural content from M1–M3 is reopened.
why it matters
Item (1) of the M4 module contract: a proved, CODATA-touching certificate that the first-order genesis residual sits in (−0.006, 0.0031). It localizes the open Alpha Genesis target: after M1 forces the response form, any second-order term is additional spectral load, and there is a unique closing load that matches CODATA. The remaining work is to derive that one number from D=3 voxel seam geometry without ever reading CODATA.
If a blind seam derivation lands on the closing load (within tolerance), the α pipeline closes at experimental precision. If it lands elsewhere, the channel-budget bridge of M3 is falsified. The anti-epicycle rule forbids admitting candidates by numerical proximity alone. This theorem does not close that derivation; it only certifies how large the residual presently is. It sits inside the broader RS constant story (α⁻¹ band near 137.03–137.04) as the quarantine comparison step, not as a forcing-chain landmark (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.