roundDyadicToIEEE32 is sandwiched by directed rounding (the “full IEEE” bridge)

Our codebase has two floating-point execution models for binary32:

1. roundDyadicToIEEE32 (in NN/Floats/IEEEExec/Exec32.lean)
   • models IEEE-754 round-to-nearest, ties-to-even when rounding an exact dyadic (-1)^sign * mant * 2^exp back to float32.
2. roundDyadicDown / roundDyadicUp
   • implement directed rounding toward -∞ / +∞.
   • these are the primitives used by interval arithmetic endpoints (addDown/addUp, etc.).

To justify “IBP/CROWN bounds are sound w.r.t. full IEEE execution”, we need a bridge that relates these two rounding policies.

The key fact is:

For every exact dyadic d, nearest-even rounding lies between the directed endpoints:

roundDyadicDown d ≤ roundDyadicToIEEE32 d ≤ roundDyadicUp d

(with the order taken in EReal via toEReal so that ±∞ behavior remains well-defined).

Intuition:

• Directed rounding computes the lower / upper neighbor of the exact real value on the binary32 grid (“floor” / “ceil” on the float lattice).
• Nearest-even rounding must choose one of these two neighbors.

So the proof splits into:

1. a nonnegative lemma showing the nearest-even implementation returns either the directed down result or the directed up result, and
2. a sign-flip lemma for toEReal allowing us to lift the result to signed dyadics.

We keep the argument executable-model-specific but mathematically elementary: the only “real math” we use is that Nat.log2 controls the bit-length, and that shifting right is division by a power of two.

Small Nat helpers

Working around Nat.decLe (Lean 4.26)

Nat.decLe is implemented as a nested dependent dite over Nat.ble, and rewriting under the scrutinee of a match on Decidable is very brittle in Lean 4.26.

To keep our main proofs readable, we use a small lemma that reduces the specific decLe-match used in the binary32 subnormal “round up to the smallest normal” check.

Bit-length bounds used to rule out impossible carries

In the normal regime, roundDyadicToIEEE32 computes a 24-bit mantissa m24.

If m24 = 2^24 we carry into the exponent (this is the IEEE rule when rounding pushes us across a power-of-two boundary).

However, the floor quotient produced by Nat.shiftRight can never be 2^24 in that regime: it always fits strictly below 2^24.

We prove the corresponding statement as a reusable lemma.

Nonnegative case: nearest-even picks down or up

For sign = false, roundDyadicDown and roundDyadicUp reduce to the positive kernels roundDyadicPosDown / roundDyadicPosUp.

In each magnitude regime, the only difference between the three rounders is the choice of Nat quotient when shifting right:

• floor quotient: Nat.shiftRight
• nearest-even: roundShiftRightEven
• ceil quotient: shiftRightCeilPow2

Since each of these returns either q or q+1, nearest-even must coincide with one of the directed candidates.

Main theorem: nearest-even lies between directed endpoints (in EReal)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundDyadicDown_le_roundDyadicToIEEE32_le_roundDyadicUp (d : Dyadic) : (roundDyadicDown d).toEReal ≤ (roundDyadicToIEEE32 d).toEReal ∧ (roundDyadicToIEEE32 d).toEReal ≤ (roundDyadicUp d).toEReal

Nearest-even rounding is sandwiched between directed roundings (in EReal).

Informal: rounding a dyadic to float32 using round-to-nearest-even yields a value that lies between rounding down and rounding up.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundDyadicDown_le_roundDyadicToIEEE32 (d : Dyadic) : (roundDyadicDown d).toEReal ≤ (roundDyadicToIEEE32 d).toEReal

Lower bound half of toEReal_roundDyadicDown_le_roundDyadicToIEEE32_le_roundDyadicUp.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundDyadicToIEEE32_le_roundDyadicUp (d : Dyadic) : (roundDyadicToIEEE32 d).toEReal ≤ (roundDyadicUp d).toEReal

Upper bound half of toEReal_roundDyadicDown_le_roundDyadicToIEEE32_le_roundDyadicUp.