alphaInv_RS_upper_verified
plain-language theorem explainer
The Recognition Science inverse fine-structure constant lies strictly below the certified upper edge of the RS prediction band (below 137.039). PDG/CODATA comparison work cites this as the upper half of the machine-checked α⁻¹ interval. The proof is a one-line wrapper of the certified interval upper-bound lemma from the numerics layer.
Claim. The canonical RS inverse fine-structure constant satisfies $\alpha^{-1}_{\mathrm{RS}} < \alpha^{-1}_{\mathrm{RS,hi}}$, where $\alpha^{-1}_{\mathrm{RS,hi}}$ is the machine-certified upper endpoint of the RS prediction interval (nominally $137.039$).
background
This module is a quarantined verification layer: it compares Recognition Science constants to CODATA/PDG numbers without feeding those experiments back into the certified derivation chain. The headline RS claim for the inverse fine-structure constant is the open interval $137.030 < \alpha^{-1} < 137.039$, to be checked against CODATA 2022 $\alpha^{-1} = 137.035999177(21)$.
The quantity under test is the canonical dimensionless inverse fine-structure expression assembled in Constants.Alpha: a seed times an exponential gap correction, with nothing fit to CODATA. A parallel PRC form writes the same constant as $44\pi,\exp(-w_8\ln\varphi/(44\pi))$. The upper comparison target is the certified RS high endpoint of that prediction band.
Upstream interval arithmetic supplies a strict inequality between the assembled real and that high endpoint. This declaration simply exposes that inequality under a PDG-comparison name.
proof idea
One-line term wrapper: the goal is definitionally the statement of the certified upper-bound lemma from Numerics.Interval.AlphaBounds, so the proof is just that lemma as a term. No extra rewriting, cases, or arithmetic is performed here.
why it matters
In the Recognition framework the inverse fine-structure constant is required to land inside the narrow band $(137.030, 137.039)$. This theorem discharges the upper half of that machine-verified band for the assembled RS expression, matching the module's key result that the RS interval is tight enough to be compared with CODATA.
The module is intentionally quarantined: experimental anchors are informational, not part of the forcing chain (T0–T8) or the Recognition Composition Law. No downstream theorems currently depend on this alias; it exists so verification pages can cite a named, proved upper bound beside the sibling lower bound and the CODATA containment claim. The exact infrared match $\alpha^{-1}(0) = 137.035999\ldots$ remains an open boundary condition upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.