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]\subseteq \left[\min\{ac,ad,bc,bd\},\max\{ac,ad,bc,bd\}\right]. $$

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\in[A.\mathtt{lo},A.\mathtt{hi}]$ and $y\in[B.\mathtt{lo},B.\mathtt{hi}]$ (interpreted as real intervals), then $xy$ 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.