minimum/maximum in EReal semantics (IEEE32Exec)

NN/Floats/IEEEExec/Exec32.lean defines executable IEEE-754 comparison operators:

• compare (unordered if either operand is NaN),
• minimum / maximum (NaNs propagate; tie-break on signed zeros).

For interval endpoint soundness, we interpret float32 values in the extended reals:

• finite values map to ↑(toReal x),
• +∞ / -∞ map to ⊤ / ⊥,
• NaN is excluded by assumption (the theorems below assume isNaN = false).

This file provides the bridge lemmas used by interval arithmetic proofs:

$$ \begin{aligned} \operatorname{toEReal}(\min(x,y)) &=\min(\operatorname{toEReal}(x),\operatorname{toEReal}(y)),\\ \operatorname{toEReal}(\max(x,y)) &=\max(\operatorname{toEReal}(x),\operatorname{toEReal}(y)). \end{aligned} $$

including the overflow cases where one of x/y is an infinity.

References:

• IEEE 754-2019: doi:10.1109/IEEESTD.2019.8766229
• Goldberg (1991): doi:10.1145/103162.103163

Main bridge lemmas

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_minimum_eq_min (x y : IEEE32Exec) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.minimum y).toEReal = min x.toEReal y.toEReal

minimum agrees with min on the toEReal interpretation, assuming no NaNs.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_maximum_eq_max (x y : IEEE32Exec) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.maximum y).toEReal = max x.toEReal y.toEReal

maximum agrees with max on the toEReal interpretation, assuming no NaNs.