claimroutine

First-order reciprocal expansion with quadratic error

1/(Cx)=α+βe+1/(Cx)=\alpha+\beta e+ quadratic error, so a linear tail term approximates it
reduces the reciprocal to a linear function of the unread tail
Claim·§10.4 Reciprocals and the early-word convention·inside lemReciprocal with early-word storage

Statement (paper)

Let k=⌊t/2⌋+ck=\lfloor t/2\rfloor+c, x0=x[k]x^0=x^{[k]}, e=x−x0e=x-x^0, and z=1/(Cx)z=1/(Cx), with cc a sufficiently large fixed integer and CC a sufficiently large fixed power of two. Then x0∈[a/2,2b]x^0\in[a/2,2b], ∣e∣≤1|e|\leq 1, the coefficients α=1/(Cx0)\alpha=1/(Cx^0) and β=−1/(C(x0)2)\beta=-1/(C(x^0)^2) are bounded by one in absolute value, and z=α+βe+e2/(C(x0)2x)z=\alpha+\beta e+e^2/(C(x^0)^2x) exactly, so Tt=α+βeT_t=\alpha+\beta e satisfies ∣Tt−z∣≤O(2−2k)|T_t-z|\leq O(2^{-2k}) and hence 2t∣Tt−z∣≤1/42^t|T_t-z|\leq 1/4 for every t≥0t\geq0. Moreover, the clipped expression T^t\widehat T_t of TtT_t to [−1,1][-1,1] satisfies the same bound 2t∣T^t−z∣≤1/42^t|\widehat T_t-z|\leq 1/4.

In plain English

With k=⌊t/2⌋+ck=\lfloor t/2\rfloor+c, x0=x[k]x^0=x^{[k]} the truncation of xx and e=x−x0e=x-x^0, the reciprocal z=1/(Cx)z=1/(Cx) equals α+βe+e2/(C(x0)2x)\alpha+\beta e+e^2/(C(x^0)^2x) exactly, where α=1/(Cx0)\alpha=1/(Cx^0) and β=−1/(C(x0)2)\beta=-1/(C(x^0)^2) are bounded by one. So Tt=α+βeT_t=\alpha+\beta e approximates zz within O(2−2k)O(2^{-2k}), giving 2t∣Tt−z∣≤1/42^t|T_t-z|\leq 1/4, and clipping TtT_t to [−1,1][-1,1] keeps this bound.

Why it's here

This reduces the reciprocal to a linear function of the not-yet-read tail ee, with coefficients that depend only on the first k≈t/2k\approx t/2 input places. The error is quadratic in ee, so it is about 2−2k≤2−t2^{-2k}\leq 2^{-t} and the approximation meets the required accuracy at level tt. This is why only places j≤⌊t/2⌋+O(1)j\leq\lfloor t/2\rfloor+O(1) are needed for the long word, and the later claims build the exact stream from it using elementary operations and multiplication.
Classified routine:
An elementary first-order Taylor/Newton expansion of 1/x about a truncation with an exact quadratic remainder. It is a direct calculation adapted from standard online-arithmetic reciprocal techniques.

Uses

Nothing else in the paper

Used by

claimClipped reciprocal approximation has exact streams

Sources

PaperOpen
Section
§10.4 Reciprocals and the early-word convention
Page
—
Label
—
Line
sections/arithmetic.tex:425
Leannot aligned

Phase 2 aligns this node to a Lean declaration.