alphaInv_corrected
plain-language theorem explainer
The corrected inverse fine-structure constant is the RS symbolic α⁻¹ plus an explicit additive geometric closure term. Verification and CODATA-alignment proofs cite this quantity as the closed target value. It is a one-line sum of the canonical RS expression and the geometric delta.
Claim. Define the corrected inverse fine-structure constant by $\alpha^{-1}_{\mathrm{corr}} := \alpha^{-1}_{\mathrm{RS}} + \delta_{\mathrm{geom}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the canonical RS exponential-resummation expression and $\delta_{\mathrm{geom}}$ is the additive geometric closure term that maps that expression onto the CODATA anchor.
background
Alpha Resolution Pass 2 turns the residual mismatch between the Recognition Science symbolic α⁻¹ and the CODATA anchor into an explicit additive closure target. The module does not yet derive a new geometric correction from first principles; it names the exact shift required and proves that the shifted value sits on the CODATA point and inside the ±3σ band.
The base quantity is the dimensionless inverse fine-structure constant from Constants.Alpha: the assembled exponential resummation (seed times exp of a gap term), reported near 137.04 with nothing fit to CODATA. The infrared CODATA value is treated as a boundary condition. The sibling geometric delta is the unique additive correction that forces exact alignment.
In RS-native units the fine-structure band is the familiar (137.030, 137.039) window; this definition supplies the closed symbolic object against which that band is checked.
proof idea
Pure definition: the corrected value is the sum of the canonical RS inverse fine-structure expression and the geometric closure term. No tactics or lemmas are required at the definition site; downstream equalities unfold this sum and cancel against the CODATA anchor by construction of the geometric delta.
why it matters
This is the closed α⁻¹ object that every Pass-2 alignment theorem quotes. It feeds the exact CODATA equality, the zero residual, the ±3σ band membership, the uniqueness of any additive closure that hits CODATA, the existence-uniqueness of that closure, and the aggregate closure-status report.
In the broader framework it sits on the verification side of the α problem: the RS formula (seeded exponential resummation, related to the PRC form 44π exp(−w₈ ln φ/(44π))) is left intact, and the missing geometric piece is isolated as an explicit target for future first-principles derivation from RS geometry (curvature/power-family work in the same module). Until that derivation lands, this definition is the formal bridge between the symbolic RS value and the experimental anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.