residual
plain-language theorem explainer
Signed gap between the first-order RS inverse fine-structure value and the CODATA 2022 anchor. Quarantine-only comparison quantity: M1–M3 never see the measured value. Downstream bounds, the unique closing-load equation, and higher-order precision hypotheses all quote this difference. Definition is a one-line subtraction of two named reals.
Claim. Define the signed residual $\mathrm{res} := \alpha^{-1}_{\mathrm{RS}} - \alpha^{-1}_{\mathrm{CODATA}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the first-order genesis assembly (canonical exponential resummation, nothing fit to data) and $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$ is the external 2022 anchor.
background
This module is the sole Alpha Genesis quarantine that may mention the measured inverse fine-structure constant. M1–M3 derive the structural value blind to CODATA; here the comparison is stated and the open second-order target is localized.
Upstream, alphaInv is the dimensionless RS assembly $\alpha_{\mathrm{seed}},e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ (seed $4\pi\cdot 11$), documented as the assembled construction near $137.04$ with no CODATA fit. The external anchor is the fixed real $137.035999177$ (CODATA 2022). Their difference is the residual that residual bounds and the closing-load uniqueness theorems act on.
The certified band later confines this residual to $(-0.006, 0.0031)$. Any second-order fix must enter as multiplicative spectral load in the exponent, not as an additive display patch.
proof idea
Pure definition: subtract the CODATA anchor from the first-order RS inverse-alpha real. No tactics, no lemmas. Sibling theorems unfold this name and feed interval bounds on the RS side plus reflexivity on the anchor literal.
why it matters
Pins the only CODATA-touching quantity in the Alpha Genesis stack, so the derivation modules stay measurement-blind. Feeds residual_bounds (certified open interval), corrected_at_closingLoad (dressed value equals the anchor at the unique load), and the uniqueness/iff package around closingLoad. Also appears in higher-order precision hypotheses and several LambdaRec cost identities that need the same gap language.
Framework role: localizes the open seam-geometry problem. Exactly one second-order load $\delta_2$ makes the dressed value match experiment; that load must be forced from D=3 voxel seam topology without referencing CODATA. Match within tolerance closes alpha at experimental precision; mismatch falsifies the channel-budget bridge. Anti-epicycle rule: numerical proximity alone never admits a candidate.
Sits inside the RS constants program (alpha band near $137.03$–$137.04$) as the explicit residual target, not as a fit parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.