alphaInv_RS_hi
plain-language theorem explainer
Upper endpoint of the Recognition Science inverse fine-structure band, fixed at 137.039. Anyone comparing the RS α⁻¹ interval to CODATA 2022, or computing the band center and width, cites this constant. It is a bare numeric definition aligned with the preregistered AlphaInv prediction hi field.
Claim. The upper bound of the Recognition Science prediction interval for the inverse fine-structure constant is $\alpha^{-1}_{\mathrm{RS,hi}} = 137.039$.
background
The PDGComparison module is quarantined from the certified surface: it imports experimental CODATA/PDG numbers and runs informational numerical checks, not part of the forcing proof chain. Its headline α⁻¹ claim is the machine-checked band $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$, which is required to contain the CODATA 2022 central value $137.035999177(21)$.
In the Recognition Science primer the inverse fine-structure constant is constrained to the open interval $(137.030, 137.039)$. The preregistered AlphaInv prediction packages that same band as an IntervalPrediction with lo := 137.030 and hi := 137.039. The sibling lower endpoint is the matching constant 137.030; together they define the RS interval used throughout the AlphaVerification section.
proof idea
One-line numeric definition: the real constant is set equal to 137.039, copying the hi field of the preregistered AlphaInv prediction. No tactics, lemmas, or algebraic reduction.
why it matters
This upper endpoint is the right wall of every α⁻¹ containment and precision claim in the module. Downstream, alphaInv_RS_contains_CODATA proves $137.030 < \alpha^{-1}_{\mathrm{CODATA}} < 137.039$; the interval-width definitions and theorems compute $0.009$ (about 66 ppm); the center is the midpoint 137.0345; deviation and sub-100 ppm precision statements unfold this constant directly.
It therefore anchors the framework landmark that α⁻¹ lies inside $(137.030, 137.039)$. The module itself stays quarantined: the number is imported from the preregistered prediction surface rather than re-derived from the T0–T8 forcing chain here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.