Soundness of IEEE32Exec.Interval32.mul (4-corner rule)

NN/Floats/Interval/IEEEExec32.lean defines executable endpoint intervals with IEEE32Exec endpoints and outward-rounded arithmetic. Interval multiplication is implemented with the classical “4-corner” rule:

[a,b] * [c,d] ⊆ [ min(ac, ad, bc, bd),  max(ac, ad, bc, bd) ].

In our executable implementation, each corner product is computed using directed rounding:

• mulDown for lower endpoints,
• mulUp for upper endpoints, and then the minimum/maximum of the four corners is taken using IEEE minimum/maximum.

This file proves the main enclosure theorem connecting that executable construction to real semantics (in EReal to allow overflow to ±∞).

The theorem is stated in a finite-input regime (isFinite endpoints), which matches the setting for interval bound propagation over real-valued networks. Overflow may still occur in intermediate corner computations, and the proof handles it via EReal.

Real helper lemmas (min/max of 4 corners)

Interval multiplication soundness

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.mul_sound (A B : Interval32) (hAlo : A.lo.isFinite = true) (hAhi : A.hi.isFinite = true) (hBlo : B.lo.isFinite = true) (hBhi : B.hi.isFinite = true) {x y : ℝ} : x ∈ Set.Icc A.lo.toReal A.hi.toReal → y ∈ Set.Icc B.lo.toReal B.hi.toReal → (A.mul B).lo.toEReal ≤ ↑x * ↑y ∧ ↑x * ↑y ≤ (A.mul B).hi.toEReal

Soundness of Interval32.mul w.r.t. real multiplication:

If x ∈ [A.lo, A.hi] and y ∈ [B.lo, B.hi] (interpreted as real intervals), then x*y lies in the real interval concretization of Interval32.mul A B.

The endpoints are interpreted in EReal so that overflow to ±∞ remains a sound enclosure.