Exact rational rounding

Division produces an exact rational rather than a dyadic. These routines round (num / den) * 2^exponent directly, using integer quotient rounding and descriptor-derived normal, subnormal, and overflow thresholds.

The leading exponent is computed before scaling, and a quotient below half the least subnormal is recognized from that exponent alone, so a format with a very wide exponent range does not materialize an enormous shifted numerator or denominator. Conventional IEEE descriptors use the proof-facing thresholds where convenient; custom biases and finite encodings follow the general path with the same one-rounding contract.

Exact rationals for division

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeRoundRatScaled (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent : ℤ) (_hfmt : fmt.isIEEE = true) : Model fmt

Round exact rational (num/den) * 2^exponent in a conventional IEEE descriptor.

The explicit isIEEE proof ensures that the layout-derived bias and exponent bounds agree with the descriptor. Use roundRatScaled for a custom bias or a finite encoding; it selects the appropriate rounder from the complete descriptor.

This is the division analogue of roundDyadic: the overflow, subnormal, and normal cases are the same, and the mantissa is obtained by roundQuotientEven instead of the integer roundShiftRightEven.

The normal-path mantissa scale is fracWidth - ⌊log₂(num/den)⌋: the external exponent cancels, so wide-exponent formats do not materialize an enormous shifted numerator or denominator. A quotient below half the least subnormal returns signed zero before any shift. A zero denominator is not a rational value and returns the format's invalid-operation result.

@[inline]

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

Round exact rational (num / den) * 2^exponent according to the complete format descriptor.

A quotient below half the least subnormal returns the format's zero from the leading exponent alone, without materializing the subnormal alignment shift. In the remaining paths, the shift is controlled by the numerator and denominator sizes and the destination precision, rather than the full exponent range.

@[inline]

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

Round exact rational (num / den) * 2^exponent to Model fmt using nearest-even.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRat (fmt : FloatFormat) (sign : Bool) (num den : ℕ) : Model fmt

Round exact rational num/den to Model fmt with nearest-even rounding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_den_zero (fmt : FloatFormat) (sign : Bool) (num : ℕ) (exponent : ℤ) : roundRatScaled fmt sign num 0 exponent = invalidResult fmt

A zero denominator is rejected by scaled rational rounding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_num_zero (fmt : FloatFormat) (sign : Bool) (den : ℕ) (exponent : ℤ) (hden : den ≠ 0) : roundRatScaled fmt sign 0 den exponent = zero fmt sign

A zero numerator rounds to the format's zero when the denominator is nonzero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRat_den_zero (fmt : FloatFormat) (sign : Bool) (num : ℕ) : roundRat fmt sign num 0 = invalidResult fmt

A zero denominator is rejected with the destination format's invalid-operation result.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRat_num_zero (fmt : FloatFormat) (sign : Bool) (den : ℕ) (hden : den ≠ 0) : roundRat fmt sign 0 den = zero fmt sign

A zero rational rounds to the format's zero when the denominator is nonzero.