Total FP32 Bridge: Minimum and Maximum

IEEE minimum and maximum are not ordinary real min and max on every bit pattern: NaNs and signed zero require explicit rules. This module proves the rounded-real equations on finite inputs and records the exceptional branches through toReal?, using the special-value semantics from the core bridge.

See FP32Total.Core for the common finite/special-value convention.

Total minimum and maximum (including infinities)

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.