pith. machine review for the scientific record. sign in
def definition def or abbrev high

contains

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  25def contains (I : Interval) (x : ℝ) : Prop :=

proof body

Definition body.

  26  (I.lo : ℝ) ≤ x ∧ x ≤ (I.hi : ℝ)
  27
  28/-- Point interval containing a single rational -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.