Nearest-even lies between directed roundings (op-level corollaries)

NN.Floats.IEEEExec.RoundDyadicToIEEE32Bounds proves the core theorem:

roundDyadicDown d ≤ roundDyadicToIEEE32 d ≤ roundDyadicUp d (in EReal).

This file packages small op-level corollaries for IEEE32Exec.add / mul / sub on the finite path:

addDown x y ≤ add x y ≤ addUp x y, and similarly for multiplication and subtraction.

These are useful for “checked boundary => enclosure” statements in downstream code (e.g. RL shadow interval diagnostics).

Small helpers

Addition sandwich

On the finite path, add/addDown/addUp all reduce to rounding the same exact dyadic sum with different rounding modes.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_addDown_le_add_le_addUp_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.addDown y).toEReal ≤ (x.add y).toEReal ∧ (x.add y).toEReal ≤ (x.addUp y).toEReal

Multiplication sandwich

On finite inputs, mul/mulDown/mulUp reduce to rounding the same exact dyadic product with different rounding modes.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_mulDown_le_mul_le_mulUp_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.mulDown y).toEReal ≤ (x.mul y).toEReal ∧ (x.mul y).toEReal ≤ (x.mulUp y).toEReal

Subtraction sandwich

This is a direct corollary of the addition sandwich, since:

sub x y = add x (neg y) and similarly for directed endpoints.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_subDown_le_sub_le_subUp_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.subDown y).toEReal ≤ (x.sub y).toEReal ∧ (x.sub y).toEReal ≤ (x.subUp y).toEReal