hi_verified
plain-language theorem explainer
The RS-derived inverse fine-structure constant lies strictly below the preregistered upper edge 137.039. Anyone auditing the α⁻¹ interval prediction cites this bound. The proof is a one-line rewrite of the existing numerical inequality alphaInv_lt after unfolding the prediction record.
Claim. The Recognition Science value of $\alpha^{-1}$ satisfies $\alpha^{-1} < 137.039$, where $137.039$ is the upper endpoint of the preregistered interval prediction for $\alpha^{-1}$.
background
This module preregisters an interval prediction for the inverse fine-structure constant and deliberately holds no experimental inputs. The core structure IntervalPrediction is a named triple (name, lo, hi) of reals. Here the prediction is fixed to lo = 137.030 and hi = 137.039, matching the RS-native α⁻¹ band from the framework primer.
The constant alphaInv is the dimensionless RS expression assembled by exponential resummation from the seed $4\pi\cdot 11$ (equivalently $44\pi$) and a gap term; its doc-comment stresses that nothing is fit to CODATA, and that the exact infrared value $\alpha^{-1}(0)=137.035999$ remains an open boundary condition. Upstream, alphaInv_lt already proves the strict numerical inequality against 137.039 by interval arithmetic on the seed and gap.
proof idea
One-line wrapper. Unfold prediction and the hi field of IntervalPrediction, then discharge the goal by the existing theorem alphaInv_lt : alphaInv < 137.039. The simpa tactic performs that rewrite and closes.
why it matters
Closes the upper half of the preregistered α⁻¹ check: the assembled RS constant must sit inside the published band (137.030, 137.039). Together with the sibling lower-bound lemma, this turns the interval prediction into a machine-checked containment statement rather than a comment. The band is a framework landmark (α⁻¹ inside that open interval). The exact IR match to CODATA is still flagged OPEN in the constant's documentation, so this result only certifies the preregistered envelope, not a precision fit. No downstream consumers are wired yet; the lemma is the verification endpoint for the upper edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.