sub_contains_sub
The theorem shows that if a real x lies inside interval I and y inside J then x minus y lies inside the difference interval I minus J. Numerics researchers building verified bounds on real functions would cite this when composing subtraction steps in interval arithmetic. The proof is a direct constructor split that reduces both endpoint inequalities to sub_le_sub via the endpoint lemmas sub_lo and sub_hi.
claimLet $I$ and $J$ be closed intervals with rational endpoints. If the real number $x$ satisfies $I.lo ≤ x ≤ I.hi$ and $y$ satisfies $J.lo ≤ y ≤ J.hi$, then $x - y$ satisfies $(I - J).lo ≤ x - y ≤ (I - J).hi$, where $(I - J).lo = I.lo - J.hi$ and $(I - J).hi = I.hi - J.lo$.
background
The module supplies verified interval arithmetic that uses rational endpoints to produce rigorous bounds on real-valued expressions. An Interval is the structure consisting of rational lo and hi with the proof obligation lo ≤ hi. The contains predicate for an interval I and real x is the conjunction (I.lo cast to ℝ) ≤ x ∧ x ≤ (I.hi cast to ℝ). Subtraction of intervals is defined by the endpoint rules sub_lo and sub_hi, which set the lower bound of I - J to I.lo - J.hi and the upper bound to I.hi - J.lo.
proof idea
The proof opens with the constructor tactic to split the target containment into its lower-bound and upper-bound conjuncts. Each conjunct is discharged by a simp only [sub_lo, Rat.cast_sub] step followed by exact sub_le_sub applied to the appropriate projections of the input hypotheses hx and hy.
why it matters in Recognition Science
This lemma supplies the subtraction case for the interval-arithmetic layer that supports exact bounding of transcendental functions inside the numerics module. It completes one of the basic arithmetic closures required before higher-level operations such as multiplication or function evaluation can be verified. No downstream uses are recorded yet, so the result currently serves as infrastructure rather than a direct input to a parent theorem.
scope and limits
- Does not treat open or half-open intervals.
- Does not cover multiplication, division, or exponentiation of intervals.
- Does not supply floating-point rounding error analysis.
- Does not extend to unbounded or infinite intervals.
formal statement (Lean)
96theorem sub_contains_sub {x y : ℝ} {I J : Interval}
97 (hx : I.contains x) (hy : J.contains y) : (I - J).contains (x - y) := by
proof body
Term-mode proof.
98 constructor
99 · simp only [sub_lo, Rat.cast_sub]
100 exact sub_le_sub hx.1 hy.2
101 · simp only [sub_hi, Rat.cast_sub]
102 exact sub_le_sub hx.2 hy.1
103
104/-- Multiplication for positive intervals -/