add_lo
plain-language theorem explainer
The lower endpoint of the sum of two closed rational intervals equals the sum of their individual lower endpoints. Numerics code that computes rigorous bounds on transcendental functions cites this when simplifying addition expressions inside interval arithmetic. The proof is a direct reflexivity that follows from the definition of interval addition.
Claim. Let $I = [a, b]$ and $J = [c, d]$ be closed intervals with rational endpoints satisfying $a ≤ b$ and $c ≤ d$. Then the lower endpoint of the sum interval $I + J$ equals $a + c$.
background
The module supplies verified interval arithmetic that uses rational endpoints to bound real values. An Interval is the structure with fields lo : ℚ, hi : ℚ and a proof that lo ≤ hi. The local setting is exact rational computation to certify bounds without floating-point error.
proof idea
One-line wrapper that applies reflexivity after the definition of addition on the lower components.
why it matters
This lemma is invoked inside add_contains_add to establish that the sum interval contains the sum of any two contained reals. It belongs to the numerics layer that supplies certified bounds for the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.