claimroutineinferred_dep

Rounded reciprocal Newton step residual bound

Rounded Newton step gives residual ≤ε2+6δ\le\varepsilon^2+6\delta
one-step error bound for reciprocal doubling
Claim·§10 Exact division and integer square root·inside corExact division and square root in multiplication time

Statement (paper)

Let 1≤c<21\le c<2, let t≥1t\ge1, δ=2−t\delta=2^{-t}, ct=Rt(c)c_t=R_t(c), and let xx be a dyadic number with ε=1−cx\varepsilon=1-cx satisfying ∣ε∣≤1/2|\varepsilon|\le1/2. If u=Rt(ctx)u=R_t(c_tx) and x+=Rt(x(2−u))x^+=R_t\bigl(x(2-u)\bigr), then ∣1−cx+∣≤ε2+234δ<ε2+6δ|1-cx^+|\le\varepsilon^2+\frac{23}{4}\delta<\varepsilon^2+6\delta. In particular, starting from the seed x=5/8x=5/8, which has ∣ε∣≤3/8|\varepsilon|\le3/8 for all 1≤c<21\le c<2, one step with t=6t=6 gives ∣1−cx+∣<15/64<1/4|1-cx^+|<15/64<1/4.

In plain English

For 1≤c<21\le c<2 and a dyadic xx with residual ε=1−cx\varepsilon=1-cx, ∣ε∣≤1/2|\varepsilon|\le1/2, one Newton step for the reciprocal of cc using products rounded to tt fractional bits (using the prefix ctc_t of cc) gives x+x^+ with ∣1−cx+∣≤ε2+234δ<ε2+6δ|1-cx^+|\le\varepsilon^2+\frac{23}{4}\delta<\varepsilon^2+6\delta, where δ=2−t\delta=2^{-t}. From the seed x=5/8x=5/8 (where ∣ε∣≤3/8|\varepsilon|\le3/8), one step with t=6t=6 gives ∣1−cx+∣<15/64<1/4|1-cx^+|<15/64<1/4.

Why it's here

This is the error analysis of one rounded Newton step: the exact step squares the residual, and the truncation of cc and of the two products adds only an O(δ)O(\delta) term, using 0≤c−ct<δ0\le c-c_t<\delta and that only products are rounded. It lets the reciprocal routine in the next claim double its accuracy at each step, while the explicit seed computation shows the warm-up step brings the residual below 1/41/4.
Classified routine:
Standard error analysis of a Newton iteration for the reciprocal with truncated operands and rounded products, as in classical treatments (e.g., Brent–Zimmermann, Modern Computer Arithmetic). Here it is only explicit bookkeeping of the rounding constants and the seed.

Uses

claimNormalization and rounding conventions for Newton iteration

Used by

claimCapped doubling gives reciprocal to precision

Sources

PaperOpen
Section
§10 Exact division and integer square root
Page
—
Label
—
Line
sections/09-exact-arithmetic.tex:27
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Rounded reciprocal Newton step residual bound" rests on claim-cor-exact-arithmetic-1