claimroutineinferred_dep

Newton routines cost O(B(p)) on fixed tapes

Both Newton routines run in O(B(p))O(B(p)) on fixed tapes
cost bound feeding the exact correction step
Claim·§10 Exact division and integer square root·inside corExact division and square root in multiplication time

Statement (paper)

With B(m)B(m) denoting the cost of Theorem  at precision mm, the reciprocal routine at target pp and the square-root routine at target pp can each be implemented on one fixed finite set of one-dimensional tapes, with a fixed finite alphabet and fixed subroutine depth, in O(B(p))O(B(p)) time, and no random-access simulation is used.

In plain English

With B(m)B(m) the multiplication cost of Theorem thm:main at precision mm, both the reciprocal routine and the square-root routine at target pp run in O(B(p))O(B(p)) time. They do so on a fixed finite set of one-dimensional tapes, with a fixed alphabet and fixed subroutine depth, and without any random-access simulation.

Why it's here

This is the cost and model bookkeeping for the two Newton routines whose accuracy was established in the reciprocal and square-root claims. Because the working precision at least doubles each step, the total cost is dominated by the last step and stays O(B(p))O(B(p)). Fixed tapes and bounded subroutine depth ensure the routines are genuine fixed-machine Turing computations, which lets the corollary's O(n(lg⁡n)1−κ)O(n(\lg n)^{1-\kappa}) bound for division and square root follow from the main multiplication theorem.
Classified routine:
This is the standard Newton-iteration cost argument: precision doubles each step, so the geometric sum is dominated by the final multiplication (Brent 1976; Aho–Hopcroft–Ullman; Brent–Zimmermann, Modern Computer Arithmetic). Here it is applied to the paper's multiplication bound B(p), together with routine Turing-machine model bookkeeping.

Uses

thmInteger multiplication in O(n (lg n)^{1-κ}) timeclaimCapped doubling gives reciprocal to precisionclaimRounded Newton square-root error analysis

Used by

claimExact quotient and root by correction tests

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Newton routines cost O(B(p)) on fixed tapes" rests on claim-cor-exact-arithmetic-3
  • info
    inferred_dep
    outline: "Newton routines cost O(B(p)) on fixed tapes" rests on claim-cor-exact-arithmetic-4