add_hi
plain-language theorem explainer
The theorem asserts that the upper endpoint of the sum of two closed rational intervals equals the sum of their separate upper endpoints. Researchers doing rigorous bound propagation on real functions would cite it when composing interval operations in verified numerics. The proof is a direct reflexivity that follows from the definition of interval addition.
Claim. Let $I$ and $J$ be closed intervals with rational endpoints. The upper endpoint of their Minkowski sum satisfies $(I + J)_{hi} = I_{hi} + J_{hi}$.
background
The module implements verified interval arithmetic that uses exact rational endpoints to enclose real values. An interval is defined as a structure carrying a lower rational bound, an upper rational bound, and a proof that the lower bound does not exceed the upper bound. Interval addition is defined componentwise on these rational fields, so the upper endpoint of the sum is literally the sum of the upper endpoints.
proof idea
The proof is a one-line reflexivity that matches the hi field of the sum directly to the sum of the hi fields by the definition of addition.
why it matters
The result is invoked inside the containment theorem add_contains_add, which establishes that the sum interval contains the sum of any pair of contained reals. It therefore supplies one of the elementary algebraic facts needed for the module's goal of producing rigorous rational bounds on transcendental functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.