Quotient and exponent semantics

Exact rational rounding reduces to an integer quotient after a power-of-two rescaling. This module proves bounds for small quotients and relates the scaled leading exponent to the order of the numerator and denominator. It also identifies the subnormal and normal grid exponents used by roundAt.

These lemmas supply the bounds and exponent identities used by the nearest-even packing proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_eq_zero_of_two_mul_le (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) (hhalf : 2 * numerator ≤ denominator) : Numerics.roundQuotientEven numerator denominator = 0

A quotient at or below one half rounds to the even integer zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_le_one_of_lt (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hlt : numerator < denominator) : Numerics.roundQuotientEven numerator denominator ≤ 1

A positive proper fraction rounds to either zero or one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleByPowerOfTwo_fst_lt_snd_of_neg_log (numerator denominator : ℕ) (shift : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hnegative : Numerics.RationalBinary.floorLog2 numerator denominator + shift < 0) : (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator shift).1 < (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator shift).2

If a scaled rational's leading exponent is negative, its scaled numerator is strictly smaller than its denominator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_scaled_eq_zero (numerator denominator : ℕ) (shift : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hsmall : Numerics.RationalBinary.floorLog2 numerator denominator + shift < -1) : Numerics.roundQuotientEven (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator shift).1 (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator shift).2 = 0

Values whose scaled leading exponent is below -1 are strictly below one half of a grid unit and therefore round to zero under nearest-even.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_subnormal_le (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hlow : fmt.minSubnormalExponent ≤ Numerics.RationalBinary.floorLog2 numerator denominator + exponent) (hhigh : Numerics.RationalBinary.floorLog2 numerator denominator + exponent < fmt.minNormalExponent) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp); Numerics.roundQuotientEven scaled.1 scaled.2 ≤ pow2 fmt.fracWidth

Nearest-even subnormal-path rounding is at most the smallest normal mantissa.

Format exponent selection

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_normalMantissaExpOffset_eq_minSubnormalExponent_sub_one (fmt : FloatFormat) : -Int.ofNat fmt.normalMantissaExpOffset = fmt.minSubnormalExponent - 1

The nearest-even implementation's half-min-subnormal cutoff in semantic form.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf_total_eq_minSubnormal (fmt : FloatFormat) (totalExponent : ℤ) (hsubnormal : totalExponent < fmt.minNormalExponent) : fexpOf fmt (totalExponent + 1) = fmt.minSubnormalExponent

Values below the normal range use the descriptor's minimum-subnormal grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf_total_eq_normal (fmt : FloatFormat) (totalExponent : ℤ) (hnormal : fmt.minNormalExponent ≤ totalExponent) : fexpOf fmt (totalExponent + 1) = totalExponent - Int.ofNat fmt.fracWidth

Normal values use the descriptor's precision-shifted rounded-real grid.