The unbounded nearest-even quotient

The quotient is characterized by an error of at most one half and even parity at the two possible midpoints. The remainder coefficient never exceeds the original dividend or half the divisor. These integer bounds will prove representability at the preferred decimal quantum, without rounding the result.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderCoefficient_le (a b : ℕ) : remainderCoefficient a b ≤ a

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderCoefficient_twice_le (a b : ℕ) (hb : b ≠ 0) : 2 * remainderCoefficient a b ≤ b

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderCoefficient_eq_zero_iff (a b : ℕ) (hb : b ≠ 0) : remainderCoefficient a b = 0 ↔ a % b = 0

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderRoundUp_eq_false_of_zero (a b : ℕ) (hb : b ≠ 0) (hz : remainderCoefficient a b = 0) : remainderRoundUp a b = false

Zero residuals use the lower quotient and therefore retain the input sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderCoefficient_signed (a b : ℕ) (hb : b ≠ 0) : (if remainderRoundUp a b = true then -↑(remainderCoefficient a b) else ↑(remainderCoefficient a b)) = ↑a - ↑(remainderQuotient a b) * ↑b

The natural coefficient and sign encode the exact signed integer residual.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderQuotient_error (a b : ℕ) (hb : b ≠ 0) : 2 * |↑a - ↑(remainderQuotient a b) * ↑b| ≤ ↑b

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderQuotient_even_at_tie (a b : ℕ) (hb : b ≠ 0) (htie : 2 * remainderCoefficient a b = b) : remainderQuotient a b % 2 = 0

Either midpoint chooses the even integer, with no bound on quotient precision.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderQuotient_nearest (a b : ℕ) (hb : b ≠ 0) (n : ℤ) : |↑a - ↑(remainderQuotient a b) * ↑b| ≤ |↑a - ↑n * ↑b|

Every other integer quotient has at least as large a residual magnitude.