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 six directions therefore returns a finite value with the same real denotation, and such a value is never a grid tie (dyadicIsGridTie_eq_false_of_eq_mul_pow2).

Internal.Directed.roundDyadic_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, by 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.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_le_maxFiniteExpField_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) : x.expField ≤ fmt.maxFiniteExpField

A finite word's exponent field is at most maxFiniteExpField. An IEEE encoding reserves the all-ones field for infinities and NaNs, and the other encodings use every field for finite values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_lt_bpow_of_toDyadic?_some {fmt : FloatFormat} (x : Model fmt) {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) : |d.toReal| < bpow (fmt.maxNormalExponent + 1)

Every decoded finite value lies strictly below 2^(maxNormalExponent + 1) in magnitude, whatever the descriptor's encoding.

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.shiftRightCeil_mul_pow2_of_le (m shift k : ℕ) (hshift : shift ≤ k) : Numerics.shiftRightCeil (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.dyadicIsGridTie_eq_false_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) : dyadicIsGridTie fmt d = false

A representable dyadic is never a grid tie: every bit below its grid spacing is clear, so the discarded bits are never one half of a unit.

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.Internal.Directed.roundDyadic_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) : (roundDyadic fmt mode d).isFinite = true ∧ (roundDyadic fmt mode d).toReal = d.toReal

Every 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.Internal.Directed.roundDyadic_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) : (roundDyadic fmt mode d).isFinite = true ∧ (roundDyadic fmt mode d).toReal = d.toReal

Every 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 Internal.Directed.roundDyadic_of_representable, this clears the overflow indicator of dyadicRoundingStatus for exactly representable results.

Exact reconstruction of finite representations

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cexp_toDyadic? {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) (hm : d.significand ≠ 0) : Flocq.cexp Numerics.binaryRadix (fexpOf fmt) d.toReal = d.exponent

A nonzero decoded dyadic already uses the format's canonical exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_exponent_eq_of_toReal_eq {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hx0 : dx.significand ≠ 0) (hy0 : dy.significand ≠ 0) (hvalue : x.toReal = y.toReal) : dx.exponent = dy.exponent

Equal nonzero numerical values have the same canonical decoded exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_eq_zero_iff (d : Numerics.Dyadic) : d.toReal = 0 ↔ d.significand = 0

A dyadic denotes zero exactly when its unsigned coefficient is zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.eq_of_toReal_eq_of_nonzero {fmt : FloatFormat} {x y : Model fmt} (hx : x.isFinite = true) (hy : y.isFinite = true) (hvalue : x.toReal = y.toReal) (hzero : x.toReal ≠ 0) : x = y

Equal nonzero finite real values determine the complete binary word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundDyadic_toDyadic?_of_nonzero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) (hm : d.significand ≠ 0) : roundDyadic fmt mode d = x

In a conventional IEEE format, rounding a decoded nonzero value restores its word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundDyadic_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) (negative : Bool) (exponent : ℤ) : roundDyadic fmt mode { negative := negative, significand := 0, exponent := exponent } = zero fmt negative

In a conventional IEEE format, rounding an exact zero preserves its sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundDyadic_toDyadic? {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) : roundDyadic fmt mode d = x

In a conventional IEEE format, rounding a decoded finite dyadic restores its complete word.