exists_unique_exact_alignment_closure
plain-language theorem explainer
A unique real additive correction aligns the Recognition Science inverse fine-structure constant to the CODATA 2022 anchor. Verification and constants work cite this as the exact-alignment uniqueness certificate. The proof takes the geometric closure term as witness, gets existence from the corrected-equals-CODATA identity, and uniqueness from the additive-closure uniqueness lemma.
Claim. There exists a unique real $\delta$ such that $\alpha^{-1}_{\mathrm{RS}} + \delta = \alpha^{-1}_{\mathrm{CODATA}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the symbolic RS inverse fine-structure constant and $\alpha^{-1}_{\mathrm{CODATA}}$ is the CODATA 2022 external anchor $137.035999177$.
background
Alpha Resolution Pass 2 converts the residual between the RS symbolic $\alpha^{-1}$ 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 shift needed for alignment and proves the corrected value hits CODATA exactly, giving a formal target for later geometry.
The RS side is alphaInv, the dimensionless inverse fine-structure expression from the canonical exponential resummation (assembled value near $137.04$, nothing fit to CODATA). The external anchor is alpha_inv_CODATA $= 137.035999177$ (CODATA 2022). The geometric closure term deltaAlphaInv_geometric is the canonical additive shift; alphaInv_corrected is their sum.
Upstream, alphaInv_corrected_eq_CODATA states that the corrected value equals the anchor by construction, and additive_closure_unique_for_exact_alignment says any additive $\delta$ with $\alpha^{-1}{\mathrm{RS}}+\delta=\alpha^{-1}{\mathrm{CODATA}}$ must equal that geometric term.
proof idea
Term-mode existence-uniqueness package. The witness is the geometric closure term. Existence is discharged by rewriting through the corrected expression and applying the identity that the corrected value equals CODATA. Uniqueness is the forward direction of the additive-closure uniqueness lemma: any $\delta$ satisfying the alignment equation equals the geometric term. No new arithmetic; pure packaging of those two prior facts into $\exists!$.
why it matters
This is the existence-uniqueness half of the Pass 2 closure certificate. Downstream, closure_status conjoins geometric-term status, equality of geometric and required deltas, corrected-equals-CODATA, this unique-alignment statement, and the curvature-exponent force at $d=5$.
In the broader RS picture the primer band $\alpha^{-1}\in(137.030,137.039)$ is the living target; CODATA sits inside it, and the symbolic RS formula sits slightly off. Pass 2 freezes the exact additive residual so a future first-principles derivation (curvature space, channel-capacity corrections, or related geometry) has a sharp equality to hit rather than a soft band. The module doc is explicit: derive this correction, or an equivalent, from RS geometry. Until that derivation lands, this theorem is the formal lock that the residual is unique and the corrected value is exact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.