corrected_in_CODATA_3sigma
plain-language theorem explainer
The Pass-2 corrected inverse fine-structure constant lies strictly inside the CODATA ±3σ window. Anyone checking that the additive closure of the symbolic RS α⁻¹ formula is observationally admissible cites this. The proof rewrites the corrected value to the CODATA anchor and discharges both inequalities by numeric normalization on the external bounds.
Claim. The corrected inverse fine-structure constant satisfies $\underline{\alpha^{-1}} < \alpha^{-1}_{\mathrm{corr}} < \overline{\alpha^{-1}}$, where the endpoints are the external CODATA $\pm 3\sigma$ bounds on $\alpha^{-1}$.
background
Alpha Resolution Pass 2 turns the residual between the symbolic RS formula for $\alpha^{-1}$ and the laboratory anchor into an explicit additive closure target. It does not yet derive a new geometric correction; it defines the exact shift needed to hit the CODATA value and checks that the shifted number sits in the accepted band.
The external anchors fix $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$ (CODATA 2022) and a surrounding $\pm 3\sigma$ interval alpha_inv_bounds. The sibling alphaInv_corrected is the RS base value plus the required additive mismatch; alphaInv_corrected_eq_CODATA asserts that this corrected quantity equals the CODATA anchor exactly.
In the broader RS picture the fine-structure target is the narrow band $\alpha^{-1}\in(137.030,137.039)$. This lemma is the verification-layer check that the Pass-2 closure lands inside the laboratory window used as that external constraint.
proof idea
One short tactic proof. Rewrite the goal with alphaInv_corrected_eq_CODATA, replacing the corrected RS value by the numeric CODATA anchor. Split the conjunction and discharge each strict inequality by norm_num against the concrete lower/upper fields of alpha_inv_bounds and the CODATA constant. No geometric or forcing lemmas are invoked; the content is pure numeric comparison after the equality rewrite.
why it matters
This is the observational admissibility check for Pass 2: after the exact additive correction that maps the symbolic RS $\alpha^{-1}$ onto the CODATA anchor, the result is certified inside the $\pm 3\sigma$ laboratory band. The module frames that correction as a formal target for a future first-principles derivation from RS geometry (curvature-space or related forcing), not as a derived geometric term itself.
In the framework landmarks this sits at the $\alpha$ band constraint $\alpha^{-1}\in(137.030,137.039)$. Sibling results (deltaAlphaInv_required, deltaAlphaInv_geometric_eq_required, corrected_residual_zero, exists_unique_exact_alignment_closure) pin the size and uniqueness of the additive shift; this theorem only certifies band membership after that shift. No downstream consumers are wired yet; it is a leaf verification fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.