Basic order bounds for roundShiftRightEven

IEEE32Exec.roundShiftRightEven is the core integer-rounding primitive used by roundDyadicToIEEE32:

• We first compute an exact mantissa n (a Nat).
• We then shrink it by shift bits to land on the target mantissa width.
• The policy is round-to-nearest, ties-to-even.

For interval verification we also implement directed rounding (toward -∞ and +∞):

• floor-quotient: q = n >>> shift
• ceil-quotient: ceil(n / 2^shift) which we implement as shiftRightCeilPow2 n shift

The key structural fact (used later to relate "nearest" to "directed" rounding) is:

roundShiftRightEven n shift always lies between the floor and ceil quotients.

In other words, round-to-nearest can only choose q or q+1, and those are exactly the two directed-rounding candidates at this scale.

We prove that here in a way that is robust to later refactors of roundDyadicToIEEE32: these lemmas talk only about the low-level Nat operations, not about floats.

Public “two-point” characterization

The nearest-even quotient can only be one of the two directed-division candidates:

• the floor quotient q = n >>> shift, or
• the next integer q + 1.

This public lemma connects roundDyadicToIEEE32 (nearest rounding) to roundDyadicPosDown/roundDyadicPosUp (directed rounding).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.roundShiftRightEven_eq_shiftRight_or_shiftRight_add1 (n shift : ℕ) : roundShiftRightEven n shift = n.shiftRight shift ∨ roundShiftRightEven n shift = n.shiftRight shift + 1

Nearest-even shift-right rounding yields one of two adjacent candidates.

Informal: roundShiftRightEven n shift is either the floor quotient n >>> shift or that value plus one.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.shiftRight_le_roundShiftRightEven (n shift : ℕ) : n.shiftRight shift ≤ roundShiftRightEven n shift

Nearest-even rounding is never below the floor-quotient (shiftRight).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.roundShiftRightEven_le_shiftRight_add1 (n shift : ℕ) : roundShiftRightEven n shift ≤ n.shiftRight shift + 1

Nearest-even rounding is never above shiftRight n shift + 1.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.roundShiftRightEven_le_shiftRightCeilPow2 (n shift : ℕ) : roundShiftRightEven n shift ≤ shiftRightCeilPow2 n shift

Nearest-even rounding is bounded above by the “ceiling quotient” shiftRightCeilPow2.

This is useful when connecting nearest-even rounding to directed rounding up, since the latter is often implemented as “divide by 2^k and round the quotient up”.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.pred_mul_pow2_lt_of_roundShiftRightEven_eq (n shift r : ℕ) (hr : roundShiftRightEven n shift = r) (hrpos : 0 < r) : (r - 1) * pow2 shift < n

If nearest-even shift rounding returns the positive integer r, then the unrounded numerator is strictly larger than (r - 1) * 2^shift.

The strict inequality matters at the top of the binary32 range: a rounded significand of 2^24 must come from a value strictly above the largest 24-bit significand 2^24 - 1.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.shiftRight_le_roundShiftRightEven_le_shiftRightCeilPow2 (n shift : ℕ) : n.shiftRight shift ≤ roundShiftRightEven n shift ∧ roundShiftRightEven n shift ≤ shiftRightCeilPow2 n shift

Convenience bundling of the lower+upper bounds used most often downstream.