Invalid flags for adjacency and number-preferring extrema

nextUp, nextDown, minimumNumber, and maximumNumber deliver a value without a status. With status := true they add the invalid indicator required for a signaling NaN operand by IEEE 754-2019 (§5.3.1 for the adjacent-value operations, §9.6 for the number-preferring selections). This module proves that the value is unchanged, that invalid is raised exactly for a signaling operand, and that no other indicator is set.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_nextUp {fmt : FloatFormat} (x : Model fmt) : (x.nextUp true).value = x.nextUp

nextUp with status := true delivers the value of nextUp.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_invalid {fmt : FloatFormat} (x : Model fmt) : (x.nextUp true).status.invalid = x.isSNaN

nextUp raises invalid exactly for a signaling NaN input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_status_eq {fmt : FloatFormat} (x : Model fmt) : (x.nextUp true).status = { invalid := x.isSNaN }

nextUp raises no indicator other than invalid.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_nextDown {fmt : FloatFormat} (x : Model fmt) : (x.nextDown true).value = x.nextDown

nextDown with status := true delivers the value of nextDown.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown_invalid {fmt : FloatFormat} (x : Model fmt) : (x.nextDown true).status.invalid = x.isSNaN

nextDown raises invalid exactly for a signaling NaN input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown_status_eq {fmt : FloatFormat} (x : Model fmt) : (x.nextDown true).status = { invalid := x.isSNaN }

nextDown raises no indicator other than invalid.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_minimumNumber {fmt : FloatFormat} (x y : Model fmt) : (x.minimumNumber y true).value = x.minimumNumber y

minimumNumber with status := true delivers the value of minimumNumber.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_invalid {fmt : FloatFormat} (x y : Model fmt) : (x.minimumNumber y true).status.invalid = (x.isSNaN || y.isSNaN)

minimumNumber raises invalid exactly when an operand is a signaling NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_status_eq {fmt : FloatFormat} (x y : Model fmt) : (x.minimumNumber y true).status = { invalid := x.isSNaN || y.isSNaN }

minimumNumber raises no indicator other than invalid.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_maximumNumber {fmt : FloatFormat} (x y : Model fmt) : (x.maximumNumber y true).value = x.maximumNumber y

maximumNumber with status := true delivers the value of maximumNumber.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_invalid {fmt : FloatFormat} (x y : Model fmt) : (x.maximumNumber y true).status.invalid = (x.isSNaN || y.isSNaN)

maximumNumber raises invalid exactly when an operand is a signaling NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_status_eq {fmt : FloatFormat} (x y : Model fmt) : (x.maximumNumber y true).status = { invalid := x.isSNaN || y.isSNaN }

maximumNumber raises no indicator other than invalid.