add
Defines addition for closed rational intervals by adding lower and upper bounds separately while preserving validity. Numerics researchers building verified bounds on real functions would cite it when composing interval operations. The implementation is a direct structure constructor that applies add_le_add to the input validity proofs.
claimFor closed intervals $I=[a,b]$ and $J=[c,d]$ with rational endpoints satisfying $a≤b$ and $c≤d$, define $I+J=[a+c,b+d]$.
background
Interval arithmetic here uses closed intervals with rational endpoints to enclose real values exactly. The structure Interval consists of lo and hi rationals together with a proof lo≤hi, and derives decidable equality. This module supplies the basic operations needed for rigorous enclosure of transcendental functions using rational arithmetic in Lean. Upstream the same Interval type appears in Recognition.Certification but with real endpoints.
proof idea
The definition is a structure constructor: lo is the sum of the input lo fields, hi is the sum of the input hi fields, and valid is obtained by applying the lemma add_le_add to the two input validity proofs. An Add instance is then registered so that + notation works on Interval.
why it matters in Recognition Science
This supplies the core addition operation for the verified interval arithmetic layer that supports numeric bounds throughout the Recognition framework. It enables the Add typeclass instance and feeds any later composite operations on intervals, though no downstream uses are recorded yet. It directly implements the interval addition rule stated in the module doc-comment.
scope and limits
- Does not extend to intervals with real endpoints.
- Does not implement subtraction or multiplication.
- Does not guarantee minimal-width results.
- Does not handle empty or unbounded intervals.
formal statement (Lean)
46def add (I J : Interval) : Interval where
47 lo := I.lo + J.lo
proof body
Definition body.
48 hi := I.hi + J.hi
49 valid := add_le_add I.valid J.valid
50
51instance : Add Interval where
52 add := add
53