alphaInv_CODATA_2022_sigma
plain-language theorem explainer
Records the CODATA 2022 one-sigma uncertainty on the inverse fine-structure constant as the real 2.1×10⁻⁸. Anyone building experimental comparison intervals against the RS α⁻¹ band cites this constant. It is a bare numeric definition, not a derived claim.
Claim. The CODATA 2022 one-standard-deviation uncertainty on $\alpha^{-1}$ is fixed as the real number $2.1 \times 10^{-8}$.
background
The module Machine-Verified PDG Comparison holds experimental anchors (CODATA, PDG) side by side with Recognition Science predictions. It is quarantined from the certified surface: experimental numbers are imported, not derived, and the comparisons are informational rather than part of the forcing chain.
The inverse fine-structure constant is the headline check. RS supplies a machine-verified open interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$. CODATA 2022 reports the experimental central value $137.035999177$ with a $1\sigma$ uncertainty of $21$ in the last digits, i.e. $2.1\times 10^{-8}$. Sibling constants package the central value and the $\pm 3\sigma$ window used for containment tests.
In RS-native units the fine-structure constant sits in the predicted band $(137.030, 137.039)$; this definition simply freezes the experimental error bar that those bounds are compared against.
proof idea
No proof. The declaration is a one-line real constant assignment equal to $0.000000021$, matching the CODATA 2022 $1\sigma$ figure quoted in the module header as $\alpha^{-1}_{\mathrm{exp}} = 137.035999177(21)$.
why it matters
Gives the experimental error bar that turns the CODATA central value into a comparison window against the RS $\alpha^{-1}$ interval. Together with the sibling central value and the derived lo/hi bounds, it supports the module's key status claim: the RS band contains the experimental number. That containment is the principal external check on the RS alpha prediction cited in the primer (alpha inverse inside $(137.030, 137.039)$). The constant itself is not on the T0–T8 forcing chain; it is verification scaffolding only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.