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.

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.