add_lo
The add_lo result states that the lower bound of the sum of two intervals with rational endpoints is exactly the sum of those lower bounds. Code verifying bounds on functions in the Recognition numerics layer cites this during simplification of interval expressions. The proof reduces immediately to the reflexivity of the interval addition definition.
claimLet $I$ and $J$ be closed intervals with rational endpoints. Then the lower endpoint of the sum interval $I + J$ equals the sum of the lower endpoints of $I$ and $J$.
background
The module implements verified interval arithmetic using rational endpoints to bound real values exactly. An Interval is a structure consisting of a lower rational lo, upper rational hi, and a proof that lo ≤ hi. This theorem relies on the definition of interval addition, which constructs a new interval with lo = I.lo + J.lo and hi = I.hi + J.hi.
proof idea
This is a one-line wrapper that applies reflexivity to the definition of addition on the Interval structure.
why it matters in Recognition Science
This declaration supports the add_contains_add theorem, which establishes that the sum of intervals contains the sum of contained reals. It forms part of the foundational layer for rigorous numerical computations in Recognition Science, ensuring that bounds on quantities like the fine structure constant or mass ladders remain exact.
scope and limits
- Does not extend to real-valued endpoints.
- Does not establish containment of sums.
- Does not define interval multiplication.
- Does not handle unbounded intervals.
formal statement (Lean)
54@[simp] theorem add_lo (I J : Interval) : (I + J).lo = I.lo + J.lo := rfl