alphaInv_RS_interval_width
plain-language theorem explainer
The RS inverse fine-structure prediction band has absolute width equal to its upper bound minus its lower bound. Anyone checking the Recognition Science α⁻¹ interval against CODATA cites this quantity as the raw precision of the forecast. The definition is the plain difference of the fixed endpoints 137.039 and 137.030.
Claim. The absolute width of the Recognition Science prediction interval for the inverse fine-structure constant is $W_{\mathrm{RS}} := 137.039 - 137.030$.
background
The module Machine-Verified PDG Comparison records rigorous numerical checks of Recognition Science forecasts against CODATA and PDG data. It is quarantined from the certified surface: experimental inputs are imported, not derived, so the comparisons are informational rather than part of the forcing chain.
For $\alpha^{-1}$, RS supplies a closed real interval with lower endpoint $137.030$ and upper endpoint $137.039$. The primer places the RS-native band inside $(137.030, 137.039)$. CODATA 2022 reports $137.035999177(21)$, which lies inside that band.
Interval width is the standard difference of endpoints (as in the rational and real interval utilities used elsewhere in the library). Here the same pattern is applied to the RS $\alpha^{-1}$ bounds so that absolute and relative precision statements can be stated as ordinary real equalities and inequalities.
proof idea
Pure definition: the width is the real difference of the two constant endpoints already declared in the module. No lemma application or tactic work occurs at this site; downstream theorems unfold the definition and discharge the arithmetic by norm_num.
why it matters
This width is the absolute precision of the RS $\alpha^{-1}$ forecast and is the numerator of the relative-precision ratio against the CODATA central value. It feeds three local results: the equality that the width equals $0.009$, the relative-precision definition (width over CODATA central, about $66$ ppm), and the theorem that relative precision is strictly less than $100$ ppm.
In the broader framework it makes the primer's alpha band concrete and machine-checkable: the same interval that contains the experimental value is shown to be narrow enough for a sub-$100$ ppm claim. The declaration does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it only quantifies how tight the already-derived numerical window is.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.