IEEE32Exec and FP32: Rational Rounder Correctness

Rounding rationals (finite/no-overflow)

Some operations (notably division and parts of transcendental approximations) naturally produce rationals num / den. The executable kernel rounds those rationals to float32 by:

• classifying magnitude (normal/subnormal/underflow/overflow),
• computing a scaled mantissa,
• applying nearest-even,
• and assembling the output bits.

This section connects that algorithm to the FP32 real rounding model.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_magnitude_signedRat (sign : Bool) (num den : ℕ) (hnum : num ≠ 0) (hden : den ≠ 0) : neuralMagnitude binaryRadix ((if sign = true then -1 else 1) * (↑num / ↑den)) = floorLog2Rat num den + 1

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_roundRatToIEEE32_eq_fp32Round (sign : Bool) (num den : ℕ) (hden : den ≠ 0) (hfin : (roundRatToIEEE32 sign num den).isFinite = true) : (roundRatToIEEE32 sign num den).toReal = fp32Round ((if sign = true then -1 else 1) * (↑num / ↑den))

Refinement theorem (finite/no-overflow): rounding an exact rational with the executable IEEE32 kernel agrees with the Flocq-style FP32 rounding-on-ℝ model.

The hypothesis isFinite (roundRatToIEEE32 sign num den) = true rules out the overflow-to-±Inf branches.