alphaInv_CODATA_2022_lo
plain-language theorem explainer
CODATA 2022 three-sigma lower edge on the inverse fine-structure constant: central value minus thrice the quoted uncertainty. Anyone checking whether the RS α⁻¹ band covers experiment cites this constant. It is a pure numeric definition, not a proved inequality.
Claim. The CODATA 2022 lower bound on $\alpha^{-1}$ at three standard deviations is $\alpha^{-1}_{\mathrm{lo}} := 137.035999177 - 3\times 0.000000021$.
background
The module Machine-Verified PDG Comparison holds experimental anchors (CODATA, PDG) next to Recognition Science predictions. It is quarantined from the certified surface: experimental inputs are not derived from RS, and the comparisons are informational only.
CODATA 2022 reports $\alpha^{-1}_{\mathrm{exp}} = 137.035999177(21)$. The sibling constants package the central value, the one-sigma uncertainty, and the three-sigma upper edge. This definition is the matching lower edge (central minus $3\sigma$).
RS itself predicts a machine-verified interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$ (primer alpha band). The comparison question is whether that interval contains the experimental window.
proof idea
Pure definition by arithmetic. No lemmas, no tactics: the real is the literal expression central value minus three times the CODATA standard uncertainty $2.1\times 10^{-8}$.
why it matters
Gives the lower fence of the experimental window against which the RS $\alpha^{-1}$ band is checked. The module doc states the key status claim: the RS interval contains the CODATA value. Together with the matching upper bound and the RS lo/hi siblings, this constant supports that containment check without entering the forcing chain (T0–T8) or the Recognition Composition Law. It is scaffolding for verification only, not a derivation of $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.