Soundness of IEEE32Exec.Interval32.div / inv (4-corner rule + zero-straddle fallback)

NN/Floats/Interval/IEEEExec32.lean defines executable endpoint intervals with IEEE32Exec endpoints and outward-rounded arithmetic. Interval division is implemented as:

• if the denominator interval contains 0, return the conservative whole = [-∞,+∞],
• otherwise use the classical “4-corner” rule:

[a,b] / [c,d] ⊆ [ min(a/c, a/d, b/c, b/d),  max(a/c, a/d, b/c, b/d) ]

where each corner is computed using directed rounding (divDown / divUp) and we take the IEEE minimum / maximum of the 4 rounded corners.

This file proves a finite-input soundness theorem for that construction, stated in EReal to keep overflow sound (corner computations may overflow to ±∞).

References / background (informal pointers):

• Moore–Kearfott–Cloud, Introduction to Interval Analysis (2009), Ch. 2 (basic interval ops).
• IEEE 1788-2015 (interval arithmetic standard) for the “whole” fallback behavior when an interval straddles 0 in division (true quotient set is typically disconnected).
• IEEE 754-2019 for the executable binary32 kernel we model in IEEE32Exec.

EReal coercion helpers

Non-NaN facts for divDown / divUp (finite, nonzero denom)

Interval division soundness

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.div_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.div B).lo.toEReal ≤ ↑x / ↑y ∧ ↑x / ↑y ≤ (A.div B).hi.toEReal

Soundness of Interval32.div w.r.t. real division.

This theorem is phrased over real concretizations Set.Icc (toReal lo) (toReal hi).

If the executable implementation detects 0 ∈ B (via containsZero), it returns whole, and the enclosure is trivial. Otherwise we use the 4-corner rule and the directed-rounding soundness lemmas for divDown/divUp.

Reciprocal as a special case of division

Interval32.inv B is defined as Interval32.div (point posOne) B. To state its soundness in the expected mathematical form (1 / y), we need a small sanity lemma about the float constant posOne.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.inv_sound (B : Interval32) (hB : B.Valid) {y : ℝ} : y ∈ Set.Icc B.lo.toReal B.hi.toReal → B.inv.lo.toEReal ≤ 1 / ↑y ∧ 1 / ↑y ≤ B.inv.hi.toEReal

Soundness of Interval32.inv w.r.t. real reciprocal.

This is derived from div_sound using the definition inv B = div (point posOne) B plus the fact that posOne decodes to the real constant 1.