Invalid flags for adjacency and number-preferring extrema

nextUp, nextDown, minimumNumber, and maximumNumber deliver a value without a status. Their *WithStatus forms 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 and that invalid is raised exactly for a signaling operand; no other indicator is ever set.

@[simp]

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

The status form of nextUp delivers exactly nextUp.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUpWithStatus_invalid {fmt : FloatFormat} (x : Model fmt) : x.nextUpWithStatus.status.invalid = x.isSNaN

nextUpWithStatus raises invalid exactly for a signaling NaN input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUpWithStatus_status_eq {fmt : FloatFormat} (x : Model fmt) : x.nextUpWithStatus.status = { invalid := x.isSNaN }

nextUpWithStatus raises no indicator other than invalid.

@[simp]

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

The status form of nextDown delivers exactly nextDown.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDownWithStatus_invalid {fmt : FloatFormat} (x : Model fmt) : x.nextDownWithStatus.status.invalid = x.isSNaN

nextDownWithStatus raises invalid exactly for a signaling NaN input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDownWithStatus_status_eq {fmt : FloatFormat} (x : Model fmt) : x.nextDownWithStatus.status = { invalid := x.isSNaN }

nextDownWithStatus raises no indicator other than invalid.

@[simp]

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

The status form of minimumNumber delivers exactly minimumNumber.

@[simp]

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

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

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

minimumNumberWithStatus raises no indicator other than invalid.

@[simp]

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

The status form of maximumNumber delivers exactly maximumNumber.

@[simp]

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

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

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

maximumNumberWithStatus raises no indicator other than invalid.