Numerics Interval Basic Hi Le Implies Contains Le

Interval bounds

Interval arithmetic is a way of computing with ranges instead of single numbers. A closed interval is a set of real numbers between a lower endpoint and an upper endpoint. The Recognition Science framework's machine-checked library defines such an interval with rational endpoints, and the theorem hi_le_implies_contains_le states a simple consequence: if the upper endpoint of an interval is at most some rational number b, then every real number contained in the interval is at most b. In symbols, if I.hi ≤ b and I contains x, then x ≤ b. This is the upper-bound half of the containment property; a companion theorem, lo_ge_implies_contains_ge, gives the lower-bound half.

The proof is a direct chain of inequalities. If x lies in the interval, then by definition x ≤ I.hi. The hypothesis supplies I.hi ≤ b. Transitivity of ≤ on the real numbers yields x ≤ b. The library's formalization uses exact_mod_cast to move the rational comparison into the real numbers, where the ordering is compatible. This is not a deep result, but it is exactly the kind of lemma that makes verified interval arithmetic trustworthy: every step of a computation can be checked against such basic facts.

In the Recognition Science framework, this theorem is part of a larger library of formalized mathematics. The library is a machine-checked collection of theorems, meaning each statement has a proof that a computer program verifies from axioms. This particular theorem does not depend on any framework-specific assumptions about recognition or cost functions. It is a general fact about intervals and ordered real numbers, usable in any context where rigorous bounds are needed.

The practical payoff is that when the framework computes bounds on transcendental functions, as its documentation describes, it can rely on these interval facts to guarantee correctness. A programmer or mathematician using the library gets a certificate that the computed range truly contains the true value. The theorem hi_le_implies_contains_le is a small but load-bearing piece of that guarantee.

/-- 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 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)

What this page does not claim

This theorem does not state that the interval's upper endpoint is the least upper bound of the contained numbers. This theorem does not imply that every rational b above the upper endpoint is a valid bound for all real numbers, only those in the interval. This theorem does not establish any property of recognition, cost, or the forcing chain.

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: