claimroutine

Coefficient digits via integer arithmetic

Coefficient digits computed by query-free integer arithmetic after place

k

shows input queries stop at early places

Claim·§10.4 Reciprocals and the early-word convention·inside lemReciprocal with early-word storage

Statement (paper)

The signed numerator of

x^0

in units

2^{-k}

has

O(k+1)

bits and is formed by querying places

0,\ldots,k

and updating the integer prefix. Once this prefix is obtained, a coefficient digit of place

r\leq t+O(1)

is returned by integer computations (numerator squaring, integer division, and floors at places

r

and

r-1

, or the place-zero floor alone at

r=0

) that make no further operand queries and use only

O(k+r+1)

bits, with no clipping needed because the coefficients were normalized in advance.

In plain English

The signed numerator of

x^0

in units

2^{-k}

has

O(k+1)

bits and comes from querying input places

0,\ldots,k

and updating an integer prefix. Given that prefix, the coefficient digit at place

r\leq t+O(1)

is computed by integer operations that make no further queries and use

O(k+r+1)

bits, with no clipping.

Why it's here

This claim bounds the cost of producing the reciprocal's coefficient digits. All input queries occur at places up to

k

while the prefix is built, and the rest is query-free integer arithmetic (squaring, division, floors at places

r

and

r-1

) in linear space. That is what the early-word payment claim uses to confine the

O(t+1)

-bit word to early input places. The residue-stream lemma then turns the approximate integers into exact digits.</br>

Classified routine:

Direct bookkeeping inside the reciprocal lemma: elementary integer arithmetic (squaring, division, floors) on an

O(k+1)

-bit prefix, combined with the earlier residue-stream lemma that turns approximate integers into exact signed digits.

Uses

lemApproximate integers give exact digit streams

Used by

claimEarly-word payment at early input places

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.