interval_contains
plain-language theorem explainer
Open-interval membership of a measurement central value inside a preregistered prediction band. Verification tests cite it to assert that a frozen formula band covers an empirical central value. The body is the two-sided strict inequality on the reals; no proof work beyond the definition.
Claim. Given an interval prediction with real bounds $\ell < h$ and a measurement with central value $c$, the containment predicate holds precisely when $\ell < c < h$.
background
The Preregistered Test Harness separates predictions from measurements in the Lean import graph so that formula modules never see empirical data. Predictions live in modules that do not import measurement modules; measurements are pure data; tests import both. This does not prove historical preregistration, but it enforces an auditable freeze inside the build.
An interval prediction is a named open band on $\mathbb{R}$ with lower and upper endpoints. A measurement here is a named triple of central value and one-sigma uncertainty. Containment ignores the sigma field and only asks whether the central value lies strictly inside the band. Sibling predicates handle point predictions and sigma-window checks.
proof idea
Pure definition, not a theorem. The predicate is definitionally the conjunction of the two strict inequalities comparing the prediction endpoints to the measurement central value. Downstream tests unfold it and discharge the inequalities by norm_num on concrete rationals.
why it matters
This is the atomic pass/fail gate for interval-style preregistered checks. The immediate consumer is the CODATA 2022 test on the inverse fine-structure constant: that theorem asserts containment of the declared CODATA central value inside the frozen prediction band, then unfolds and closes by numeric normalization. Tightening of the band itself is deferred to AlphaBounds; this definition only records the open-interval criterion. In the broader Recognition verification stack it is the structural link between a formula frozen before data and an empirical central value, supporting the alpha band claim without smuggling measurement into the prediction module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.