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] ⊆ [a+c, b+d],
• negation: -[a,b] = [-b, -a],
• subtraction: [a,b] - [c,d] ⊆ [a-d, b-c] (a derived combination of addition + 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 subDown x y = addDown x (neg y) and similarly for subUp.

We work in EReal so that later pipelines can compose these lemmas with the multiplication/division soundness lemmas (which are naturally overflow-aware). In the finite-input regime considered here, addition/subtraction themselves cannot overflow to ±∞, but phrasing the result in EReal keeps the API uniform.

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 ∈ [A.lo,A.hi] and y ∈ [B.lo,B.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 ∈ [A.lo,A.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.