Exactness of Addition Errors

For a valid, monotone exponent function and any nearest rounding rule, the error of adding two representable values is itself representable. The proof aligns both operands on the smaller canonical grid, represents the rounded result on that same grid, and uses nearestness to control the canonical exponent of the error.

Nearestness is essential. For directed rounding the statement fails: with radix 2 and three digits of precision, rounding 1 - 2^(-10) downward gives 7/8, and the error 2^(-3) - 2^(-10) needs seven digits.

The representable error is the mathematical content of the TwoSum and FastTwoSum error-free transformations: x + y = round (x + y) + e with e in the format. The step-by-step exactness of the floating-point operations that compute e in those algorithms is not formalized here.

theorem FloatLib.Floats.Formats.Flocq.add_round_error_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] [MonotoneExp fexp] {rnd : ℝ → ℤ} [ValidRndToNearest rnd] {x y : ℝ} (hx : genericFormat β fexp x) (hy : genericFormat β fexp y) : genericFormat β fexp (round rnd (x + y) - (x + y))

The addition error of two representable values under any nearest rounding rule is representable.

The rounding rule is implicit because it is determined by the conclusion; nearestEven is the usual instance. The statement needs a monotone exponent function and fails for directed rounding.

theorem FloatLib.Floats.Formats.Flocq.add_round_exact_error {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] [MonotoneExp fexp] {rnd : ℝ → ℤ} [ValidRndToNearest rnd] {x y : ℝ} (hx : genericFormat β fexp x) (hy : genericFormat β fexp y) : ∃ (e : ℝ), genericFormat β fexp e ∧ x + y = round rnd (x + y) + e

Error-free transformation of addition: the exact sum of two representable values is the rounded sum plus a representable error term.

This is the specification met by the TwoSum and FastTwoSum algorithms. The term e is x + y - round (x + y); its representability is add_round_error_generic up to sign.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLT_to_FIX {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : genericFormat β (fltExp emin prec) x) : genericFormat β (fixExp emin) x

Every FLT value lies on its minimum-exponent FIX grid.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FIX_to_FLT_of_abs_le {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : genericFormat β (fixExp emin) x) (hbound : |x| ≤ bpow β (prec + emin)) : genericFormat β (fltExp emin prec) x

A bounded FIX value is FLT-representable, including the radix-power boundary.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLT_add_small {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hx : genericFormat β (fltExp emin prec) x) (hy : genericFormat β (fltExp emin prec) y) (hbound : |x + y| ≤ bpow β (prec + emin)) : genericFormat β (fltExp emin prec) (x + y)

A sufficiently small sum of two FLT values is exactly FLT-representable.