Rational meaning of P3109 rounding decisions

The report's fractional part is an exact rational. Natural division implements its floor, and quotient/remainder comparisons implement nearest-even integer rounding. These facts identify every executable rounding decision with §4.7.4, including each possible supplied stochastic word. No distribution or randomness-quality assumption is made.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §4.7.4.

def FloatLib.Floats.Formats.P3109.RationalRounding.nearestEven (value : ℚ) : ℕ

Nearest integer to a nonnegative rational, with ties sent to the even integer.

def FloatLib.Floats.Formats.P3109.RationalRounding.roundAway (mode : RoundingMode) (negative lowerEven : Bool) (fraction : ℚ) : Bool

The report's rounding decision in terms of the exact fractional part.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.div_eq_quotient_add_fraction (numerator denominator : ℕ) (hd : 0 < denominator) : ↑numerator / ↑denominator = ↑(numerator / denominator) + ↑(numerator % denominator) / ↑denominator

Division splits a nonnegative rational into its integer part and exact remainder.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.fraction_lt_half (remainder denominator : ℕ) (hd : 0 < denominator) : ↑remainder / ↑denominator < 1 / 2 ↔ 2 * remainder < denominator

The exact remainder fraction is below one half precisely under the integer comparison.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.fraction_eq_half (remainder denominator : ℕ) (hd : 0 < denominator) : ↑remainder / ↑denominator = 1 / 2 ↔ denominator = 2 * remainder

Equality at a halfway point is an exact integer equality.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundQuotientEven_eq_nearestEven (numerator denominator : ℕ) (hd : 0 < denominator) : Numerics.roundQuotientEven numerator denominator = nearestEven (↑numerator / ↑denominator)

Quotient/remainder nearest-even rounding implements the report's mathematical RNITE.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.scaleRationalFractionFloor_eq (remainder denominator bits : ℕ) : Format.Internal.scaleRationalFractionFloor remainder denominator bits = ⌊↑remainder / ↑denominator * 2 ^ bits⌋₊

Binary scaling followed by natural division is the floor of the exact scaled fraction.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.scaleRationalFractionNearestEven_eq (remainder denominator bits : ℕ) (hd : 0 < denominator) : Format.Internal.scaleRationalFractionNearestEven remainder denominator bits = nearestEven (↑remainder / ↑denominator * 2 ^ bits)

The stochastic-C helper computes mathematical nearest-even rounding of the scaled fraction.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.random_lt_modulus (random : RandomBits) : random.toNat < 2 ^ random.width

Every supplied word is strictly below the modulus specified by its width.

@[simp]

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAway_zero (mode : RoundingMode) (negative lowerEven : Bool) : roundAway mode negative lowerEven 0 = false

An exact integer is unchanged even by stochastic rounding, for every supplied word.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundRationalAwayWithParity_eq (mode : RoundingMode) (negative lowerEven : Bool) (remainder denominator : ℕ) (hd : 0 < denominator) : Format.Internal.roundRationalAwayWithParity mode negative lowerEven remainder denominator = roundAway mode negative lowerEven (↑remainder / ↑denominator)

All nine executable decisions agree with the report's exact rational formulas.