Numerical inexactness and signed-zero arithmetic

For finite operands and results without overflow, inexactness means that the returned value differs from the exact rational expression; the division theorem also requires a nonzero divisor. Zero results use the operation's sign rule and preferred quantum clamped to the destination range. Changing a zero's cohort alone does not raise inexact.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.add_inexact_iff (f : Format) (mode : RoundingMode) (x y : Datum) (a b value : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (add f mode x y).status.overflow = false) (hv : (add f mode x y).value.toRat? = some value) : (add f mode x y).status.inexact = true ↔ value ≠ a + b

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sub_inexact_iff (f : Format) (mode : RoundingMode) (x y : Datum) (a b value : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (sub f mode x y).status.overflow = false) (hv : (sub f mode x y).value.toRat? = some value) : (sub f mode x y).status.inexact = true ↔ value ≠ a - b

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.mul_inexact_iff (f : Format) (mode : RoundingMode) (x y : Datum) (a b value : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (mul f mode x y).status.overflow = false) (hv : (mul f mode x y).value.toRat? = some value) : (mul f mode x y).status.inexact = true ↔ value ≠ a * b

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.div_inexact_iff (f : Format) (mode : RoundingMode) (x y : Datum) (a b value : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hb : b ≠ 0) (hfinite : (div f mode x y).status.overflow = false) (hv : (div f mode x y).value.toRat? = some value) : (div f mode x y).status.inexact = true ↔ value ≠ a / b

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.fma_inexact_iff (f : Format) (mode : RoundingMode) (x y z : Datum) (a b c value : ℚ) (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) (hv : (fma f mode x y z).value.toRat? = some value) : (fma f mode x y z).status.inexact = true ↔ value ≠ a * b + c

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.add_zeros (f : Format) (mode : RoundingMode) (sx sy : Bool) (qx qy : ℤ) : add f mode (Datum.finite sx 0 qx) (Datum.finite sy 0 qy) = { value := Datum.finite (zeroSumSign mode sx sy) 0 (max f.minQuantum (min (min qx qy) f.maxQuantum)) }

Equal-sign zeros preserve their sign; opposite signs use the cancellation rule.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.mul_zero_left (f : Format) (mode : RoundingMode) (sx sy : Bool) (c : ℕ) (qx qy : ℤ) : mul f mode (Datum.finite sx 0 qx) (Datum.finite sy c qy) = { value := Datum.finite (sx ^^ sy) 0 (max f.minQuantum (min (qx + qy) f.maxQuantum)) }

A zero product uses the XOR sign and clamps the sum of operand quanta to the format range.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.div_zero_numerator (f : Format) (mode : RoundingMode) (sx sy : Bool) (c : ℕ) (hc : c ≠ 0) (qx qy : ℤ) : div f mode (Datum.finite sx 0 qx) (Datum.finite sy c qy) = { value := Datum.finite (sx ^^ sy) 0 (max f.minQuantum (min (qx - qy) f.maxQuantum)) }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.div_zero_denominator (f : Format) (mode : RoundingMode) (sx sy : Bool) (c : ℕ) (hc : c ≠ 0) (qx qy : ℤ) : div f mode (Datum.finite sx c qx) (Datum.finite sy 0 qy) = { value := Datum.infinity (sx ^^ sy), status := { divideByZero := true } }

Divide-by-zero is raised for a finite nonzero numerator, with the quotient's XOR sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.div_infinity_zero (f : Format) (mode : RoundingMode) (sx sy : Bool) (q : ℤ) : div f mode (Datum.infinity sx) (Datum.finite sy 0 q) = { value := Datum.infinity (sx ^^ sy) }

Infinity divided by zero does not raise divide-by-zero: the numerator is not finite.