Soundness of IEEE32Exec.Interval32.add / sub / neg

This file proves the “golden theorem”-style enclosure results for the monotone interval operations:

• addition: $[a,b]+[c,d]\subseteq[a+c,b+d]$,
• negation: $-[a,b]=[-b,-a]$,
• subtraction: $[a,b]-[c,d]\subseteq[a-d,b-c]$ (a derived combination of addition and negation).

In NN/Floats/Interval/IEEEExec32.lean, these are implemented with IEEE32 executable outward-rounded endpoints:

• add uses addDown / addUp,
• sub uses subDown / subUp, where $\operatorname{subDown}(x,y)=\operatorname{addDown}(x,-y)$, and similarly for subUp.

We work in EReal because finite binary32 inputs can still overflow under addition or subtraction. The extended-real endpoints record those infinite results directly and let these lemmas compose with the multiplication/division soundness layer without a separate no-overflow hypothesis.

Standards alignment (informal):

• IEEE 754-2019 defines binary32 arithmetic and special values (NaN/Inf/signed zero).
• IEEE 1788-2015 defines a standard API and semantics for interval arithmetic; the enclosures above are the basic “set-based” interval laws in the valid (outer enclosure) mode.

Note: we do not attempt to prove bit-for-bit conformance of IEEE32Exec to any specific CPU/GPU. Instead, we prove that our executable model (which follows IEEE-style rules) has the stated enclosure relationship to the real semantics on the finite path.

Small helpers

Interval addition

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.add_sound (A B : Interval32) (hA : A.Valid) (hB : B.Valid) {x y : ℝ} : x ∈ Set.Icc A.lo.toReal A.hi.toReal → y ∈ Set.Icc B.lo.toReal B.hi.toReal → (A.add B).lo.toEReal ≤ ↑x + ↑y ∧ ↑x + ↑y ≤ (A.add B).hi.toEReal

Soundness of Interval32.add w.r.t. real addition, in the finite-endpoint regime.

If $x\in[A.\mathtt{lo},A.\mathtt{hi}]$ and $y\in[B.\mathtt{lo},B.\mathtt{hi}]$ in real semantics, then $x+y$ lies between the EReal interpretation of the executable endpoints of Interval32.add A B.

Interval negation

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.neg_sound (A : Interval32) (hA : A.Valid) {x : ℝ} : x ∈ Set.Icc A.lo.toReal A.hi.toReal → A.neg.lo.toEReal ≤ -↑x ∧ -↑x ≤ A.neg.hi.toEReal

Soundness of Interval32.neg w.r.t. real negation, in the finite-endpoint regime.

If $x\in[A.\mathtt{lo},A.\mathtt{hi}]$ in real semantics, then $-x$ lies between the EReal interpretation of the executable endpoints of Interval32.neg A.

Interval subtraction

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.sub_sound (A B : Interval32) (hA : A.Valid) (hB : B.Valid) {x y : ℝ} : x ∈ Set.Icc A.lo.toReal A.hi.toReal → y ∈ Set.Icc B.lo.toReal B.hi.toReal → (A.sub B).lo.toEReal ≤ ↑x - ↑y ∧ ↑x - ↑y ≤ (A.sub B).hi.toEReal

Soundness of Interval32.sub w.r.t. real subtraction, in the finite-endpoint regime.

This is a derived enclosure rule: [a,b] - [c,d] ⊆ [a-d, b-c], implemented with directed rounding via subDown/subUp.