Exactness of single-quotient rounding

If num = den * q + r, with r < den, dividing 2 * num yields 2 * q below the midpoint and 2 * q + 1 at or above it. Its low two bits and the equality test den * quotient = 2 * num therefore carry all the information ties to even needs. The low-word product can only reject that equality, and a low-word match is checked in full.

Nearest-away rounding reuses the nearest-even and directed branches, and its supplied-exponent tie test is the reference rationalIsGridTieScaled.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundEvenDoubled_twice (num den : ℕ) (hden : den ≠ 0) : roundEvenDoubled (2 * num) den = Numerics.roundQuotientEven num den

On a doubled numerator, roundEvenDoubled rounds to nearest even for any nonzero divisor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundEvenScaled_eq (num den : ℕ) (shift : ℤ) (hden : den ≠ 0) : roundEvenScaled num den shift = have scaled := Numerics.RationalBinary.scaleByPowerOfTwo num den shift; Numerics.roundQuotientEven scaled.1 scaled.2

Fusing the binary scale into the doubled numerator preserves quotient rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundDirectedScaled_eq (up : Bool) (num den : ℕ) (shift : ℤ) : roundDirectedScaled up num den shift = have scaled := Numerics.RationalBinary.scaleByPowerOfTwo num den shift; roundQuotDirected up scaled.1 scaled.2

Directed rounding uses the same lower and upper adjacent integers as the reference.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.ieeeRoundAtExponent_eq (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) (hfmt : fmt.isIEEE = true) (hlog : rationalExponent = Numerics.RationalBinary.floorLog2 num den) : ieeeRoundAtExponent fmt sign num den exponent rationalExponent = ieeeRoundRatScaled fmt sign num den exponent hfmt

The IEEE branch is ieeeRoundRatScaled, thresholds, carries, signed zeros and ties included.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.generalRoundAtExponent_eq (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) (hlog : rationalExponent = Numerics.RationalBinary.floorLog2 num den) : generalRoundAtExponent fmt sign num den exponent rationalExponent = roundRatScaledGeneral fmt sign num den exponent

The descriptor-generic branch is the reference rounder roundRatScaledGeneral.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.directedRoundAtExponent_eq (fmt : FloatFormat) (up sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) (hlog : rationalExponent = Numerics.RationalBinary.floorLog2 num den) : directedRoundAtExponent fmt up sign num den exponent rationalExponent = roundRatMagnitudeDirectedScaled fmt up sign num den exponent

Both directed magnitudes agree with the reference rational rounder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.nearestEvenRoundAtExponent_eq (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) (hlog : rationalExponent = Numerics.RationalBinary.floorLog2 num den) : nearestEvenRoundAtExponent fmt sign num den exponent rationalExponent = roundRatScaled fmt sign num den exponent

Selecting the IEEE or descriptor-generic branch gives the reference nearest-even rounder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.isGridTieAtExponent_eq (fmt : FloatFormat) (num den : ℕ) (exponent rationalExponent : ℤ) (hlog : rationalExponent = Numerics.RationalBinary.floorLog2 num den) : isGridTieAtExponent fmt num den exponent rationalExponent = rationalIsGridTieScaled fmt num den exponent

With a correct rational exponent, the tie test is the reference rational grid-tie test.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundAtExponent_eq (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) (hlog : rationalExponent = Numerics.RationalBinary.floorLog2 num den) : roundAtExponent fmt mode sign num den exponent rationalExponent = Internal.Directed.roundRatScaled fmt mode sign num den exponent

A correct rational exponent suffices for exact agreement in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundScaled_eq (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (num den : ℕ) (exponent : ℤ) : roundScaled fmt mode sign num den exponent = Internal.Directed.roundRatScaled fmt mode sign num den exponent

roundScaled equals exact rational rounding, with no width or format restriction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.floorLog2_eq_of_normal (precision num den : ℕ) (hnum : 2 ^ precision ≤ num ∧ num < 2 ^ (precision + 1)) (hden : 2 ^ precision ≤ den ∧ den < 2 ^ (precision + 1)) : Numerics.RationalBinary.floorLog2 num den = if den ≤ num then 0 else -1

Two normalized significands of the same precision have ratio in (1/2, 2). Their relative order therefore determines its binary exponent.