alphaInv_RS_lo
plain-language theorem explainer
Fixes the lower edge of the Recognition Science prediction band for the inverse fine-structure constant at 137.030. Anyone checking the RS-versus-CODATA containment claim cites this constant as the left endpoint. It is a bare real literal, not a derived theorem.
Claim. The Recognition Science lower bound on the inverse fine-structure constant is the real number $\alpha^{-1}_{\mathrm{RS,lo}} := 137.030$, so the predicted open interval is $137.030 < \alpha^{-1} < 137.039$.
background
The module Machine-Verified PDG Comparison holds numerical RS predictions next to CODATA/PDG experimental anchors. 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.
In RS-native units the inverse fine-structure constant is forced into a narrow band. The primer records that band as $\alpha^{-1}$ inside $(137.030, 137.039)$. This definition is simply the left endpoint of that interval; its sibling supplies the right endpoint 137.039.
CODATA 2022 reports $\alpha^{-1}_{\mathrm{exp}} = 137.035999177(21)$. The verification goal is to show the RS open interval contains that central value and to measure the residual deviation and relative width.
proof idea
No proof. The declaration is a definition equal to the decimal literal 137.030. Downstream lemmas unfold it and discharge numeric goals with norm_num.
why it matters
This constant is the left endpoint used by the key containment theorem: the RS interval contains the CODATA 2022 central value. It also feeds the center $(lo+hi)/2 = 137.0345$, the width $hi-lo = 0.009$ (about 66 ppm), the signed deviation from CODATA (about $-0.0015$), the lower-bound verification lemma, and the sub-100 ppm precision claim.
In the broader framework it is the concrete numerical face of the RS $\alpha$ band cited in the primer. It does not itself derive $\alpha$ from the forcing chain (T0–T8) or the Recognition Composition Law; those derivations live upstream in Constants.Alpha and the interval numerics. Here the number is frozen so machine-checked comparison lemmas can cite a single shared endpoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.