additive_closure_unique_for_exact_alignment
plain-language theorem explainer
Any real additive correction that takes the RS inverse fine-structure formula exactly onto the CODATA anchor must equal the canonical geometric closure term (CODATA minus the symbolic RS value). Verification and constants authors cite this when locking uniqueness of the α⁻¹ alignment target. The proof is a two-sided real-arithmetic argument: rearrange by linarith one way, and rewrite through the corrected-equals-CODATA identity the other.
Claim. For every real $\delta$, one has $\alpha^{-1}_{\mathrm{RS}} + \delta = \alpha^{-1}_{\mathrm{CODATA}}$ if and only if $\delta$ equals the geometric closure term $\delta_{\mathrm{geom}} := \alpha^{-1}_{\mathrm{CODATA}} - \alpha^{-1}_{\mathrm{RS}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the canonical seed-gap exponential formula and $\alpha^{-1}_{\mathrm{CODATA}}$ is the external CODATA 2022 anchor.
background
Alpha Resolution Pass 2 turns the residual between the symbolic RS 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 defines the exact additive term required for alignment and proves the corrected value hits CODATA exactly, giving a formal target for later derivation.
The RS side is alphaInv, the dimensionless inverse fine-structure expression built as seed times an exponential gap resummation (canonical value near 137.04, nothing fit to data). The external anchor is CODATA 2022, $\alpha^{-1} = 137.035999177$. The geometric closure term is written directly as CODATA minus that seed-gap expression, so the corrected value is definitionally RS formula plus that term.
Upstream, the corrected expression is proved equal to CODATA by unfolding. The present statement is the uniqueness half of that story: the additive shift that achieves exact alignment is forced.
proof idea
Biconditional via constructor.
Forward: from $\alpha^{-1}{\mathrm{RS}} + \delta = \mathrm{CODATA}$, rearrange by linarith to $\delta = \mathrm{CODATA} - \alpha^{-1}{\mathrm{RS}}$, then simpa against the definition of the geometric closure (and the simp form of alphaInv).
Reverse: substitute $\delta = \delta_{\mathrm{geom}}$ and rewrite $\alpha^{-1}{\mathrm{RS}} + \delta{\mathrm{geom}}$ as the corrected expression, then apply alphaInv_corrected_eq_CODATA (the by-construction identity that corrected equals CODATA).
why it matters
This is the uniqueness direction needed by exists_unique_exact_alignment_closure, which packages existence and uniqueness of an additive closure producing exact CODATA alignment. Downstream uses the reverse direction of this iff as the uniqueness witness after exhibiting the geometric term.
In the Recognition framework the inverse fine-structure constant sits in a narrow predicted band near 137.03–137.04; the symbolic RS formula is close but not definitionally equal to the CODATA boundary value. Pass 2 isolates the residual as a named geometric closure target rather than absorbing it into a fit. The module doc is explicit that first-principles derivation of this (or an equivalent) correction from RS geometry remains open; uniqueness of the additive form is the formal lock that makes that open target well-posed.
Anyone arguing that several distinct additive patches could all hit CODATA is blocked here: only one real $\delta$ works.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.