Nearest-even rounding of positive rational numbers

Lean's logical floating-point model represents an inexact quotient by its integer quotient and an Accuracy value computed from the remainder. Model.roundRatScaled rounds the same rational after moving a binary exponent into its numerator or denominator. This module proves that those representations remain equivalent through model normalization.

All results are independent of a particular floating-point format.

Quotient bounds

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_false_le_roundQuotientEven_le_true (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuotDirected false numerator denominator ≤ Numerics.roundQuotientEven numerator denominator ∧ Numerics.roundQuotientEven numerator denominator ≤ roundQuotDirected true numerator denominator

Nearest-even quotient rounding lies between the directed floor and ceiling rounders.

The nonzero-denominator premise is essential: at denominator zero and positive numerator, both directed rounders return zero but nearest-even quotient rounding returns one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_normal_bounds (fmt : FloatFormat) (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent); pow2 fmt.fracWidth ≤ Numerics.roundQuotientEven scaled.1 scaled.2 ∧ Numerics.roundQuotientEven scaled.1 scaled.2 ≤ pow2 (fmt.fracWidth + 1)

Nearest-even normal-path rounding stays within the normalized mantissa interval.

def FloatLib.Floats.Formats.BinaryInterchange.Model.quotientExtendedMantissa (numerator denominator : ℕ) : Float.Model.UnpackedFloat.ExtendedMantissa

The integer quotient and remainder accuracy used to round numerator / denominator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.accuracyOfFraction_mul_right (remainder denominator factor : ℕ) (hfactor : factor ≠ 0) : Float.Model.UnpackedFloat.accuracyOfFraction (remainder * factor) (denominator * factor) = Float.Model.UnpackedFloat.accuracyOfFraction remainder denominator

Multiplying the remainder and denominator by a common nonzero factor preserves accuracy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.quotientExtendedMantissa_mul_right (numerator denominator factor : ℕ) (hfactor : factor ≠ 0) : quotientExtendedMantissa (numerator * factor) (denominator * factor) = quotientExtendedMantissa numerator denominator

A common nonzero scale factor does not change a quotient's extended mantissa.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_eq_of_rat_eq (numerator denominator numerator' denominator' : ℕ) (hdenominator : denominator ≠ 0) (hdenominator' : denominator' ≠ 0) (hvalue : ↑numerator / ↑denominator = ↑numerator' / ↑denominator') : Numerics.roundQuotientEven numerator denominator = Numerics.roundQuotientEven numerator' denominator'

Nearest-even quotient rounding depends only on the represented nonnegative rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_scaleByPowerOfTwo_add (numerator denominator : ℕ) (firstExponent secondExponent : ℤ) (hdenominator : denominator ≠ 0) : have first := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator firstExponent; have second := Numerics.RationalBinary.scaleByPowerOfTwo first.1 first.2 secondExponent; have combined := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (firstExponent + secondExponent); Numerics.roundQuotientEven second.1 second.2 = Numerics.roundQuotientEven combined.1 combined.2

Successive exact binary scalings may be combined before nearest-even rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_mul_pow2_den (numerator denominator shift : ℕ) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (-Int.ofNat shift); Numerics.roundQuotientEven numerator (denominator * 2 ^ shift) = Numerics.roundQuotientEven scaled.1 scaled.2

Scaling a denominator by 2 ^ shift is exact binary scaling by 2 ^ (-shift).

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotientEven_shift_to_exponent (numerator denominator : ℕ) (exponent targetExponent : ℤ) (hdenominator : denominator ≠ 0) (hexponent : exponent ≤ targetExponent) : have shift := (targetExponent - exponent).toNat; have exact := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent; have normalized := Numerics.RationalBinary.scaleByPowerOfTwo exact.1 exact.2 (-targetExponent); Numerics.roundQuotientEven numerator (denominator * 2 ^ shift) = Numerics.roundQuotientEven normalized.1 normalized.2

Round a quotient at a chosen binary exponent either directly or by first restoring the quotient's exact external exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.quotientExtendedMantissa_shift (numerator denominator shift : ℕ) (hdenominator : denominator ≠ 0) : quotientExtendedMantissa numerator denominator >>> shift = quotientExtendedMantissa numerator (denominator * 2 ^ shift)

Shifting a quotient right by shift bits scales its denominator by 2 ^ shift.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.quotientExtendedMantissa_shiftLeft_shiftRight (numerator denominator shift : ℕ) (hdenominator : denominator ≠ 0) : quotientExtendedMantissa (numerator <<< shift) denominator >>> shift = quotientExtendedMantissa numerator denominator

Adding quotient bits by shifting left is undone by the matching right shift.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundedMantissa_shift_quotient (numerator denominator shift : ℕ) (hdenominator : denominator ≠ 0) : (Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy (numerator / denominator) (Float.Model.UnpackedFloat.accuracyOfFraction (numerator % denominator) denominator) >>> shift).roundedMantissa = Numerics.roundQuotientEven numerator (denominator * 2 ^ shift)

Nearest-even rounding after shifting a quotient agrees with rounding the rational number whose denominator has been scaled by the same power of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundWithAccuracy_quotient_eq_finishRoundedMantissa (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : Float.Model.UnpackedFloat.roundWithAccuracy spec sign (numerator / denominator) exponent (Float.Model.UnpackedFloat.accuracyOfFraction (numerator % denominator) denominator) = have shift := (spec.targetExponent (Float.Model.totalExponent (numerator / denominator) exponent) - exponent).toNat; finishRoundedMantissa spec sign (Numerics.roundQuotientEven numerator (denominator * 2 ^ shift), exponent + ↑shift)

After choosing the format's target exponent, model quotient rounding reduces to one roundQuotientEven call on the correspondingly scaled denominator.