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.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.