Signed bounds for conventional IEEE directed dyadic rounding

The semantic contracts of roundDyadicDown and roundDyadicUp give outward bounds for signed dyadics. For every exact signed dyadic and conventional IEEE FloatFormat, executable downward rounding is an extended-real lower bound and executable upward rounding is an extended-real upper bound.

Infinities are handled by the positive-magnitude results. Negative inputs follow by swapping the magnitude rounders and reversing order under negation.

For every descriptor, the directed rounders, the nearest-even general rounder, and the packing helpers they share turn a nonnegative exact value into a value with a nonnegative real meaning. A value that is not finite denotes zero, which covers the NaN that a finite-unsigned-zero encoding delivers on overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nativeOverflow_true_eq_neg_false_of_isIEEE (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : nativeOverflow fmt true = (nativeOverflow fmt false).neg

Conventional IEEE overflow results of opposite signs are negations of each other.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicMagnitudeDown_true_eq_neg_false (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hsigned : fmt.supportsSignedZero = true) : roundDyadicMagnitudeDown fmt true mantissa exponent = (roundDyadicMagnitudeDown fmt false mantissa exponent).neg

When the format has signed zeros, rounding a magnitude downward and attaching a negative sign is the negation of the same rounded magnitude with a positive sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicMagnitudeUp_true_eq_neg_false (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hsigned : fmt.supportsSignedZero = true) (hoverflow : nativeOverflow fmt true = (nativeOverflow fmt false).neg) : roundDyadicMagnitudeUp fmt true mantissa exponent = (roundDyadicMagnitudeUp fmt false mantissa exponent).neg

When the format has signed zeros and sign-symmetric overflow results, rounding a magnitude upward and attaching a negative sign is the negation of the same rounded magnitude with a positive sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundDyadicDown_eq_false (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.isIEEE = true) : (roundDyadicDown fmt d).isNaN = false

Directed-down rounding of an exact signed dyadic never produces a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundDyadicUp_eq_false (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.isIEEE = true) : (roundDyadicUp fmt d).isNaN = false

Directed-up rounding of an exact signed dyadic never produces a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_roundDyadicDown_le (fmt : FloatFormat) (d : Numerics.Dyadic) : fmt.isIEEE = true → (roundDyadicDown fmt d).toEReal ≤ ↑d.toReal

Directed-down dyadic rounding never exceeds the exact signed dyadic value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_roundDyadicUp (fmt : FloatFormat) (d : Numerics.Dyadic) : fmt.isIEEE = true → ↑d.toReal ≤ (roundDyadicUp fmt d).toEReal

The exact signed dyadic value never exceeds directed-up dyadic rounding.

Nonnegative results of positive rounding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_eq_zero_of_isFinite_eq_false {fmt : FloatFormat} {x : Model fmt} (hfinite : x.isFinite = false) : x.toReal = 0

A value that is not finite denotes zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_nonneg_of_signBit_eq_false {fmt : FloatFormat} {x : Model fmt} (hsign : x.signBit = false) : 0 ≤ x.toReal

A value with a clear sign bit has a nonnegative real value, whether or not it is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_nativeOverflow_false_nonneg (fmt : FloatFormat) : 0 ≤ (nativeOverflow fmt false).toReal

The positive native overflow value has a nonnegative real value in every encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicMagnitudeDown_false_nonneg (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : 0 ≤ (roundDyadicMagnitudeDown fmt false mantissa exponent).toReal

Rounding a positive magnitude downward gives a nonnegative value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicMagnitudeUp_false_nonneg (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : 0 ≤ (roundDyadicMagnitudeUp fmt false mantissa exponent).toReal

Rounding a positive magnitude upward gives a nonnegative value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicGeneral_nonneg (fmt : FloatFormat) (value : Numerics.Dyadic) (hvalue : value.negative = false) : 0 ≤ (roundDyadicGeneral fmt value).toReal

Nearest-even rounding of a nonnegative dyadic gives a nonnegative value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicUp_nonneg (fmt : FloatFormat) (value : Numerics.Dyadic) (hvalue : value.negative = false) : 0 ≤ (roundDyadicUp fmt value).toReal

Rounding a nonnegative dyadic upward gives a nonnegative value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicDown_nonneg (fmt : FloatFormat) (value : Numerics.Dyadic) (hvalue : value.negative = false) : 0 ≤ (roundDyadicDown fmt value).toReal

Rounding a nonnegative dyadic downward gives a nonnegative value.