alphaInv_corrected_eq_CODATA
plain-language theorem explainer
The RS inverse fine-structure value, after adding the canonical geometric closure term, equals the CODATA 2022 anchor exactly. Verification and α-resolution work cite this as the exact-alignment identity. The proof unfolds the corrected definition and simplifies against the symbolic RS formula.
Claim. By construction, $\alpha^{-1}_{\mathrm{corr}} := \alpha^{-1}_{\mathrm{RS}} + \delta_{\mathrm{geom}}$ equals the CODATA 2022 anchor $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$ exactly.
background
Alpha Resolution Pass 2 converts the residual mismatch between the Recognition Science inverse fine-structure formula and the external CODATA anchor into an explicit additive closure target. It does not yet derive a new geometric term from first principles; it defines the exact correction needed so that the corrected value lands on the anchor, giving a formal target for later derivation.
The bare RS quantity $\alpha^{-1}{\mathrm{RS}}$ is the dimensionless expression alphaInv: the seed $4\pi\cdot 11$ times an exponential gap resummation, yielding a value near $137.04$ with nothing fitted to CODATA. The external anchor is the CODATA 2022 value $137.035999177$. The geometric closure term $\delta{\mathrm{geom}}$ is defined so that adding it to the RS formula produces the corrected value $\alpha^{-1}_{\mathrm{corr}}$.
Upstream, the honest status of alphaInv records that the exact infrared value is still an open boundary condition; this module isolates that gap as a named additive target rather than absorbing it into a fit.
proof idea
One-line definitional proof. Unfold the corrected value and the geometric closure term (so $\alpha^{-1}{\mathrm{corr}}$ becomes $\alpha^{-1}{\mathrm{RS}} + (\alpha^{-1}{\mathrm{CODATA}} - \alpha^{-1}{\mathrm{RS}})$), then simp with the definition of $\alpha^{-1}_{\mathrm{RS}}$ to cancel and obtain equality with the CODATA anchor. No external lemmas beyond the local definitions.
why it matters
This identity is the exact-alignment fact that the rest of Pass 2 hangs on. Downstream, corrected_residual_zero rewrites with it to get a zero residual; corrected_in_CODATA_3sigma rewrites with it and checks the $\pm 3\sigma$ band by norm_num; exists_unique_exact_alignment_closure uses it as the witness that a unique additive $\delta$ hits CODATA; additive_closure_unique_for_exact_alignment characterizes that $\delta$ as exactly the geometric term; and closure_status packages the equality into the module-level closure report.
In the broader framework it sits inside the $\alpha^{-1}$ band check (primer: $\alpha^{-1}$ inside $(137.030, 137.039)$) and makes precise the OPEN infrared boundary condition on the RS formula. The module doc is explicit: future work must derive this correction (or an equivalent) from RS geometry; the theorem only certifies that the named target does align exactly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.