alphaInv_deviation
plain-language theorem explainer
Signed difference between the Recognition Science inverse fine-structure midpoint and the CODATA 2022 central value. Verification authors cite it when reporting how far the RS α⁻¹ center sits from experiment. Defined by direct subtraction of the two real constants already fixed in this module.
Claim. Define the deviation $\delta\alpha^{-1} := \alpha^{-1}_{\mathrm{RS,\,center}} - \alpha^{-1}_{\mathrm{CODATA\,2022}}$, where $\alpha^{-1}_{\mathrm{RS,\,center}}$ is the midpoint of the certified RS interval for the inverse fine-structure constant and $\alpha^{-1}_{\mathrm{CODATA\,2022}} = 137.035999177$.
background
This module is a quarantined verification layer: it imports experimental CODATA/PDG numbers and compares them to Recognition Science predictions, without feeding those numbers into the certified forcing chain. The headline comparison is the inverse fine-structure constant. RS supplies a machine-verified open interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$; CODATA 2022 reports the central value $137.035999177(21)$.
The RS center used here is the arithmetic midpoint of the certified RS bounds (documented as $137.0345$). The CODATA central value is the literal real $137.035999177$. Their difference is the natural signed residual for later numerical statements about agreement.
Framework context: the primer places $\alpha^{-1}$ inside the band $(137.030, 137.039)$. Containment of the experimental point inside that band is the module's key status claim; the residual defined here quantifies center-to-center offset inside that containment.
proof idea
Pure definition: subtract the CODATA 2022 central constant from the RS interval midpoint. No lemmas, no tactics, no rewriting. Downstream theorems unfold this name and discharge concrete inequalities by norm_num on the expanded reals.
why it matters
Gives a single named residual for the α⁻¹ center-to-center comparison that the module advertises as its key result. The immediate consumer is the theorem that the residual is negative and smaller than $0.002$ in absolute value (RS center slightly below CODATA, offset well under two parts in a thousand). That pins the informal claim "RS predicts slightly lower" to a machine-checked inequality.
In the broader framework this residual sits inside the primer's α band $(137.030, 137.039)$ and the module's containment statement that the CODATA point lies in the certified RS interval. It does not enter the T0–T8 forcing chain; it is informational verification only, consistent with the module's quarantined status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.