Remainder representability and exact value

On the finer operand grid, either the dividend or the divisor has an original bounded coefficient. The integer remainder is no larger than either. Hence the exact result fits at the preferred quantum, including subnormal results.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_align_value (c : ℕ) (q r : ℤ) (hr : r ≤ q) : ↑(c * 10 ^ (q - r).toNat) * 10 ^ r = ↑c * 10 ^ q

Moving to a finer grid changes the coefficient by an integral radix power.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_coefficient_lt (f : Format) (cx cy : ℕ) (qx qy : ℤ) (hx : cx < f.coefficientBound) (hy : cy < f.coefficientBound) (hc : cy ≠ 0) : remainderCoefficient (cx * 10 ^ (qx - min qx qy).toNat) (cy * 10 ^ (qy - min qx qy).toNat) < f.coefficientBound

The exact remainder coefficient fits the original precision at the smaller quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderFinite_valid (f : Format) (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) (hx : Datum.Valid f (Datum.finite sx cx qx)) (hy : Datum.Valid f (Datum.finite sy cy qy)) (hc : cy ≠ 0) : Datum.Valid f (remainderFinite sx cx qx cy qy)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_valid (f : Format) (x y : Datum) (hx : Datum.Valid f x) (hy : Datum.Valid f y) : Datum.Valid f (remainder f x y).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_status (f : Format) (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) (hc : cy ≠ 0) : (remainder f (Datum.finite sx cx qx) (Datum.finite sy cy qy)).status = { }

Finite, nonzero-divisor remainder raises no default exceptions.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_quantum (f : Format) (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) (hc : cy ≠ 0) : ∃ (s : Bool) (c : ℕ), (remainder f (Datum.finite sx cx qx) (Datum.finite sy cy qy)).value = Datum.finite s c (min qx qy)

Every finite ordinary result uses exactly the preferred quantum.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainderInteger (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) : ℤ

Signed integer quotient used in the exact remainder identity.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_value (f : Format) (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) (hc : cy ≠ 0) : (remainder f (Datum.finite sx cx qx) (Datum.finite sy cy qy)).value.toRat? = some (Datum.finiteValue sx cx qx - ↑(remainderInteger sx sy cx cy qx qy) * Datum.finiteValue sy cy qy)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_error_le_half_divisor (f : Format) (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) (hc : cy ≠ 0) : ∃ (v : ℚ), (remainder f (Datum.finite sx cx qx) (Datum.finite sy cy qy)).value.toRat? = some v ∧ 2 * |v| ≤ ↑cy * 10 ^ qy

The actual delivered remainder is at most half the divisor in magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_zero_sign (sx : Bool) (cx cy : ℕ) (qx qy : ℤ) (hc : cy ≠ 0) (s : Bool) (q : ℤ) (hz : remainderFinite sx cx qx cy qy = Datum.finite s 0 q) : s = sx

A zero remainder retains the dividend's sign, for either sign of divisor.