Total optional observations of binary32 minimum and maximum

Finite operands use the real minimum and maximum contracts. NaNs propagate without a real observation, while positive infinity is neutral for minimum and negative infinity is neutral for maximum. The exceptional cases follow FloatLib's NaN selection and infinity comparison directly.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_minimum_eq_match_total (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?_minimum_eq_match_total._proof_3 toReal?_minimum_eq_match_total._proof_4 toReal?_minimum_eq_match_total._proof_5 toReal?_minimum_eq_match_total._proof_6) : toReal? (x ⊓ y) = match toReal? x, toReal? y with | some rx, some ry => some (min rx ry) | some rx, none => if (y.isInfinite && !y.signBit) = true then some rx else none | none, some ry => if (x.isInfinite && !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 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?_minimum_eq_match_total._proof_3 toReal?_minimum_eq_match_total._proof_4 toReal?_minimum_eq_match_total._proof_5 toReal?_minimum_eq_match_total._proof_6) : toReal? (x ⊔ y) = match toReal? x, toReal? y with | some rx, some ry => some (max rx ry) | some rx, none => if (y.isInfinite && y.signBit) = true then some rx else none | none, some ry => if (x.isInfinite && 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.