Range-limited directed bounds for finite-only binary formats

Every word of an Encoding.finite descriptor denotes a finite real. Outward rounding therefore has a real enclosure contract exactly while the exact value lies between the largest negative and positive finite values. Unlike the IEEE theorem, no infinity is available outside that range.

These results are specific to Encoding.finite. Formats using Encoding.finiteMaxNaN or Encoding.finiteUnsignedZero reserve exceptional words and need their own boundary arguments.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicPosDown_le_of_encoding_finite (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hm : mantissa ≠ 0) : (roundDyadicPosDown fmt mantissa exponent).toReal ≤ ↑mantissa * bpow exponent

Positive downward rounding in a finite-only format is a real lower bound.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toReal_roundDyadicPosUp_of_encoding_finite (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hm : mantissa ≠ 0) (hbound : ↑mantissa * bpow exponent ≤ (posMaxFinite fmt).toReal) : ↑mantissa * bpow exponent ≤ (roundDyadicPosUp fmt mantissa exponent).toReal

Within the largest-finite range, positive upward rounding in a finite-only format is a real upper bound. Outside that range the executable operation saturates, so no such theorem is possible.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.supportsSignedZero_eq_true_of_encoding_finite (fmt : FloatFormat) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) : fmt.supportsSignedZero = true

Finite-only formats have signed zeros.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nativeOverflow_true_eq_neg_false_of_encoding_finite (fmt : FloatFormat) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) : nativeOverflow fmt true = (nativeOverflow fmt false).neg

Saturating overflow results of opposite signs are negations of each other.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicDown_le_of_encoding_finite (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : (roundDyadicDown fmt d).toReal ≤ d.toReal

Range-limited downward rounding of an exact dyadic is a real lower bound in a finite-only format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toReal_roundDyadicUp_of_encoding_finite (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : d.toReal ≤ (roundDyadicUp fmt d).toReal

Range-limited upward rounding of an exact dyadic is a real upper bound in a finite-only format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_addDown_le_of_encoding_finite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |x.toReal + y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.addDown y).toReal ≤ x.toReal + y.toReal

Range-limited downward addition is a real lower bound in a finite-only format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toReal_addUp_of_encoding_finite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |x.toReal + y.toReal| ≤ (posMaxFinite fmt).toReal) : x.toReal + y.toReal ≤ (x.addUp y).toReal

Range-limited upward addition is a real upper bound in a finite-only format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_subDown_le_of_encoding_finite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |x.toReal - y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.subDown y).toReal ≤ x.toReal - y.toReal

Range-limited downward subtraction is a real lower bound in a finite-only format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toReal_subUp_of_encoding_finite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |x.toReal - y.toReal| ≤ (posMaxFinite fmt).toReal) : x.toReal - y.toReal ≤ (x.subUp y).toReal

Range-limited upward subtraction is a real upper bound in a finite-only format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_mulDown_le_of_encoding_finite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |x.toReal * y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.mulDown y).toReal ≤ x.toReal * y.toReal

Range-limited downward multiplication is a real lower bound in a finite-only format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toReal_mulUp_of_encoding_finite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hbound : |x.toReal * y.toReal| ≤ (posMaxFinite fmt).toReal) : x.toReal * y.toReal ≤ (x.mulUp y).toReal

Range-limited upward multiplication is a real upper bound in a finite-only format.