claimroutineinferred_dep

Rounded Newton square-root error analysis

Rounded Newton step for c\sqrt c squares the error plus 92δ\frac92\delta
approximate square root for the exact correction
Claim·§10 Exact division and integer square root·inside corExact division and square root in multiplication time

Statement (paper)

Let cc be the input and ctc_t its prefix at tt fractional bits, with ct<4c_t<4. Suppose the current dyadic xx satisfies 1/2≤x≤5/21/2\le x\le5/2, and let x+=Rt((x+qt)/2)x^+=R_t((x+q_t)/2) where qt=Rt(ctv)q_t=R_t(c_tv) and v=2−jzv=2^{-j}z with x=2jdx=2^jd, 1≤d<21\le d<2, j∈{−1,0,1}j\in\{-1,0,1\}, and ∣1−dz∣≤2−t−1|1-dz|\le2^{-t-1}. Then ∣v−1/x∣≤2−t=δ|v-1/x|\le2^{-t}=\delta, ∣qt−c/x∣≤7δ|q_t-c/x|\le7\delta, and ∣x+−c∣≤(x−c)22x+92δ|x^+-\sqrt c|\le\frac{(x-\sqrt c)^2}{2x}+\frac92\delta. Starting from the seed x=3/2x=3/2, with one step at t=6t=6 giving error less than 1/41/4, and thereafter maintaining the invariant ∣x−c∣≤2−m−1|x-\sqrt c|\le2^{-m-1} with m≥1m\ge1 (which gives 3/4≤x≤9/43/4\le x\le9/4), the capped doubling schedule with five guard bits yields ∣x−c∣≤2−p−1|x-\sqrt c|\le2^{-p-1} at target pp.

In plain English

One rounded Newton step x+=Rt((x+qt)/2)x^+=R_t((x+q_t)/2) for c\sqrt c, using an approximate reciprocal vv of xx with error at most δ=2−t\delta=2^{-t}, has error at most (x−c)22x+92δ\frac{(x-\sqrt c)^2}{2x}+\frac92\delta. Starting from x=3/2x=3/2 with a warm-up step at t=6t=6 and following the capped doubling schedule with five guard bits, the routine reaches ∣x−c∣≤2−p−1|x-\sqrt c|\le2^{-p-1} at any target pp.

Why it's here

This is the square-root counterpart of the reciprocal claim: the Newton step squares the error, and the guard bits keep the rounding terms (7δ7\delta for the quotient, then 92δ\frac92\delta) small enough to preserve the invariant while precision doubles. It provides the approximate square root that the cost analysis and the exact correction step for ⌊a⌋\lfloor\sqrt a\rfloor depend on.
Classified routine:
This is the standard error analysis of Newton's (Heron's) iteration for square roots with rounding at doubling precision. It adapts the textbook Newton-iteration analysis (e.g. Brent–Zimmermann, Modern Computer Arithmetic) and mirrors the paper's own reciprocal claim (claim-cor-exact-arithmetic-3).

Uses

claimCapped doubling gives reciprocal to precision

Used by

claimNewton routines cost O(B(p)) on fixed tapesclaimExact quotient and root by correction tests

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Square-root Newton iteration error analysis" rests on claim-cor-exact-arithmetic-3