deltaAlphaInv_required
plain-language theorem explainer
Exact additive residual between the CODATA 2022 inverse fine-structure constant and the Recognition Science symbolic α⁻¹. Cited by anyone measuring RS–CODATA α alignment or building a geometric closure term. Defined as a one-line difference of two named real constants; no geometric content is claimed here.
Claim. Define the required additive correction by $\delta_{\alpha^{-1}}^{\mathrm{req}} := \alpha^{-1}_{\mathrm{CODATA}} - \alpha^{-1}_{\mathrm{RS}}$, where $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$ is the CODATA 2022 external anchor and $\alpha^{-1}_{\mathrm{RS}}$ is the canonical RS dimensionless inverse fine-structure expression (seed times exponential gap resummation).
background
Alpha Resolution Pass 2 turns the RS–CODATA $\alpha^{-1}$ discrepancy into an explicit closure target. It does not yet derive a geometric correction; it records the exact additive shift that would map the current symbolic RS formula onto the CODATA anchor, and later proves the corrected value sits in the CODATA band.
The RS side is the assembled canonical expression $\alpha^{-1}{\mathrm{RS}} = \alpha{\mathrm{seed}},\mathrm{e}^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$, documented as the dimensionless inverse fine-structure constant from exponential resummation (value near $137.04$, nothing fit to CODATA). The seed $4\pi\cdot 11$ is an identification, not a derived coupling; the exact infrared value is treated as a boundary condition still open in the AlphaGenesis status notes.
The external side is the CODATA 2022 anchor $\alpha^{-1} = 137.035999177(21)$. Their difference is the formal residual this definition names.
proof idea
Definitional one-liner: subtract the RS symbolic $\alpha^{-1}$ from the CODATA anchor. No lemmas, tactics, or algebraic reduction; the body is literally the difference of those two constants.
why it matters
Gives the module its numerical closure target: the additive $\delta$ such that RS $\alpha^{-1}$ plus $\delta$ equals CODATA exactly. Downstream, the geometric closure expression is proved definitionally equal to this residual; the relative size in ppm is built from it; and the module-level closure status packages geometric equality, exact CODATA alignment, uniqueness of the additive shift, and the forced curvature exponent $d=5$.
In the broader framework this sits against the RS $\alpha^{-1}$ band $(137.030, 137.039)$ and the honest status that infrared $\alpha^{-1}(0)$ remains a boundary condition. The module doc frames the open task: derive this correction (or an equivalent) from RS geometry rather than leave it as an external mismatch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.