IEEE32Exec and FP32: Nearest-Even Quotient Lemmas

Signed nearest-even (and power-of-two specialization)

FP32 uses “round to nearest, ties to even” (IEEE 754's default). The executable kernel implements the same policy, but at the level of integer arithmetic on mantissas.

In this section we establish basic algebraic properties of nearest-even rounding that we can reuse later when relating the IEEE32Exec rounding code to fp32Round.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_nearest_even_neg (x : ℝ) : neuralNearestEven (-x) = -neuralNearestEven x

Nearest-even integer rounding commutes with negation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_nearest_even_neg_div_eq_roundQuotEven (num den : ℕ) (hden : den ≠ 0) : neuralNearestEven (-(↑num / ↑den)) = -Int.ofNat (roundQuotEven num den)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.roundShiftRightEven_eq_roundQuotEven_pow2 (n shift : ℕ) : roundShiftRightEven n shift = roundQuotEven n (pow2 shift)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_nearest_even_div_pow2_eq_roundShiftRightEven (num shift : ℕ) : neuralNearestEven (↑num / ↑(pow2 shift)) = Int.ofNat (roundShiftRightEven num shift)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_nearest_even_sqrt_nat (n : ℕ) : neuralNearestEven √↑n = Int.ofNat (have q := n.sqrt; have r := n - q * q; if r > q then q + 1 else q)