deltaAlphaInv_geometric_eq_required
plain-language theorem explainer
The geometric inverse-fine-structure closure correction equals the exact additive RS-versus-CODATA mismatch. Constants and verification authors cite it to collapse two writings of the same residual into one object. The proof is a one-line definitional simplification after unfolding the canonical RS α⁻¹ expression.
Claim. The geometric closure term $\alpha^{-1}_{\mathrm{CODATA}}-\alpha_{\mathrm{seed}}\,e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ equals the required mismatch $\alpha^{-1}_{\mathrm{CODATA}}-\alpha^{-1}_{\mathrm{RS}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the canonical seed-gap exponential.
background
Alpha Resolution Pass 2 turns the residual between the Recognition Science symbolic inverse fine-structure constant and the CODATA anchor into an explicit additive closure target. It does not yet derive a new geometric correction from first principles; it names the exact shift that would align the present RS formula with CODATA and records that the corrected value sits in the CODATA band.
The required mismatch is CODATA $\alpha^{-1}$ minus the RS $\alpha^{-1}$. The geometric form writes the same difference with the seed-gap exponential in place: $\alpha_{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$. Upstream, the canonical RS $\alpha^{-1}$ is defined exactly as that seed-gap expression (nothing fit to CODATA; the infrared CODATA value remains a boundary condition). The two closures therefore differ only by how the RS side is written.
proof idea
Term-mode proof by a single simp that unfolds the geometric closure, the required mismatch, and the canonical RS $\alpha^{-1}$. After those three unfolds, both sides are literally $\alpha^{-1}{\mathrm{CODATA}}-\alpha{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$, so equality is definitional.
why it matters
This equality is one conjunct in the module's closure-status theorem, which packages geometric derivation of the closure term, exact CODATA alignment of the corrected $\alpha^{-1}$, uniqueness of the additive shift, and the forced curvature exponent in the power family. It lets later statements treat the seed-gap writing and the abstract mismatch as interchangeable, so the formal target for a future first-principles derivation is unambiguous. In the broader RS picture the symbolic $\alpha^{-1}$ already sits near the accepted band $(\approx 137.03$–$137.04)$; the residual named here is the precise object any geometric correction must reproduce.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.