alphaInv_RS_interval_width_eq
plain-language theorem explainer
The Recognition Science prediction band for the inverse fine-structure constant has exact width 0.009. Anyone quoting the RS α⁻¹ interval precision (about 66 ppm relative) cites this equality. The proof unfolds the width as hi minus lo and discharges the decimal arithmetic by norm_num.
Claim. The width of the Recognition Science prediction interval for $\alpha^{-1}$, defined as the difference between the upper endpoint $137.039$ and the lower endpoint $137.030$, equals $0.009$.
background
The module Machine-Verified PDG Comparison records rigorous numerical checks of Recognition Science outputs against PDG and CODATA data. It is quarantined from the certified surface: experimental inputs are not RS-derived, and the comparisons are informational rather than part of the forcing chain.
For $\alpha^{-1}$, RS supplies the open interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$, matching the primer band and the preregistered AlphaInv prediction record. The lower and upper endpoints are fixed real constants; their difference is the interval width used to report absolute and relative precision (doc-comment: about 66 ppm relative to the central value).
CODATA 2022 sits at $137.035999177(21)$ inside that band. This declaration only pins the arithmetic width, not containment or derivation of the endpoints.
proof idea
One-line tactic proof. Unfold the width definition (hi minus lo) together with the two endpoint constants $137.039$ and $137.030$, then apply norm_num to evaluate the decimal subtraction to $0.009$. No lemmas beyond the local defs are required.
why it matters
Pins the absolute precision figure attached to the RS $\alpha^{-1}$ band that the primer states as $\alpha^{-1}$ inside $(137.030, 137.039)$. Downstream prose and relative-precision remarks (interval width over central value $\approx 66$ ppm) rest on this equality. The module's key verification claim is that the same interval contains the CODATA 2022 value; the width equality is the companion arithmetic fact that makes the reported ppm figure machine-checked rather than hand-stated.
No parent theorems currently depend on it (used_by is empty). It does not touch T0–T8, RCL, or the mass ladder; it is a verification-layer constant identity supporting the quarantined PDG comparison narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.