deltaAlphaInv_ppm
plain-language theorem explainer
Defines the signed relative size, in parts per million, of the additive α⁻¹ correction that aligns the current RS formula with the CODATA 2022 anchor. Anyone tracking the α⁻¹ closure target or reporting residual mismatch in ppm cites this scalar. It is a one-line normalization: one million times the required additive shift divided by the CODATA inverse fine-structure constant.
Claim. The signed relative correction is $\delta_{\mathrm{ppm}} := 10^6 \cdot \Delta_{\mathrm{req}} / \alpha^{-1}_{\mathrm{CODATA}}$, where $\Delta_{\mathrm{req}}$ is the exact additive shift that maps the current RS $\alpha^{-1}$ to the CODATA 2022 value $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$.
background
Alpha Resolution Pass 2 does not yet derive a new geometric correction. It packages the α⁻¹ discrepancy as an explicit additive closure target: the unique real shift that sends the present symbolic RS inverse fine-structure value onto the external CODATA 2022 anchor $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$, and then checks that the corrected value sits in the CODATA band.
The sibling quantity $\Delta_{\mathrm{req}}$ (required additive correction) is that exact shift. The present definition only rescales it into a signed parts-per-million figure relative to the CODATA anchor, which is the conventional reporting unit for fine-structure residuals.
Upstream, alpha_inv_CODATA is the fixed external anchor (with its 1σ uncertainty defined alongside). The module imports the RS α machinery and curvature-space derivation only to name the uncorrected RS value and the geometric candidates; this definition itself depends only on the required shift and the CODATA denominator.
proof idea
Pure definitional abbreviation: the body is the arithmetic expression $10^6 \cdot \Delta_{\mathrm{req}} / \alpha^{-1}{\mathrm{CODATA}}$. No tactics, no lemmas. Downstream equality to the direct RS-vs-CODATA mismatch form is then rfl once $\Delta{\mathrm{req}}$ is unfolded as $\alpha^{-1}{\mathrm{CODATA}} - \alpha^{-1}{\mathrm{RS}}$.
why it matters
Gives the human-readable ppm size of the Pass 2 closure target so residual and band checks can be stated in standard metrology language. The immediate consumer is the equality theorem that rewrites this ppm figure as $10^6(\alpha^{-1}{\mathrm{CODATA}} - \alpha^{-1}{\mathrm{RS}})/\alpha^{-1}_{\mathrm{CODATA}}$, after which corrected-residual-zero and CODATA-3σ membership are proved for the additively corrected value.
In the broader RS picture this sits under the α band target (primer: $\alpha^{-1}$ inside roughly $(137.030, 137.039)$): Pass 2 fixes the exact additive gap the geometry must eventually produce, without claiming that derivation yet. The module doc states the open task explicitly: derive this correction (or an equivalent) from RS geometry, so first-principles work has a sharp numeric objective rather than a floating discrepancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.