claimroutine

Normalization and rounding conventions for Newton iteration

Defines normalized ranges and truncation RtR_t for Newton iteration
fixes rounding conventions for the Newton error analysis
Claim·§10 Exact division and integer square root·inside corExact division and square root in multiplication time

Statement (paper)

Set B(p)=p(lg⁡p)1−κB(p)=p(\lg p)^{1-\kappa}. After a linear scan handling zero inputs and locating the significant bits, write b=2hcb=2^h c with 0≤h<n0\le h<n and 1≤c<21\le c<2 for division, and a=22eca=2^{2e}c with 0≤e<n/20\le e<n/2 and 1≤c<41\le c<4 for square root. For an integer t≥1t\ge1 let Rt(z)=2−t⌊2tz⌋R_t(z)=2^{-t}\lfloor 2^t z\rfloor and δ=2−t\delta=2^{-t}; then the prefix ct=Rt(c)c_t=R_t(c) satisfies 0≤c−ct<δ0\le c-c_t<\delta. Each product is computed exactly on integer significands and then rounded by RtR_t, while additions and shifts are exact until a stated rounding.

In plain English

Defines the setup for exact division and square root: with B(p)=p(lg⁡p)1−κB(p)=p(\lg p)^{1-\kappa}, zero inputs are handled by a linear scan, and the divisor is written b=2hcb=2^h c with 1≤c<21\le c<2 (or a=22eca=2^{2e}c with 1≤c<41\le c<4 for square root). Truncation Rt(z)=2−t⌊2tz⌋R_t(z)=2^{-t}\lfloor 2^t z\rfloor with δ=2−t\delta=2^{-t} gives a prefix ct=Rt(c)c_t=R_t(c) with 0≤c−ct<δ0\le c-c_t<\delta, and products are computed exactly then rounded by RtR_t, while sums and shifts are exact.

Why it's here

This fixes the normalized ranges and the rounding rule once, so the later Newton-iteration steps for the reciprocal and the inverse square root can track their errors in units of δ\delta. The bound 0≤c−ct<δ0\le c-c_t<\delta and the rule that only products are rounded are what the residual bounds in the following claims rely on.
Classified routine:
Standard normalization and truncation setup for Newton iteration in multiple-precision arithmetic, as in Brent–Zimmermann's Modern Computer Arithmetic. It is bookkeeping that fixes the conventions the later error analysis relies on.

Uses

Nothing else in the paper

Used by

claimRounded reciprocal Newton step residual bound

Sources

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

Phase 2 aligns this node to a Lean declaration.