alphaInv_RS_contains_CODATA
plain-language theorem explainer
The Recognition Science prediction band for the inverse fine-structure constant strictly contains the CODATA 2022 central value. Metrologists and RS auditors cite this as the headline α⁻¹ consistency check against experiment. The proof is a two-sided decimal comparison: unfold the three real constants and discharge both inequalities by norm_num.
Claim. The RS prediction interval for the inverse fine-structure constant satisfies $137.030 < 137.035999177 < 137.039$, so the CODATA 2022 central value of $\alpha^{-1}$ lies strictly inside the RS band $(137.030, 137.039)$.
background
Recognition Science predicts a fixed open interval for the inverse fine-structure constant: $137.030 < \alpha^{-1} < 137.039$ (primer band). In this verification module those edges are the real constants 137.030 and 137.039; the CODATA 2022 central value is the real constant 137.035999177 (uncertainty recorded separately as about $2.1\times 10^{-8}$).
The module is quarantined from the certified surface: it imports experimental numbers and performs informational numerical comparisons, not steps of the forcing chain. Upstream interval-width helpers exist in the recognition and spacetime layers, but the containment claim only needs the three decimal constants and strict inequality on $\mathbb{R}$.
proof idea
Split the conjunction with constructor. Left goal: unfold the RS lower edge and the CODATA central value, then norm_num to get $137.030 < 137.035999177$. Right goal: unfold the CODATA value and the RS upper edge, then norm_num to get $137.035999177 < 137.039$. No analytic lemmas; pure machine-checked decimal arithmetic.
why it matters
Headline consistency fact of the PDG/CODATA comparison module: the machine-verified RS band for $\alpha^{-1}$ contains the experimental central value. Downstream it feeds the module's alpha-inverse summary report string, which records the proven lower and upper edges for human audit. It directly supports the framework landmark that $\alpha^{-1}$ lies in $(137.030, 137.039)$. Containment here is informational only; it does not enter T0–T8, RCL, or the certified derivation of constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.