alphaInv_CODATA_2022_hi
plain-language theorem explainer
Defines the CODATA 2022 three-sigma upper edge on the inverse fine-structure constant: central value plus three times the reported uncertainty. Experimentalists and RS auditors use it as the hard ceiling when checking whether the RS α⁻¹ interval sits inside the CODATA band. The body is a pure real literal arithmetic definition, not a proved inequality.
Claim. Let $\alpha^{-1}_{\mathrm{CODATA},2022} = 137.035999177$ with one-sigma uncertainty $\sigma = 2.1\times 10^{-8}$. The three-sigma upper bound is $\alpha^{-1}_{\mathrm{hi}} := 137.035999177 + 3\sigma = 137.035999177 + 3\cdot 0.000000021$.
background
The module Verification.PDGComparison is quarantined from the certified RS surface: it imports external CODATA/PDG numbers and only reports informational containment checks. Its headline comparison is the inverse fine-structure constant. Recognition Science predicts a machine-verified open interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$, while CODATA 2022 quotes $\alpha^{-1} = 137.035999177(21)$ (Tiesinga et al., J. Phys. Chem. Ref. Data 50, 033105).
Sibling constants package that experimental datum: the central value, the one-sigma width, the three-sigma floor, and this three-sigma ceiling. Together they form a closed numerical window against which the RS lo/hi bounds are compared. No derivation from the forcing chain (T5 J-uniqueness, RCL, or the phi ladder) is claimed here; the number is an external anchor.
proof idea
There is no proof. The declaration is a def equal to the real expression $137.035999177 + 3 \cdot 0.000000021$, i.e. CODATA central value plus three reported standard deviations. Lean reduces it by ordinary real arithmetic on literals.
why it matters
In the RS framework the inverse fine-structure constant is one of the sharpest external checks: the primer band $\alpha^{-1}\in(137.030,137.039)$ must contain the CODATA point. This constant supplies the experimental upper edge of that check (central $+3\sigma$). The module doc records the status claim that the RS interval contains the experimental value. No downstream theorem currently depends on the symbol (used-by is empty); it exists so comparison lemmas or numerical reports can name a single frozen CODATA ceiling rather than inlining the arithmetic. It does not touch T0–T8, the eight-tick octave, or mass-ladder rungs; it is pure metrology scaffolding for verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.