prediction
plain-language theorem explainer
Preregisters the RS target band for the inverse fine-structure constant as the closed interval [137.030, 137.039] under the name alphaInv. Verification and phenomenology modules cite this record as the fixed, non-experimental prediction against which derived α⁻¹ expressions are checked. The body is a plain IntervalPrediction structure literal: name plus two decimal endpoints, no proof obligations.
Claim. The preregistered prediction for the inverse fine-structure constant is the interval record with name $\mathrm{alphaInv}$ and endpoints $\mathrm{lo}=137.030$, $\mathrm{hi}=137.039$ (an $IntervalPrediction$).
background
This module is the preregistered prediction file for $\alpha^{-1}$. Its module header states that the file intentionally contains no experimental values: the band is a fixed RS target, not a CODATA fit.
Upstream, Constants.Alpha.alphaInv is the dimensionless inverse fine-structure expression from the canonical exponential resummation (seed $4\pi\cdot 11$ times an exponential gap factor), assembled with nothing fit to CODATA. A parallel PRC form writes $\alpha^{-1}=44\pi\exp(-w_8\ln\varphi/(44\pi))$. The exact infrared value $\alpha^{-1}(0)=137.035999$ is flagged OPEN as a boundary condition.
IntervalPrediction (from Preregistered.Core) is the common record type for named real intervals used across the verification layer. The sibling AlphaS prediction file uses the same pattern for a point prediction.
proof idea
Definition, not a theorem. The body is a single structure literal of type IntervalPrediction: set the name string to "alphaInv", lower endpoint to 137.030, upper endpoint to 137.039. No tactics, no lemmas, no computation.
why it matters
Locks the RS $\alpha^{-1}$ band cited in the framework primer: $\alpha^{-1}$ inside $(137.030, 137.039)$. Downstream consumers (about forty use sites) treat this record as the shared preregistered target when certifying constants, chemistry proxies, and astrophysical ladders. Sibling lemmas lo_verified and hi_verified in the same module are the natural place to discharge that the constructed alphaInv expression lands inside the band.
The declaration does not close the OPEN infrared boundary-condition question on the exact CODATA-scale value; it only freezes the interval that RS claims before comparison. That separation (prediction record vs. derived expression vs. experiment) is the point of the Preregistered layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.