alphaInv_RS_relative_precision
plain-language theorem explainer
Relative precision of the RS inverse fine-structure prediction is the RS interval width divided by the CODATA 2022 central value, about 66 ppm. Verification authors cite it when stating how tight the RS α⁻¹ band is against experiment. The body is a one-line quotient of two named real constants already fixed in this module.
Claim. Define the RS relative precision of $\alpha^{-1}$ by $\mathrm{rel\,prec} := w_{\mathrm{RS}} / \alpha^{-1}_{\mathrm{CODATA\,2022}}$, where $w_{\mathrm{RS}}$ is the width of the RS prediction interval for $\alpha^{-1}$ and $\alpha^{-1}_{\mathrm{CODATA\,2022}} = 137.035999177$ is the CODATA 2022 central value.
background
This module machine-compares Recognition Science predictions to PDG/CODATA numbers. 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.
The RS band for the inverse fine-structure constant is the machine-verified open interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$. Its width is the difference of the named upper and lower endpoints (about $0.009$). CODATA 2022 supplies the experimental central value $\alpha^{-1} = 137.035999177(21)$, stored here as a plain real constant.
Relative precision is the natural dimensionless ratio of that interval width to the experimental central value, converting the absolute band into a parts-per-million figure of merit.
proof idea
Definition, not a proof. The body is the single quotient of the already-defined RS interval width by the CODATA 2022 central value. No tactics, no lemmas beyond those two named constants.
why it matters
Gives the dimensionless figure of merit used by the sibling theorem that the RS relative precision is strictly less than $100$ ppm ($1$ part in $10^{4}$). That theorem unfolds this definition and the endpoint constants, then closes by norm_num.
In the broader framework the RS $\alpha^{-1}$ band $(137.030, 137.039)$ is a landmark constant claim; this ratio turns the absolute width into a ppm comparison against CODATA without entering the certified forcing chain (T0–T8). It is verification scaffolding only: containment of the experimental point and the ppm bound are informational checks, not derivation steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.