deltaAlphaInv_ppm_eq_mismatch
plain-language theorem explainer
The relative ppm shift aligning the RS inverse fine-structure value with the CODATA anchor equals one million times the fractional RS-versus-CODATA mismatch. Anyone tracking the α⁻¹ closure target in Alpha Resolution Pass 2 would cite this identity. The proof is pure definitional reflexivity after unfolding the ppm definition and the required additive correction.
Claim. The signed parts-per-million relative correction equals $10^{6}\cdot(\alpha^{-1}_{\mathrm{CODATA}}-\alpha^{-1}_{\mathrm{RS}})/\alpha^{-1}_{\mathrm{CODATA}}$, where $\alpha^{-1}_{\mathrm{RS}}$ is the canonical RS inverse fine-structure expression and $\alpha^{-1}_{\mathrm{CODATA}}$ is the CODATA 2022 external anchor.
background
Recognition Science assembles a dimensionless inverse fine-structure value from a seed times an exponential gap factor, producing a pure RS number near 137.04 with nothing fitted to experiment. CODATA 2022 anchors $\alpha^{-1}$ at 137.035999177. Alpha Resolution Pass 2 does not yet derive a geometric correction; it records the exact additive shift needed to map the symbolic RS formula onto that external anchor and proves the corrected value lands in the CODATA band.
The ppm quantity is that required additive correction, scaled by one million and normalized by the CODATA value. The residual is the signed RS-minus-CODATA difference. The present identity rewrites the ppm figure directly from the opposite mismatch (CODATA minus RS), so the two bookkeeping forms are interchangeable.
proof idea
One-line wrapper by reflexivity. The ppm shift is defined as one million times the required additive correction divided by the CODATA anchor; the required correction is definitionally CODATA minus the RS inverse fine-structure value. Unfolding both sides yields identical terms, so rfl closes the goal with no lemmas or arithmetic.
why it matters
Pass 2 turns the $\alpha^{-1}$ discrepancy into an explicit closure target for a future first-principles derivation from RS geometry. This identity is pure bookkeeping: it lets later statements about residual vanishing or CODATA-band membership cite either the ppm form or the raw fractional mismatch. It sits with the sibling results that prove uniqueness of the additive closure and exact post-correction alignment. Framework-wide, the infrared value 137.035999 remains an open boundary condition; the correction itself is still to be derived (curvature-space and channel-capacity imports mark candidate routes). The primer band $\alpha^{-1}\in(137.030,137.039)$ is the coarser target this exact-alignment work refines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.