alphaInv_deviation_approx
plain-language theorem explainer
The RS center for α⁻¹ sits about 0.0015 below the CODATA 2022 central value, and the absolute deviation is strictly less than 0.002. Anyone checking the fine-structure comparison in the quarantined PDG module would cite this bound. The proof unfolds the center and CODATA constants and discharges both inequalities by numerical normalization.
Claim. Let $\delta = \alpha^{-1}_{\mathrm{RS,center}} - \alpha^{-1}_{\mathrm{CODATA\,2022}}$, where the RS center is the midpoint of the interval $(137.030, 137.039)$ and the CODATA central value is $137.035999177$. Then $\delta < 0$ and $|\delta| < 0.002$.
background
The module Verification.PDGComparison is quarantined from the certified surface: it imports experimental CODATA/PDG numbers and reports informational comparisons, not steps of the forcing chain. Its headline check is that the machine-verified RS band $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$ contains the CODATA 2022 value $\alpha^{-1} = 137.035999177(21)$.
Local constants fix the endpoints alphaInv_RS_lo = 137.030 and alphaInv_RS_hi = 137.039, so the RS center is their arithmetic mean $137.0345$. The deviation is defined as that center minus the CODATA central value. The primer band for $\alpha^{-1}$ is exactly this interval $(137.030, 137.039)$.
Upstream, the CODATA constant and the lo/hi/center defs are pure numerical abbreviations; no analytic derivation of $\alpha$ is invoked here.
proof idea
Term-mode proof by unfolding. Expand the deviation, the RS center, the lo/hi endpoints, and the CODATA constant into concrete rationals. Split the conjunction: the first goal $\delta < 0$ is closed by norm_num; the second rewrites $|\delta|$ via abs_of_neg (again justified by norm_num) and finishes with norm_num. No external lemmas beyond the local defs are required.
why it matters
This pins the signed offset of the RS $\alpha^{-1}$ midpoint relative to CODATA: RS sits slightly low by roughly $1.5 \times 10^{-3}$, well inside a $0.002$ envelope. It supports the module's key claim that the RS interval contains experiment, and it quantifies how centered that containment is.
In the broader framework the $\alpha^{-1}$ band is a landmark prediction (primer: $\alpha^{-1}$ inside $(137.030, 137.039)$). The result is informational only: the module is explicitly quarantined because experimental inputs are not derived from the T0–T8 forcing chain. No downstream theorems currently depend on it; it is a verification report entry rather than a link in the certified proof graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.