contains
plain-language theorem explainer
The contains definition specifies membership of a real number x inside a closed interval I whose endpoints are rationals. Numerics code and downstream results in complexity and cosmology cite it to obtain rigorous bounds on computations. It is a direct structural unfolding of the Interval record with no additional lemmas or tactics.
Claim. Let $I = [a, b]$ be a closed interval with $a, b : ℚ$ and $a ≤ b$. For $x : ℝ$, $x$ lies in $I$ if and only if $a ≤ x ≤ b$.
background
The module supplies verified interval arithmetic that bounds real values by rational endpoints, allowing exact computation of transcendental functions without floating-point error. The Interval structure records two rationals lo and hi together with the proof that lo ≤ hi. Containment is the predicate that lifts these rational bounds to the reals. Upstream structures in Certification and Manifold supply analogous interval and point notions that this definition generalizes for numeric use.
proof idea
One-line definition that directly projects the lo and hi fields of the Interval structure and asserts the standard real inequality between them.
why it matters
The predicate is invoked by forty downstream declarations, including jcostEdgeWeight bounds in JCostLaplacian, H_SATCARuntime in CellularAutomata, zAgingChannel_count in HubbleTensionPipeline, and reachability checks in StakeGraph. It supplies the basic membership test required for interval-based verification throughout the numerics layer that supports unification and emergence calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.