claimroutineinferred_dep

Capped doubling gives reciprocal to precision

Capped-doubling reciprocal reaches ∣1−cx∣≤2−p−1|1-cx|\le2^{-p-1} at target pp
approximate reciprocal for division and cost analysis
Claim·§10 Exact division and integer square root·inside corExact division and square root in multiplication time

Statement (paper)

For every target p≥1p\ge1, the reciprocal routine, started from the seed x=5/8x=5/8 and one warm-up step with t=6t=6, and then doubling the accuracy via m′=min⁡{2m,p}m'=\min\{2m,p\} at t=m′+5t=m'+5 fractional bits, returns a dyadic xx satisfying ∣1−cx∣≤2−p−1|1-cx|\le2^{-p-1} and ∣x−1/c∣≤2−p−1|x-1/c|\le2^{-p-1}, where these errors are measured against the true cc at every stage, although the prefix ctc_t changes.

In plain English

For any target p≥1p\ge1, the reciprocal routine starting from the seed x=5/8x=5/8 with one warm-up step at t=6t=6, then doubling accuracy via m′=min⁡{2m,p}m'=\min\{2m,p\} at t=m′+5t=m'+5 fractional bits, outputs a dyadic xx with ∣1−cx∣≤2−p−1|1-cx|\le2^{-p-1} and ∣x−1/c∣≤2−p−1|x-1/c|\le2^{-p-1}.

Why it's here

This is the induction that turns the one-step rounded Newton bound into a full reciprocal routine. The warm-up step brings the residual below 1/41/4, and each later step squares the residual while the extra 55 guard bits keep the rounding term 6δ6\delta small enough to preserve the target accuracy. The errors are always measured against the true cc even though the prefix ctc_t changes, and the final accuracy is then exactly pp. It supplies the approximate reciprocal that the exact-division step and the cost analysis rely on.
Classified routine:
Standard induction for Newton iteration with precision doubling and guard bits (as in Brent 1976 / Brent–Zimmermann, Modern Computer Arithmetic), applied to the earlier one-step rounded Newton residual bound.

Uses

claimRounded reciprocal Newton step residual bound

Used by

claimRounded Newton square-root error analysisclaimNewton 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:48
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Capped doubling gives reciprocal to target precision" rests on claim-cor-exact-arithmetic-2