IntervalPrediction
plain-language theorem explainer
A named open real interval (lo, hi) used as a frozen forecast before any measurement module is imported. Verification authors cite it when wiring preregistered RS constants such as the fine-structure band. It is a plain three-field structure with no proof content.
Claim. An interval prediction is a triple $(n,\ell,h)$ with label $n\in\mathrm{String}$ and real endpoints $\ell,h\in\mathbb{R}$, standing for the open forecast interval $(\ell,h)$ on a physical observable.
background
The Preregistered Core module enforces a structural freeze: prediction modules must not import measurement modules; measurements are pure data; tests alone import both. That separation does not prove historical preregistration, but it makes the Lean build graph auditable.
An interval prediction is the basic forecast carrier in that harness: a string name plus real lower and upper endpoints. Sibling carriers include point predictions and measurements. The containment predicate later asks whether a measurement central value lies strictly between the two endpoints.
Upstream name helpers (kernel families, alignment protocols, protocol lower endpoints) only supply the String and $\mathbb{R}$ field types; they do not constrain the interval itself.
proof idea
Definitional structure only: three fields (name : String, lo : ℝ, hi : ℝ) and an empty body. No tactics, no lemmas, no obligations.
why it matters
This is the type of every preregistered band forecast in the verification layer. The canonical use is the fine-structure inverse prediction with $\mathrm{lo}=137.030$ and $\mathrm{hi}=137.039$, matching the RS-native $\alpha^{-1}$ band from the primer. Downstream lo_verified and hi_verified prove the derived constant sits strictly inside that band; interval_contains turns the structure into a Prop relating a prediction to a measurement. Without this carrier the freeze-before-measure discipline has nothing to freeze.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.