lo_verified
plain-language theorem explainer
The preregistered lower endpoint 137.030 lies strictly below the Recognition Science inverse fine-structure constant. Constants and verification auditors cite it to confirm the announced α⁻¹ band is open on the left relative to the closed-form value. The proof is a one-line wrapper that unfolds the interval record and applies the numeric lower-bound theorem.
Claim. The lower endpoint of the preregistered interval for the inverse fine-structure constant satisfies $137.030 < \alpha^{-1}$, where $\alpha^{-1}$ denotes the RS closed-form value $\alpha_{\mathrm{seed}}\,\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$.
background
This module preregisters an interval prediction for the inverse fine-structure constant and deliberately stores no experimental (CODATA) numbers. The prediction record is the open band with endpoints $137.030$ and $137.039$, matching the RS-native $\alpha^{-1}$ window.
The constant $\alpha^{-1}$ is the dimensionless RS expression $\alpha_{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$ (canonical exponential resummation). Upstream documentation stresses that nothing is fit to CODATA: the seed $4\pi\cdot 11$ is an identification, and the exact infrared value $\alpha^{-1}(0)=137.035999$ remains an open boundary condition.
The supporting numeric theorem states $(137.030:\mathbb{R})<\alpha^{-1}$, obtained from a stronger lower estimate on the gap term (via $\log\varphi>0.481$ and eight-tick weight bounds).
proof idea
One-line wrapper. Unfold the local prediction record and its lower-endpoint field, then discharge the goal by the upstream numeric inequality $(137.030:\mathbb{R})<\alpha^{-1}$. The simpa call only rewrites definitional equalities; no new arithmetic is performed here.
why it matters
Closes the left half of the preregistered $\alpha^{-1}$ check: the RS closed-form value sits strictly above the announced floor $137.030$. Together with the sibling upper-bound verification it pins the framework landmark that $\alpha^{-1}$ lies inside $(137.030,137.039)$ in RS-native units, with no experimental input in this file.
No downstream consumers are wired yet; the lemma is a leaf of the verification layer. It does not touch the still-open infrared boundary condition $\alpha^{-1}(0)=137.035999$, nor the status of the seed identification. It simply certifies that the assembled construction clears the preregistered lower cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.