Deterministic nearest-even rational rounding

This is the exact Rat-to-Int specialization of the shared quotient-rounding decision. It uses integer numerator and denominator arithmetic throughout; no floating approximation is introduced while deciding a tie.

The proofs cover both signs, the half-unit error bound, fixed points, and exact half steps. Keeping those facts beside the executable definition gives fixed-point and mixed-precision code one rounding primitive with a stable, reusable contract.

@[inline]

def FloatLib.Numerics.roundRatEven (x : ℚ) : ℤ

Round an exact rational to the nearest integer, breaking halfway cases toward the even result.

theorem FloatLib.Numerics.roundQuotientEven_error_le_half (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : |↑(roundQuotientEven numerator denominator) - ↑numerator / ↑denominator| ≤ 1 / 2

Nearest-even quotient rounding differs from the exact nonnegative rational by at most one half.

@[simp]

theorem FloatLib.Numerics.roundRatEven_intCast (value : ℤ) : roundRatEven ↑value = value

Nearest-even rational rounding fixes every integer exactly.

theorem FloatLib.Numerics.roundRatEven_error_eq_magnitude (x : ℚ) : |↑(roundRatEven x) - x| = |↑(roundQuotientEven x.num.natAbs x.den) - ↑x.num.natAbs / ↑x.den|

Signed rational rounding has the same absolute error as rounding its magnitude.

theorem FloatLib.Numerics.roundRatEven_error_le_half (x : ℚ) : |↑(roundRatEven x) - x| ≤ 1 / 2

Nearest-even rational rounding differs from its exact input by at most one half.

theorem FloatLib.Numerics.roundRatEven_eq_of_error_lt_half (x : ℚ) (n : ℤ) (h : |↑n - x| < 1 / 2) : roundRatEven x = n

A candidate strictly within half a unit is the unique rounded integer.

theorem FloatLib.Numerics.roundRatEven_nearest (x : ℚ) (n : ℤ) : |↑(roundRatEven x) - x| ≤ |↑n - x|

The delivered integer is at least as close as every competing integer.

theorem FloatLib.Numerics.roundQuotientEven_even_of_tie (numerator denominator : ℕ) (htie : 2 * (numerator % denominator) = denominator) : roundQuotientEven numerator denominator % 2 = 0

An exact quotient midpoint rounds to an even natural number.

theorem FloatLib.Numerics.roundQuotientEven_error_lt_half (numerator denominator : ℕ) (hd : denominator ≠ 0) (ht : 2 * (numerator % denominator) ≠ denominator) : |↑(roundQuotientEven numerator denominator) - ↑numerator / ↑denominator| < 1 / 2

Away from a quotient midpoint the error is strictly less than half a unit.

theorem FloatLib.Numerics.roundRatEven_even_of_quotient_tie (x : ℚ) (ht : 2 * (x.num.natAbs % x.den) = x.den) : roundRatEven x % 2 = 0

An exact quotient midpoint rounds to an even integer, regardless of its sign.

theorem FloatLib.Numerics.roundRatEven_even_of_error_eq_half (x : ℚ) (h : |↑(roundRatEven x) - x| = 1 / 2) : roundRatEven x % 2 = 0

Half-unit error can occur only when the delivered integer is even, for either sign.

theorem FloatLib.Numerics.roundRatEven_half_step (n : ℤ) : roundRatEven (↑n + 1 / 2) = if n % 2 = 0 then n else n + 1

Every half-integer rounds to its even neighbor, including negative inputs.

theorem FloatLib.Numerics.roundRatEven_eq_floor_ceil (x : ℚ) : roundRatEven x = if x.floor = x.ceil then x.floor else if x - ↑x.floor < ↑x.ceil - x then x.floor else if ↑x.ceil - x < x - ↑x.floor then x.ceil else if x.floor % 2 = 0 then x.floor else x.ceil

The shared quotient algorithm agrees with the floor/ceiling nearest-even decision.