alphaInv_RS_precision_sub_100ppm
plain-language theorem explainer
The Recognition Science inverse-fine-structure interval has relative width strictly below 100 ppm versus the CODATA 2022 central value. Citation target for anyone auditing how sharp the RS α⁻¹ band is against experiment. Proof is pure definition unfolding plus a `norm_num` discharge of the rational inequality.
Claim. The relative precision of the Recognition Science inverse fine-structure interval (half-width or full width over the CODATA 2022 central value $\alpha^{-1}_{\mathrm{CODATA}}=137.035999177$) satisfies $\mathrm{rel\_prec}_{\mathrm{RS}}(\alpha^{-1}) < 10^{-4}$ (equivalently, less than 100 ppm).
background
This lives in the quarantined PDG/CODATA comparison module: experimental anchors are imported, so nothing here enters the certified RS forcing chain. The local objects are the machine interval bounds on the RS inverse fine-structure constant (roughly $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$) and the CODATA 2022 central value $\alpha^{-1}=137.035999177(21)$.
Relative precision is defined from the RS interval width divided by that CODATA central value (via alphaInv_RS_interval_width and the lo/hi endpoints). The primer landmark is the RS $\alpha^{-1}$ band inside $(137.030, 137.039)$; this lemma only quantifies how narrow that band is in ppm, not why the band is forced.
Upstream numerical constants (alphaInv_RS_lo, alphaInv_RS_hi, alphaInv_CODATA_2022) are plain real definitions; the comparison is informational against Tiesinga et al. (CODATA 2022).
proof idea
One short tactic proof. Unfold the relative-precision abbreviation, then the interval-width definition, then the concrete lo/hi RS endpoints and the CODATA 2022 central value. After those unfolds the goal is a closed numerical inequality on concrete rationals/reals; norm_num finishes it. No lemmas beyond definitional reduction.
why it matters
Closes the precision half of the module's headline α⁻¹ audit: not only does the RS interval contain the CODATA central value, its relative width is under 100 ppm. That is the quantitative sharpness claim a referee wants next to the containment statement.
It does not feed further theorems in-tree (used_by is empty); it is a terminal verification fact. Framework landmark: the RS $\alpha^{-1}$ window $(137.030, 137.039)$ from the constants layer. Epistemic status stays quarantined: experimental CODATA input means this never joins the T0–T8 forcing chain or the certified surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.