Decimal arithmetic range and numerical error

Every operation returns a valid destination datum. For finite operands and a result without overflow, the nearest-mode error bounds compare the returned value with the exact rational sum, difference, product, quotient, or fused expression. Division additionally requires a nonzero divisor. The fused bound concerns x * y + z directly, without a rounded intermediate product.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nanResult_valid (f : Format) (s : Bool) (p : ℕ) (invalid : Bool) : Datum.Valid f (nanResult f s p invalid).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.invalidResult_valid (f : Format) : Datum.Valid f invalidResult.value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.add_valid (f : Format) (mode : RoundingMode) (x y : Datum) : Datum.Valid f (add f mode x y).value

Addition always returns a valid representation, including exceptional operands.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sub_valid (f : Format) (mode : RoundingMode) (x y : Datum) : Datum.Valid f (sub f mode x y).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.mul_valid (f : Format) (mode : RoundingMode) (x y : Datum) : Datum.Valid f (mul f mode x y).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.div_valid (f : Format) (mode : RoundingMode) (x y : Datum) : Datum.Valid f (div f mode x y).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.addInfinity_valid (f : Format) (s : Bool) (z : Datum) : Datum.Valid f (addInfinity f s z).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.fma_valid (f : Format) (mode : RoundingMode) (x y z : Datum) : Datum.Valid f (fma f mode x y z).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.add_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (add f mode x y).status.overflow = false) : ∃ (value : ℚ), (add f mode x y).value.toRat? = some value ∧ |value - (a + b)| ≤ 10 ^ roundingQuantum f |a + b| / 2

Nearest addition is within half a decimal grid unit of the exact sum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sub_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (sub f mode x y).status.overflow = false) : ∃ (value : ℚ), (sub f mode x y).value.toRat? = some value ∧ |value - (a - b)| ≤ 10 ^ roundingQuantum f |a - b| / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.mul_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (mul f mode x y).status.overflow = false) : ∃ (value : ℚ), (mul f mode x y).value.toRat? = some value ∧ |value - a * b| ≤ 10 ^ roundingQuantum f |a * b| / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.div_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hb : b ≠ 0) (hfinite : (div f mode x y).status.overflow = false) : ∃ (value : ℚ), (div f mode x y).value.toRat? = some value ∧ |value - a / b| ≤ 10 ^ roundingQuantum f |a / b| / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.fma_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x y z : Datum) (a b c : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hz : z.toRat? = some c) (hfinite : (fma f mode x y z).status.overflow = false) : ∃ (value : ℚ), (fma f mode x y z).value.toRat? = some value ∧ |value - (a * b + c)| ≤ 10 ^ roundingQuantum f |a * b + c| / 2

FMA rounds the exact fused expression, including cancellation across the format range.