Total FP32 Bridge: Finite and Special Values

“Total” bridge theorems combining:

• IEEE32Exec's proved NaN/Inf propagation rules, and
• the FP32-on-ℝ refinement theorems for the finite/no-overflow branch (NN/Floats/IEEEExec/Bridge/FP32.lean).

The key end-user view is toReal?:

• toReal? x = none for NaN/Inf,
• toReal? x = some r for finite values, with r : ℝ.

In most of TorchLean, the finite path is treated as real arithmetic + float32 rounding while special-value behavior is kept explicit. This file packages that split in one place.

The per-op lemmas are phrased in the style:

toReal? (op …) = if isFinite (op …) then some (fp32Round …) else none.

That makes the trust boundary readable at the call site: the if is exactly where NaN/Inf (or overflow-to-Inf) can occur.

Background references (for float32 rounding/special values):

• IEEE 754-2019: https://doi.org/10.1109/IEEESTD.2019.8766229
• Goldberg (1991): https://doi.org/10.1145/103162.103163
• Flocq (Boldo–Melquiond, 2011): https://doi.org/10.1109/ARITH.2011.40

Basic facts: isFinite ↔ toDyadic?/toReal?

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_eq_false_of_toDyadic?_eq_none (x : IEEE32Exec) (hx : x.toDyadic? = none) : x.isFinite = false

toDyadic? x = none implies x is not finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_eq_none_of_isFinite_eq_false (x : IEEE32Exec) (hx : x.isFinite = false) : x.toDyadic? = none

If x is not finite, then toDyadic? x = none.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_eq_none_of_isFinite_eq_false (x : IEEE32Exec) (hx : x.isFinite = false) : x.toReal? = none

toReal? returns none on non-finite values.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_eq_some_toReal_of_isFinite_eq_true (x : IEEE32Exec) (hx : x.isFinite = true) : x.toReal? = some x.toReal

On finite values, toReal? x is just some (toReal x).

Helpers: NaN/Inf/zero interactions

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isInf_eq_false_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) : x.isInf = false

NaNs are not infinities.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isZero_eq_false_of_isInf (x : IEEE32Exec) (hx : x.isInf = true) : x.isZero = false

Infinities are not zeros.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isInf_eq_true_of_toDyadic?_eq_none_of_isNaN_eq_false (x : IEEE32Exec) (hx : x.toDyadic? = none) (hxNaN : x.isNaN = false) : x.isInf = true

If dyadic decoding fails and the value is not NaN, then it must be infinite.