Rounding an exactly representable dyadic is the identity

For a descriptor with fmt.isIEEE = true, a dyadic m * 2^e whose significand fits in the precision, whose exponent is at least the minimum subnormal exponent, and whose magnitude is at most the largest finite value is exactly representable. Rounding it in any of the four IEEE directions therefore returns a finite value with exactly the same real denotation.

roundDyadicWithRounding_of_representable is the statement used by IEEE remainder (whose exact result is always representable) and by roundToIntegral (whose rounded integer is always representable for every IEEE interchange format). The finite decoded value of any word satisfies the three hypotheses; see toDyadic?_significand_lt and minSubnormalExponent_le_toDyadic?.

Bounds satisfied by every decoded finite value

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_significand_lt_and_minSubnormalExponent_le {fmt : FloatFormat} (x : Model fmt) {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) : d.significand < 2 ^ (fmt.fracWidth + 1) ∧ fmt.minSubnormalExponent ≤ d.exponent

The decoded dyadic of a word has a significand below 2^(fracWidth + 1) and an exponent no smaller than the minimum subnormal exponent. These bounds describe the format's precision and exponent grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_significand_lt {fmt : FloatFormat} (x : Model fmt) {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) : d.significand < 2 ^ (fmt.fracWidth + 1)

The decoded significand of a word fits in the format's precision.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minSubnormalExponent_le_toDyadic? {fmt : FloatFormat} (x : Model fmt) {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) : fmt.minSubnormalExponent ≤ d.exponent

The decoded exponent of a word is at least the minimum subnormal exponent.

Membership in the format grid

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.genericFormat_of_eq_mul_pow2 (fmt : FloatFormat) (d : Numerics.Dyadic) (m k : ℕ) (hsig : d.significand = m * 2 ^ k) (hm : m < 2 ^ (fmt.fracWidth + 1)) (hexp : fmt.minSubnormalExponent ≤ d.exponent) : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) d.toReal

A dyadic belongs to the gradual-underflow grid when its significand is m * 2^k with m below 2^(fracWidth + 1) and its exponent is at least the minimum subnormal exponent. The scaled form is what roundToIntegral produces when the input already has a nonnegative exponent, so the trailing zero bits must be allowed here. Dyadic.genericFormat_of_significand_lt is the unscaled special case.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.genericFormat_of_significand_lt (fmt : FloatFormat) (d : Numerics.Dyadic) (hsig : d.significand < 2 ^ (fmt.fracWidth + 1)) (hexp : fmt.minSubnormalExponent ≤ d.exponent) : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) d.toReal

A dyadic whose significand fits in the precision and whose exponent is at least the minimum subnormal exponent belongs to the descriptor's Flocq grid. No magnitude bound is needed because the grid has no upper exponent limit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_maxFiniteDyadic (fmt : FloatFormat) : (maxFiniteDyadic fmt).toReal = (posMaxFinite fmt).toReal

The exact value of the largest finite word, as a dyadic, denotes the same real.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.leadingExponent_le_maxNormalExponent (fmt : FloatFormat) (d : Numerics.Dyadic) (hm : d.significand ≠ 0) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : ↑d.significand.log2 + d.exponent ≤ fmt.maxNormalExponent

The leading binary exponent of a nonzero dyadic within the largest finite magnitude does not exceed the largest normal exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.shiftRightCeilPow2_mul_pow2_of_le (m shift k : ℕ) (hshift : shift ≤ k) : shiftRightCeilPow2 (m * 2 ^ k) shift = m * 2 ^ (k - shift)

Ceiling division of a multiple of 2^shift by 2^shift is exact.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaToLeadingBitUp_ne_pow2_succ_of_eq_mul_pow2 (m k fracWidth : ℕ) (hm : m ≠ 0) (hsig : m < 2 ^ (fracWidth + 1)) : roundMantissaToLeadingBitUp (m * 2 ^ k) fracWidth ≠ pow2 (fracWidth + 1)

Normalizing a significand of the form m * 2^k with m in precision never carries into the next binade: the shift discards only zero bits or the value already fits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaToLeadingBitUp_ne_pow2_succ_of_lt (mantissa fracWidth : ℕ) (hm : mantissa ≠ 0) (hsig : mantissa < 2 ^ (fracWidth + 1)) : roundMantissaToLeadingBitUp mantissa fracWidth ≠ pow2 (fracWidth + 1)

Normalizing a significand that already fits in the precision never carries.

Exact rounding, one direction at a time

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic_of_representable (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (d : Numerics.Dyadic) (m k : ℕ) (hsig : d.significand = m * 2 ^ k) (hm : m < 2 ^ (fmt.fracWidth + 1)) (hexp : fmt.minSubnormalExponent ≤ d.exponent) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : (roundDyadic fmt d).isFinite = true ∧ (roundDyadic fmt d).toReal = d.toReal

Nearest-even rounding of a representable dyadic returns a finite word with the same real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicPosDown_of_representable (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (m k : ℕ) (exponent : ℤ) (hm0 : m ≠ 0) (hm : m < 2 ^ (fmt.fracWidth + 1)) (hexp : fmt.minSubnormalExponent ≤ exponent) (hmax : ↑(m * 2 ^ k).log2 + exponent ≤ fmt.maxNormalExponent) : (roundDyadicPosDown fmt (m * 2 ^ k) exponent).isFinite = true ∧ (roundDyadicPosDown fmt (m * 2 ^ k) exponent).toReal = ↑(m * 2 ^ k) * bpow exponent

Downward rounding of a representable positive magnitude is exact and finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicPosUp_of_representable (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (m k : ℕ) (exponent : ℤ) (hm0 : m ≠ 0) (hm : m < 2 ^ (fmt.fracWidth + 1)) (hexp : fmt.minSubnormalExponent ≤ exponent) (hmax : ↑(m * 2 ^ k).log2 + exponent ≤ fmt.maxNormalExponent) : (roundDyadicPosUp fmt (m * 2 ^ k) exponent).isFinite = true ∧ (roundDyadicPosUp fmt (m * 2 ^ k) exponent).toReal = ↑(m * 2 ^ k) * bpow exponent

Upward rounding of a representable positive magnitude is exact and finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicWithRounding_of_eq_mul_pow2 (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) (d : Numerics.Dyadic) (m k : ℕ) (hsig : d.significand = m * 2 ^ k) (hm : m < 2 ^ (fmt.fracWidth + 1)) (hexp : fmt.minSubnormalExponent ≤ d.exponent) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : (roundDyadicWithRounding fmt mode d).isFinite = true ∧ (roundDyadicWithRounding fmt mode d).toReal = d.toReal

Every IEEE rounding direction fixes an exactly representable dyadic: the result is finite and its real value is the dyadic's own value. The significand may carry trailing zero bits beyond the precision, as m * 2^k.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicWithRounding_of_representable (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) (d : Numerics.Dyadic) (hsig : d.significand < 2 ^ (fmt.fracWidth + 1)) (hexp : fmt.minSubnormalExponent ≤ d.exponent) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : (roundDyadicWithRounding fmt mode d).isFinite = true ∧ (roundDyadicWithRounding fmt mode d).toReal = d.toReal

Every IEEE rounding direction fixes an exactly representable dyadic whose significand fits in the precision: the result is finite and its real value is the dyadic's own value.

Overflow classification of representable dyadics

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingOverflows_eq_false_of_abs_toReal_le_posMaxFinite (fmt : FloatFormat) (mode : IEEERoundingMode) (d : Numerics.Dyadic) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : dyadicRoundingOverflows fmt mode d = false

No rounding direction classifies a dyadic within the largest finite magnitude as overflowing. Together with roundDyadicWithRounding_of_representable, this clears the overflow indicator of dyadicRoundingStatus for exactly representable results.