IEEE32Exec and FP32: Dyadic Rounder Correctness

Signed zeros

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_signedZero (s : Bool) : (if s = true then negZero else posZero).toReal = 0

Both +0 and -0 decode to the real number 0.

IEEE-754 has signed zeros because they matter for some operations (notably division and some transcendentals). Our finite FP32 model treats them as equal at the real level, and the bridge lemmas in this file use this fact repeatedly.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_posZero : posZero.toReal = 0

+0 decodes to the real number 0.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_negZero : negZero.toReal = 0

-0 decodes to the real number 0.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_roundDyadicToIEEE32_of_abs_le_ieeeMaxFinite (d : Dyadic) (hbound : |dyadicToReal d| ≤ FP32.ieeeMaxFinite) : (roundDyadicToIEEE32 d).isFinite = true

Nearest-even rounding of a dyadic whose magnitude is at most the largest finite binary32 value cannot overflow.

The initial exponent guard is ruled out by the lower log2 magnitude bound. At exponent 127, the only remaining overflow path is a carry from a rounded 24-bit significand; that carry implies that the exact significand was strictly larger than 2^24 - 1, contradicting hbound.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_roundDyadicToIEEE32_eq_fp32Round (d : Dyadic) (hfin : (roundDyadicToIEEE32 d).isFinite = true) : (roundDyadicToIEEE32 d).toReal = fp32Round (dyadicToReal d)

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

The hypothesis isFinite (roundDyadicToIEEE32 d) = true rules out the overflow-to-±Inf branches.