Division and Square-Root Residuals

Division and square-root residuals in FLX are exactly representable under the stated precision and operand hypotheses. A division residual is controlled both relative to the dividend and relative to the product of the rounded quotient with the divisor; the two bounds place it on their common exponent grid.

theorem FloatLib.Floats.Formats.Flocq.magnitude_le_round_FLX {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [ValidRnd rnd] {x : ℝ} (hround : round rnd x ≠ 0) : magnitude β x ≤ magnitude β (round rnd x)

A nonzero FLX rounded result has magnitude at least that of its exact input.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLX_sub_mul_of_bounds {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) {x a b : ℝ} (hx : genericFormat β (flxExp prec) x) (ha : genericFormat β (flxExp prec) a) (hb : genericFormat β (flxExp prec) b) (hlt : |x - a * b| < |x|) (hbound : |x - a * b| < bpow β (cexp β (flxExp prec) a + magnitude β b)) : genericFormat β (flxExp prec) (x - a * b)

Common grid argument for arithmetic residuals in FLX.

If x, a and b are representable and the residual x - a * b is smaller than |x| and than the radix power at exponent cexp a + magnitude b, then the residual lies on the exponent grid shared by x and by the product representation of a * b, so it is itself representable.

theorem FloatLib.Floats.Formats.Flocq.div_round_residual_FLX {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [ValidRnd rnd] {x y : ℝ} (hx : genericFormat β (flxExp prec) x) (hy : genericFormat β (flxExp prec) y) : genericFormat β (flxExp prec) (x - round rnd (x / y) * y)

The residual x - round(x / y) * y is exactly FLX-representable.

theorem FloatLib.Floats.Formats.Flocq.sqrt_round_residual_FLX {β : Numerics.Radix} (prec : ℤ) (hprec : 1 < prec) {x : ℝ} (hxFmt : genericFormat β (flxExp prec) x) : genericFormat β (flxExp prec) (x - round nearestEven √x ^ 2)

For precision greater than one, the nearest-rounded square-root residual x - q^2 is FLX-representable, where q is the nearest-even rounding of √x.

The hypothesis 1 < prec makes the unit roundoff u = β^(1 - prec) / 2 at most 1/4. The proof uses that bound to show |x - q^2| < x, which places the residual on the grid of x; with prec = 1 the relative error of q can reach 1/2 and the argument does not apply.