claimroutineinferred_dep

Exact quotient and root by correction tests

Correction tests make quotient and root exact from estimates off by one
turns approximate outputs into exact division and root
Claim·§10 Exact division and integer square root·inside corExact division and square root in multiplication time

Statement (paper)

With P=2n+4P=2n+4, the approximate reciprocal and square-root routines followed by the exact correction steps produce q=⌊a/b⌋q=\lfloor a/b\rfloor, r=a−bqr=a-bq and ⌊a⌋\lfloor\sqrt a\rfloor exactly: the floor q0q_0 of a2−hxa2^{-h}x differs from qq by at most one, and the floor s0s_0 of the shifted root approximation differs from ⌊a⌋\lfloor\sqrt a\rfloor by at most one, so the tests r0<0r_0<0, r0≥br_0\ge b, s02>as_0^2>a and (s0+1)2≤a(s_0+1)^2\le a yield the exact values, all computed on O(n)O(n)-bit quantities in time O(B(n))O(B(n)) plus O(n)O(n) overhead for descriptors, scans and padding.

In plain English

With working precision P=2n+4P=2n+4, the approximate reciprocal and square-root routines give a quotient estimate q0q_0 and a root estimate s0s_0 that are each off by at most one from q=⌊a/b⌋q=\lfloor a/b\rfloor and ⌊a⌋\lfloor\sqrt a\rfloor. The tests r0<0r_0<0, r0≥br_0\ge b, s02>as_0^2>a and (s0+1)2≤a(s_0+1)^2\le a then fix them to the exact values, using only O(n)O(n)-bit arithmetic in time O(B(n))O(B(n)) plus O(n)O(n) overhead.

Why it's here

This turns the approximate Newton outputs (the reciprocal and square-root accuracy claims) into exact integer division with remainder and exact integer square root. Precision P=2n+4P=2n+4 keeps the error below one unit, so a single correction step suffices. The cost claim for the Newton routines, together with a constant number of multiplications from the main theorem, gives the corollary's O(n(lg⁡n)1−κ)O(n(\lg n)^{1-\kappa}) bound.
Classified routine:
This is the textbook reduction of exact division and integer square root to Newton iteration with a final ±1 correction, as in Brent–Zimmermann, Modern Computer Arithmetic. Here it is applied to the earlier precision and cost claims.

Uses

claimCapped doubling gives reciprocal to precisionclaimRounded Newton square-root error analysisclaimNewton routines cost O(B(p)) on fixed tapesthmInteger multiplication in O(n (lg n)^{1-κ}) time

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Exact quotient and root by correction tests" rests on claim-cor-exact-arithmetic-3
  • info
    inferred_dep
    outline: "Exact quotient and root by correction tests" rests on claim-cor-exact-arithmetic-4
  • info
    inferred_dep
    outline: "Exact quotient and root by correction tests" rests on claim-cor-exact-arithmetic-5
  • info
    inferred_dep
    outline: "Exact quotient and root by correction tests" rests on thm:main