Deterministic nearest-even quotient rounding

Format-independent nearest-even rounding for a natural quotient and remainder. The executable decision uses only quotient parity and the remainder, so optimized kernels can recover the same result without constructing a large scaled numerator.

@[inline]

def FloatLib.Numerics.nearestEvenRoundsUp (quotientOdd : Bool) (remainder denominator : ℕ) : Bool

Whether a quotient should increase when rounding a nonnegative quotient and remainder to nearest, with an exact halfway case sent to the even integer.

Only the quotient's parity is needed. Keeping that fact explicit lets callers handle very large scaled numerators through modular arithmetic without first constructing the full quotient.

@[inline]

def FloatLib.Numerics.roundQuotientEven (numerator denominator : ℕ) : ℕ

Round numerator / denominator to the nearest natural number, breaking exact halfway cases toward the even result.

The function is total. Callers that assign mathematical quotient semantics must establish that denominator is nonzero: with denominator = 0, Lean's conventions n / 0 = 0 and n % 0 = n make the result 0 for numerator = 0 and 1 otherwise. The native kernel FixedWord.roundQuotientEven returns 0 for a zero denominator instead, so its refinement theorem assumes a nonzero denominator.

theorem FloatLib.Numerics.roundQuotientEven_eq_quotient_add (numerator denominator : ℕ) : roundQuotientEven numerator denominator = numerator / denominator + if nearestEvenRoundsUp (numerator / denominator % 2 == 1) (numerator % denominator) denominator = true then 1 else 0

Nearest-even quotient rounding either retains the integer quotient or increases it by one.

The decision depends only on the remainder and quotient parity. This form is useful for optimized algorithms that recover those two facts through modular arithmetic without constructing a very large scaled numerator.