lo_gt_implies_contains_gt
The theorem shows that if a rational b lies strictly below the lower endpoint of a closed rational interval I, then every real x contained in I satisfies b < x. Interval-arithmetic routines for bounding transcendental functions invoke this to propagate strict inequalities from rational endpoints. The proof is a one-line term that applies lt_of_lt_of_le after casting the rational inequality to the reals.
claimLet $I$ be a closed interval with rational endpoints. If a rational $b$ satisfies $b < I.lo$ and a real $x$ satisfies $x$ in $I$, then $b < x$.
background
The module supplies verified interval arithmetic for computing bounds on transcendental functions, using rational endpoints that Lean can compute exactly. The Interval structure consists of rational lower and upper bounds together with a proof that the lower bound does not exceed the upper bound. Containment of a real number $x$ in $I$ holds precisely when the cast of the lower bound is at most $x$ and $x$ is at most the cast of the upper bound.
proof idea
The term-mode proof applies lt_of_lt_of_le to the cast of the hypothesis b < I.lo (via exact_mod_cast) together with the left conjunct of the containment hypothesis.
why it matters in Recognition Science
This lemma is invoked by prove_lower_bound in the Numerics.Interval.Tactic module to establish strict lower bounds from containment. It supports the verified numerical infrastructure used to confirm Recognition Science constants such as the inverse fine-structure constant inside the interval (137.030, 137.039).
scope and limits
- Does not establish the symmetric upper-bound implication.
- Does not extend to intervals with irrational endpoints.
- Does not apply to open or half-open intervals.
- Does not supply quantitative error bounds beyond the strict inequality.
Lean usage
theorem example {I : Interval} {b : ℚ} {x : ℝ} (h : b < I.lo) (hx : I.contains x) : (b : ℝ) < x := lo_gt_implies_contains_gt h hxformal statement (Lean)
162theorem lo_gt_implies_contains_gt {I : Interval} {b : ℚ} (h : b < I.lo) {x : ℝ}
163 (hx : I.contains x) : (b : ℝ) < x :=
proof body
Term-mode proof.
164 lt_of_lt_of_le (by exact_mod_cast h) hx.1
165
166/-- If I.hi < b, then all x in I satisfy x < b -/