BridgeFP32Total

“Total” bridge theorems combining:

• IEEE32Exec's proved NaN/Inf propagation rules, and
• the FP32-on-ℝ refinement theorems for the finite/no-overflow branch (BridgeFP32.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.

Per-op “finite branch” wrappers (hide dyadic witnesses)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round_of_isFinite (x y : IEEE32Exec) (hfin : (x.add y).isFinite = true) : (x.add y).toReal = fp32Round (x.toReal + y.toReal)

Addition refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_fp32Round_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.sub y).isFinite = true) : (x.sub y).toReal = fp32Round (x.toReal - y.toReal)

Subtraction refinement packaged for total reasoning (hide dyadic witnesses).

This is the “finite-path” wrapper around BridgeFP32.toReal_sub_eq_fp32Round, replacing explicit toDyadic? witnesses with the more user-facing finiteness hypotheses.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_eq_fp32Round_of_isFinite (x y : IEEE32Exec) (hfin : (x.mul y).isFinite = true) : (x.mul y).toReal = fp32Round (x.toReal * y.toReal)

Multiplication refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_eq_fp32Round_of_isFinite (x y z : IEEE32Exec) (hfin : (x.fma y z).isFinite = true) : (x.fma y z).toReal = fp32Round (x.toReal * y.toReal + z.toReal)

Fused multiply-add refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_eq_fp32Round_of_isFinite (x : IEEE32Exec) (hfin : x.sqrt.isFinite = true) : x.sqrt.toReal = fp32Round √x.toReal

Square-root refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_fp32Round_of_isFinite (x y : IEEE32Exec) (hfin : (x.div y).isFinite = true) : (x.div y).toReal = fp32Round (x.toReal / y.toReal)

Division refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_minimum_eq_min_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.minimum y).toReal = min x.toReal y.toReal

On finite values, IEEE-754 minimum agrees with real min.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_maximum_eq_max_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.maximum y).toReal = max x.toReal y.toReal

On finite values, IEEE-754 maximum agrees with real max.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_lt_iff_toReal_lt_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.compare y = some Ordering.lt ↔ x.toReal < y.toReal

On finite values, compare x y = some .lt iff toReal x < toReal y.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_eq_iff_toReal_eq_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.compare y = some Ordering.eq ↔ x.toReal = y.toReal

On finite values, compare x y = some .eq iff toReal x = toReal y.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_gt_iff_toReal_gt_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.compare y = some Ordering.gt ↔ y.toReal < x.toReal

On finite values, compare x y = some .gt iff toReal y < toReal x.

“Both” view: toReal? semantics as an ite

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_add_eq_ite (x y : IEEE32Exec) : (x.add y).toReal? = if (x.add y).isFinite = true then some (fp32Round (x.toReal + y.toReal)) else none

toReal? (add x y) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_mul_eq_ite (x y : IEEE32Exec) : (x.mul y).toReal? = if (x.mul y).isFinite = true then some (fp32Round (x.toReal * y.toReal)) else none

toReal? (mul x y) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_fma_eq_ite (x y z : IEEE32Exec) : (x.fma y z).toReal? = if (x.fma y z).isFinite = true then some (fp32Round (x.toReal * y.toReal + z.toReal)) else none

toReal? (fma x y z) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_sqrt_eq_ite (x : IEEE32Exec) : x.sqrt.toReal? = if x.sqrt.isFinite = true then some (fp32Round √x.toReal) else none

toReal? (sqrt x) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_div_eq_ite (x y : IEEE32Exec) : (x.div y).toReal? = if (x.div y).isFinite = true then some (fp32Round (x.toReal / y.toReal)) else none

toReal? (div x y) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_minimum_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.minimum y).isFinite = true

minimum of two finite values is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_minimum_eq_min_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.minimum y).toReal? = some (min x.toReal y.toReal)

On finite inputs, toReal? (minimum x y) returns some (min (toReal x) (toReal y)).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_maximum_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.maximum y).isFinite = true

maximum of two finite values is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_maximum_eq_max_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.maximum y).toReal? = some (max x.toReal y.toReal)

On finite inputs, toReal? (maximum x y) returns some (max (toReal x) (toReal y)).

Total packaging for minimum/maximum (covers ±Inf)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_minimum_eq_match_total (x y : IEEE32Exec) : (x.minimum y).toReal? = match x.toReal?, y.toReal? with | some rx, some ry => some (min rx ry) | some rx, none => if (y.isInf && !y.signBit) = true then some rx else none | none, some ry => if (x.isInf && !x.signBit) = true then some ry else none | none, none => none

Total characterization of toReal? (minimum x y) via toReal? x and toReal? y.

This lemma covers the cases where one side is +∞ (which acts as a neutral element for min) and the cases where toReal? is none because of NaN.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_maximum_eq_match_total (x y : IEEE32Exec) : (x.maximum y).toReal? = match x.toReal?, y.toReal? with | some rx, some ry => some (max rx ry) | some rx, none => if (y.isInf && y.signBit) = true then some rx else none | none, some ry => if (x.isInf && x.signBit) = true then some ry else none | none, none => none

Total characterization of toReal? (maximum x y) via toReal? x and toReal? y.

This lemma covers the cases where one side is -∞ (which acts as a neutral element for max) and the cases where toReal? is none because of NaN.