Numerics Interval Basic Lo Ge Implies Contains Ge

The lower bound guarantee

Interval arithmetic is a way to do calculations with ranges of values instead of single numbers. A closed interval with rational endpoints is written as [lo, hi], where lo is the lower endpoint and hi is the upper endpoint, and the condition lo ≤ hi always holds. The interval contains a real number x when both lo ≤ x and x ≤ hi are true. This is the classical setup used in numerical analysis to track rounding errors and to prove that a computed result lies within a known range.

The theorem lo_ge_implies_contains_ge states a simple consequence of this setup. If a rational number b is less than or equal to the lower endpoint lo, and x is any real number contained in the interval, then b is less than or equal to x. In symbols: if b ≤ lo and x ∈ [lo, hi], then b ≤ x. The proof is a direct chain of inequalities: b ≤ lo (given), and lo ≤ x (because x is in the interval), so b ≤ x. This is a basic but essential lemma for verifying that a lower bound computed with rational arithmetic is a true lower bound for the real value it approximates.

The theorem is part of a larger verified interval arithmetic library. The library uses rational endpoints, which a machine can compute exactly, to bound real values. Other theorems in the same library establish the analogous result for the upper endpoint (hi_le_implies_contains_le), and for strict inequalities (lo_gt_implies_contains_gt and hi_lt_implies_contains_lt). Together these lemmas form the foundation for proving that operations like addition, subtraction, multiplication, and exponentiation on intervals correctly contain the results of the corresponding operations on real numbers.

In Recognition Science, this theorem is not a claim about the physical world. It is a piece of mathematical infrastructure. The framework's larger claims about cost functions and physical constants depend on being able to compute rigorously, and this lemma is one of the small, machine-checked steps that make such computation trustworthy. The theorem itself says nothing about recognition, ledgers, or any physical quantity; it is purely a statement about ordered real numbers and intervals.

What the theorem does not claim is equally clear. It does not claim that every real number inside the interval is greater than b, only that it is at least b. It does not claim that b itself is inside the interval; b could be strictly less than lo. And it does not claim anything about the upper endpoint hi. The theorem is a one-way implication: given a lower bound on the interval's lower endpoint, it produces a lower bound on every point the interval contains.

/-- If b ≤ I.lo, then all x in I satisfy b ≤ x -/
theorem lo_ge_implies_contains_ge {I : Interval} {b : ℚ} (h : b ≤ I.lo) {x : ℝ}
    (hx : I.contains x) : (b : ℝ) ≤ x :=
  le_trans (by exact_mod_cast h) hx.1

/-- If b ≤ I.lo, then all x in I satisfy b ≤ x -/
theorem lo_ge_implies_contains_ge {I : Interval} {b : ℚ} (h : b ≤ I.lo) {x : ℝ}
    (hx : I.contains x) : (b : ℝ) ≤ x :=
  le_trans (by exact_mod_cast h) hx.1

/-- A closed interval with rational endpoints. -/
structure Interval where
  lo : ℚ
  hi : ℚ
  valid : lo ≤ hi
  deriving DecidableEq

/-- If I.hi ≤ b, then all x in I satisfy x ≤ b -/
theorem hi_le_implies_contains_le {I : Interval} {b : ℚ} (h : I.hi ≤ b) {x : ℝ}
    (hx : I.contains x) : x ≤ (b : ℝ) :=
  le_trans hx.2 (by exact_mod_cast h)

/-- If b < I.lo, then all x in I satisfy b < x -/
theorem lo_gt_implies_contains_gt {I : Interval} {b : ℚ} (h : b < I.lo) {x : ℝ}
    (hx : I.contains x) : (b : ℝ) < x :=
  lt_of_lt_of_le (by exact_mod_cast h) hx.1

/-- If I.hi < b, then all x in I satisfy x < b -/
theorem hi_lt_implies_contains_lt {I : Interval} {b : ℚ} (h : I.hi < b) {x : ℝ}
    (hx : I.contains x) : x < (b : ℝ) :=
  lt_of_le_of_lt hx.2 (by exact_mod_cast h)

What this page does not claim

The theorem does not claim that every real number inside the interval is strictly greater than b. The theorem does not claim that b itself is inside the interval. The theorem does not claim anything about the upper endpoint hi.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Numerics/Interval/Basic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: