Total FP32 Bridge: Ordering

This module relates executable IEEE comparisons to real order when the operands are finite. It keeps unordered NaN cases explicit rather than coercing every bit pattern into ℝ; signed zeros, which have distinct encodings but equal real values, are handled by the IEEE comparison rules.

See FP32Total.Core for the total bridge convention and references.

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.