sub_hi
The high endpoint of the difference of two closed rational intervals equals the high of the first minus the low of the second. Verified numerics code for bounding subtractions cites this identity when computing interval results. The proof is a direct reflexivity that follows from the definition of interval subtraction.
claimFor closed intervals $I = [I_0, I_1]$ and $J = [J_0, J_1]$ with rational endpoints satisfying $I_0 ≤ I_1$ and $J_0 ≤ J_1$, the upper endpoint of the difference satisfies $(I - J)_1 = I_1 - J_0$.
background
The module supplies verified interval arithmetic that uses rational endpoints to bound real values. Interval is the structure with fields lo, hi : ℚ and a proof that lo ≤ hi. Subtraction on intervals is defined so that the resulting interval respects the worst-case bounds for real subtraction.
proof idea
The proof is a one-line reflexivity that matches the definition of interval subtraction directly.
why it matters in Recognition Science
This identity is invoked by the containment theorem sub_contains_sub, which establishes that if x lies in I and y lies in J then x - y lies in I - J. It belongs to the numerics layer that supplies exact rational bounds for Recognition Science computations.
scope and limits
- Does not prove any containment or ordering properties.
- Does not apply to intervals whose endpoints are real numbers.
- Does not address open intervals or unbounded sets.
Lean usage
example (I J : Interval) : (I - J).hi = I.hi - J.lo := by simp [sub_hi]formal statement (Lean)
94@[simp] theorem sub_hi (I J : Interval) : (I - J).hi = I.hi - J.lo := rfl
proof body
95