Basic lemmas for format-parameterized directed rounding

Shared arithmetic facts support both directed dyadic and rational rounding proofs. Further lemmas give closed forms for the smallest positive subnormal and a strict power-of-two bound for the largest finite value. All statements are uniform in FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_le_pow2_succ (exponent : ℕ) : pow2 exponent ≤ pow2 (exponent + 1)

Increasing a natural exponent by one does not decrease its power of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_pos (exponent : ℕ) : 0 < pow2 exponent

Natural powers of two are positive.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_lt_pow2_succ (exponent : ℕ) : pow2 exponent < pow2 (exponent + 1)

Natural powers of two grow strictly with the exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_add (left right : ℕ) : pow2 (left + right) = pow2 left * pow2 right

Split a natural power of two across an exponent sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_mul (left right : ℕ) : pow2 left * pow2 right = pow2 (left + right)

Multiplicative form of pow2_add.

Floor and ceiling shifts

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.shiftRight_mul_pow2_le (n shift : ℕ) : n.shiftRight shift * pow2 shift ≤ n

Shifting right and restoring the removed power of two cannot exceed the original number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_shiftRightCeilPow2_mul_pow2 (n shift : ℕ) : n ≤ shiftRightCeilPow2 n shift * pow2 shift

A ceiling right shift, followed by restoration of its scale, covers the original number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.shiftRightCeilPow2_le_shiftRight_add_one (n shift : ℕ) : shiftRightCeilPow2 n shift ≤ n.shiftRight shift + 1

A ceiling shift is at most one larger than the corresponding floor shift.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.shiftRight_le_shiftRightCeilPow2 (n shift : ℕ) : n.shiftRight shift ≤ shiftRightCeilPow2 n shift

A floor right shift never exceeds the corresponding ceiling right shift.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_log2_le {n : ℕ} (hn : n ≠ 0) : pow2 n.log2 ≤ n

The leading power of two does not exceed a nonzero natural number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.lt_pow2_log2_add_one {n : ℕ} (hn : n ≠ 0) : n < pow2 (n.log2 + 1)

A nonzero natural number is below the next power after its leading bit.

Format constants

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minSubnormalExponent_lt_minNormalExponent (fmt : FloatFormat) : fmt.minSubnormalExponent < fmt.minNormalExponent

The subnormal grid starts strictly below the smallest normal exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minSubnormalExponent_add_fracWidth (fmt : FloatFormat) : fmt.minSubnormalExponent + Int.ofNat fmt.fracWidth = fmt.minNormalExponent

The subnormal exponent plus the explicit fraction width is the minimum normal exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.posMinSubnormal_eq_ofFields (fmt : FloatFormat) : posMinSubnormal fmt = ofFields fmt false 0 1

The smallest positive subnormal is explicit field packing with fraction one.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_posMinSubnormal (fmt : FloatFormat) : (posMinSubnormal fmt).toReal = bpow fmt.minSubnormalExponent

The smallest positive subnormal denotes one unit at the minimum subnormal exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_posMaxFinite (fmt : FloatFormat) : (posMaxFinite fmt).toReal = ↑(pow2 fmt.fracWidth + fmt.maxFiniteFracField) * bpow (fmt.maxNormalExponent - Int.ofNat fmt.fracWidth)

Closed form for the largest finite positive value of an arbitrary format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_signed_mul_bpow_le_toReal_posMaxFinite (fmt : FloatFormat) (sign : Bool) (mantissa : ℕ) (exponent : ℤ) (hmantissa : mantissa ≤ pow2 fmt.fracWidth + fmt.maxFiniteFracField) (hexponent : exponent ≤ fmt.maxNormalExponent - Int.ofNat fmt.fracWidth) : |(if sign = true then -1 else 1) * ↑mantissa * bpow exponent| ≤ (posMaxFinite fmt).toReal

A signed magnitude whose mantissa and exponent do not exceed those of the largest finite value is bounded by that value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_le_posMaxFinite_of_isIEEE_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) : |x.toReal| ≤ (posMaxFinite fmt).toReal

Every finite IEEE value lies between the two largest-finite endpoints.

The finiteness hypothesis excludes infinities and NaNs; the bound follows from the descriptor's exponent and fraction fields.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_posMaxFinite_lt_bpow (fmt : FloatFormat) : (posMaxFinite fmt).toReal < bpow (fmt.maxNormalExponent + 1)

The largest finite value is strictly below the next normal power of two.