sub_lo
The declaration states that the lower endpoint of the difference of two intervals equals the lower endpoint of the first minus the upper endpoint of the second. Researchers performing verified bound propagation on real-valued functions would cite it to simplify expressions during interval subtraction. The proof is immediate reflexivity from the definition of interval subtraction.
claimLet $I$ and $J$ be closed intervals with rational endpoints. The lower endpoint of the interval $I - J$ equals the lower endpoint of $I$ minus the upper endpoint of $J$.
background
The module supplies verified interval arithmetic over rational endpoints to produce rigorous bounds on transcendental functions. An interval is defined as a structure with rational lower and upper endpoints together with a proof that the lower does not exceed the upper. This supplies exact arithmetic without rounding error for subsequent certification steps.
proof idea
The proof is a one-line reflexivity that matches the definition of subtraction on the Interval structure.
why it matters in Recognition Science
The lemma is invoked inside the containment theorem for interval subtraction, which shows that if a real lies in the first interval and another lies in the second then their difference lies in the difference interval. It therefore supports the module's goal of rigorous numerical verification inside Recognition Science computations.
scope and limits
- Does not establish validity of the resulting difference interval.
- Does not extend to intervals whose endpoints are real numbers.
- Does not treat addition, multiplication, or other arithmetic operations.
- Does not address empty intervals or unbounded intervals.
Lean usage
simp only [sub_lo, Rat.cast_sub]formal statement (Lean)
93@[simp] theorem sub_lo (I J : Interval) : (I - J).lo = I.lo - J.hi := rfl