corrected_residual_zero
plain-language theorem explainer
After the geometric additive correction is applied, the residual between the corrected inverse fine-structure constant and the CODATA 2022 anchor is exactly zero. Anyone checking that Pass 2 closes the α⁻¹ mismatch to machine equality will cite this. The proof is a one-step rewrite by the construction equality, followed by ring.
Claim. The corrected inverse fine-structure constant equals the CODATA anchor with zero residual: $\alpha^{-1}_{\mathrm{corr}} - \alpha^{-1}_{\mathrm{CODATA}} = 0$.
background
Alpha Resolution Pass 2 does not yet derive a new geometric correction from first principles. It defines the exact additive shift needed to map the current symbolic RS formula for $\alpha^{-1}$ onto the external CODATA 2022 anchor $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$, and proves that the corrected value sits exactly on that anchor (and inside the $\pm 3\sigma$ band).
The corrected value is $\alpha^{-1}{\mathrm{corr}} := \alpha^{-1} + \Delta\alpha^{-1}{\mathrm{geom}}$, where $\Delta\alpha^{-1}{\mathrm{geom}}$ is the explicit closure term. Upstream, alphaInv_corrected_eq_CODATA already records that this construction forces $\alpha^{-1}{\mathrm{corr}} = \alpha^{-1}_{\mathrm{CODATA}}$ exactly. The residual form here is the same fact rewritten as a vanishing difference, which is the natural target for later first-principles derivation of the correction from RS geometry (curvature / hinge structure).
proof idea
One-line algebraic closure. Rewrite the residual with the upstream equality $\alpha^{-1}{\mathrm{corr}} = \alpha^{-1}{\mathrm{CODATA}}$, then apply ring to obtain $0$. No new arithmetic or bounds are introduced.
why it matters
In the Recognition framework the inverse fine-structure constant is constrained to a narrow band near $137.03$–$137.04$. Pass 2 isolates the residual mismatch between the present symbolic RS expression and CODATA as an explicit additive target. This theorem states that, once that target correction is installed, the residual is identically zero, so the corrected value is not merely inside the CODATA band but pinned to the anchor.
No downstream consumers are wired yet (used_by is empty). The module’s stated purpose is to hand a formal closure target to future geometry: derive $\Delta\alpha^{-1}_{\mathrm{geom}}$ (or an equivalent) from RS structure rather than by fitting. Sibling results already give uniqueness of the additive alignment and membership in the $\pm 3\sigma$ band; the zero residual is the sharpest form of exact alignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.