Division with one integer quotient

The nearest-even kernel divides a doubled numerator. The low quotient bit distinguishes values below a rounding midpoint, and the next bit resolves ties whose retained significand is odd. Only the remaining case needs an exactness check. A machine-word product often disproves exactness before the full product is needed. Equality of machine words never certifies equality of natural numbers.

Scaling and the extra quotient bit share one numerator shift. Neither the fraction width nor the integer division has a fixed limb bound. GeneralProof proves agreement with the exact rational rounders, including subnormal results and all six rounding directions.

Nearest-away rounding first tests for a grid tie with isGridTieAtExponent, which costs one more remainder, and then rounds the magnitude up at a tie and to nearest-even otherwise.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundEvenDoubled (doubled den : ℕ) : ℕ

Round doubled / (2 * den) to nearest, with ties to even.

Callers supply an even doubled and a nonzero denominator. Computing the extra quotient bit avoids a second arbitrary-precision division for a remainder. A failed low-word comparison certifies inexactness, but a successful one still needs equality of the full product.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundEvenScaled (num den : ℕ) : ℤ → ℕ

Nearest-even quotient rounding with a fused binary scale and extra quotient bit.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundDirectedScaled (up : Bool) (num den : ℕ) (shift : ℤ) : ℕ

Directed quotient rounding after an exact binary scale.

The ceiling is roundQuotient .up, which needs one integer division.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.ieeeRoundAtExponent (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) : Model fmt

IEEE nearest-even rational rounding with a supplied rational exponent.

rationalExponent must equal RationalBinary.floorLog2 num den. Supplying it lets a finite division use a single significand comparison when both operands are normal.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.generalRoundAtExponent (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) : Model fmt

Descriptor-generic nearest-even rational rounding with a supplied rational exponent.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.directedRoundAtExponent (fmt : FloatFormat) (up sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) : Model fmt

Directed rational rounding with a supplied rational exponent.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.nearestEvenRoundAtExponent (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) : Model fmt

Nearest-even rational rounding with a supplied rational exponent, selecting the IEEE branch for a conventional IEEE descriptor and the descriptor-generic branch otherwise.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.isGridTieAtExponent (fmt : FloatFormat) (num den : ℕ) (exponent rationalExponent : ℤ) : Bool

Whether (num / den) * 2^exponent lies exactly halfway between two adjacent values of the binary grid of fmt, reusing a supplied rational exponent.

rationalExponent must equal RationalBinary.floorLog2 num den. The test is then rationalIsGridTieScaled (isGridTieAtExponent_eq), and with another exponent it scales the quotient to the wrong grid. The quotient is scaled as the nearest-even and directed branches scale it, to the subnormal spacing below the normal range and to fracWidth + 1 significant bits above it, and it is a tie when twice the remainder equals the denominator. A zero numerator or denominator and a magnitude below half the least subnormal are never ties.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundAtExponent (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (num den : ℕ) (exponent rationalExponent : ℤ) : Model fmt

Rational rounding in any direction, reusing a supplied rational exponent.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.roundScaled (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (num den : ℕ) (exponent : ℤ) : Model fmt

Round with one integer quotient, inlining the thresholds for fixed descriptors. Nearest-away rounding also takes the remainder of its tie test.