alphaInv_CODATA_2022
plain-language theorem explainer
Pins the CODATA 2022 central value of the inverse fine-structure constant at 137.035999177. Downstream verification lemmas cite it as the experimental anchor when checking that the RS interval (137.030, 137.039) contains the measured α⁻¹ and when measuring deviation and relative precision. The body is a bare real literal; no proof work.
Claim. The CODATA 2022 central value of the inverse fine-structure constant is $\alpha^{-1}_{\mathrm{CODATA\,2022}} = 137.035999177$ (with $1\sigma$ uncertainty $2.1\times 10^{-8}$ reported separately).
background
The module Machine-Verified PDG Comparison is quarantined from the certified RS surface: it imports experimental numbers and runs informational numerical checks, not part of the forcing chain. Its headline comparison is the inverse fine-structure constant.
Recognition Science predicts a closed interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$ (machine-checked bounds). CODATA 2022 reports $\alpha^{-1} = 137.035999177(21)$ (Tiesinga et al., J. Phys. Chem. Ref. Data 50, 033105). This definition stores only the central value as a real constant for Lean arithmetic.
Sibling constants in the same file hold the $1\sigma$ uncertainty and the RS interval endpoints; relative-precision and containment statements divide or compare against this anchor.
proof idea
Definitional constant: the body is the decimal literal $137.035999177$ at type $\mathbb{R}$. No tactics, no lemmas. Downstream proofs unfold this name and discharge numeric goals with norm_num.
why it matters
Experimental reference point for every $\alpha^{-1}$ check in PDGComparison. Parent results include: containment of the CODATA center in the RS band ($\alpha^{-1}{\mathrm{RS,lo}} < \alpha^{-1}{\mathrm{CODATA}} < \alpha^{-1}_{\mathrm{RS,hi}}$); the signed deviation of the RS center from CODATA (about $-0.0015$); relative precision as interval width over this central value (claimed $< 100,\mathrm{ppm}$); and the preregistered measurement record that packages the same central value with $\sigma = 2.1\times 10^{-8}$.
In the broader framework this is the external benchmark against the RS native $\alpha^{-1}$ band cited in the primer (inside $(137.030, 137.039)$). It does not derive $\alpha$ from the forcing chain; it only freezes the CODATA number so containment and ppm claims are machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.