Bounds for positive directed dyadic rounding

Positive executable dyadic rounding satisfies lower and upper bounds and agrees with real floor or ceiling rounding in the stated finite cases. Downward overflow saturates at the largest finite value, while upward overflow produces positive infinity.

The proofs separate underflow, subnormal, normal, and normalization-carry regimes. The public results hide those packing details behind real and extended-real bounds. Formats without infinity need range-limited upper-bound theorems instead: after finite saturation, no encoded value can bound an arbitrarily large exact input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicPosDown_eq_roundAt_of_le_max (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hm : mantissa ≠ 0) (hmax : ↑mantissa.log2 + exponent ≤ fmt.maxNormalExponent) : (roundDyadicPosDown fmt mantissa exponent).toReal = roundAtDown fmt (↑mantissa * bpow exponent)

Below positive overflow, executable downward dyadic rounding equals independent real floor rounding on the format grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadicPosDown_le (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hm : mantissa ≠ 0) : (roundDyadicPosDown fmt mantissa exponent).toReal ≤ ↑mantissa * bpow exponent

Positive executable downward dyadic rounding never exceeds the exact real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_roundDyadicPosDown (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) : (roundDyadicPosDown fmt mantissa exponent).isFinite = true

Positive downward dyadic rounding always produces a finite value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundDyadicPosDown_eq_false (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) : (roundDyadicPosDown fmt mantissa exponent).isNaN = false

Positive downward dyadic rounding is never classified as NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_roundDyadicPosDown_le (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hm : mantissa ≠ 0) : (roundDyadicPosDown fmt mantissa exponent).toEReal ≤ ↑↑mantissa * ↑(bpow exponent)

Positive downward dyadic rounding is a lower bound in the extended reals.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicPosUp_eq_posInf_or_finite_roundAt (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hm : mantissa ≠ 0) : roundDyadicPosUp fmt mantissa exponent = posInf fmt ∨ (roundDyadicPosUp fmt mantissa exponent).isFinite = true ∧ (roundDyadicPosUp fmt mantissa exponent).toReal = roundAtUp fmt (↑mantissa * bpow exponent)

Positive upward dyadic rounding is either positive infinity or the finite independent real ceiling on the format grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicPosUp_finite_roundAt_of_le_max_of_no_carry (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hm : mantissa ≠ 0) (hmax : ↑mantissa.log2 + exponent ≤ fmt.maxNormalExponent) (hnoCarry : roundMantissaToLeadingBitUp mantissa fmt.fracWidth ≠ pow2 (fmt.fracWidth + 1)) : (roundDyadicPosUp fmt mantissa exponent).isFinite = true ∧ (roundDyadicPosUp fmt mantissa exponent).toReal = roundAtUp fmt (↑mantissa * bpow exponent)

Positive upward dyadic rounding is finite and equals the real ceiling on the format grid whenever the leading exponent is within range and normalizing the mantissa does not carry into the next binade. The carry hypothesis is what separates this statement from roundDyadicPosUp_eq_posInf_or_finite_roundAt: an exactly representable input never carries, so it can never overflow under upward rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundDyadicPosUp_eq_false (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hm : mantissa ≠ 0) : (roundDyadicPosUp fmt mantissa exponent).isNaN = false

Positive upward dyadic rounding is never classified as NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_roundDyadicPosUp (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hm : mantissa ≠ 0) : ↑↑mantissa * ↑(bpow exponent) ≤ (roundDyadicPosUp fmt mantissa exponent).toEReal

Positive upward dyadic rounding is an upper bound in the extended reals.