claimroutineinferred_dep

Clipped reciprocal approximation has exact streams

Clipped linear approximation has exact streams and integer error below 2
builds the reciprocal from elementary ops and multiplication
Claim·§10.4 Reciprocals and the early-word convention·inside lemReciprocal with early-word storage

Statement (paper)

For the fixed original tt, the coefficients α,β\alpha,\beta are exact rational numbers and the suffix ee has an exact stream (digit zero through kk, digit xjx_j thereafter), so Lemmas  and yield exact streams for the clipped expression T^t\widehat T_t using a fixed number of normalized operations and no additional reciprocal operation. Moreover, with Pt+3(T^t)P_{t+3}(\widehat T_t) the integer approximation at place t+3t+3 and Nt(z)=⌊Pt+3(T^t)/8⌋N_t(z)=\lfloor P_{t+3}(\widehat T_t)/8\rfloor, where kk and the coefficients are those of the original tt, one has ∣Nt(z)−2tz∣<3/2<2|N_t(z)-2^tz|<3/2<2; this integer modulo 2q2^q is obtained from Pt+3P_{t+3} modulo 2q+32^{q+3}.

In plain English

For fixed tt, the clipped linear approximation T^t=clip(α+βe)\widehat T_t=\mathrm{clip}(\alpha+\beta e) has exact streams, built from a fixed number of normalized elementary and multiplication operations with no further reciprocal. Its integer approximation Nt(z)=⌊Pt+3(T^t)/8⌋N_t(z)=\lfloor P_{t+3}(\widehat T_t)/8\rfloor satisfies ∣Nt(z)−2tz∣<3/2<2|N_t(z)-2^tz|<3/2<2, and Nt(z)N_t(z) modulo 2q2^q can be computed from Pt+3P_{t+3} modulo 2q+32^{q+3}.

Why it's here

Since α,β\alpha,\beta are exact rationals fixed by the first kk places and the tail ee has a simple exact stream, the linear expression can be assembled using only the elementary and multiplication lemmas, so the reciprocal inherits their clock, record and space bounds. The previous claim's bound 2t∣Tt−z∣≤1/42^t|T_t-z|\leq 1/4 (preserved by clipping), together with rounding at place t+3t+3, gives the integer error below 2. The residue handoff from Pt+3P_{t+3} mod 2q+32^{q+3} to NtN_t mod 2q2^q lets the reciprocal be used as an ordinary residue procedure.
Classified routine:
Direct consequence of the earlier elementary and multiplication lemmas together with the previous claim's error bound 2t∣Tt−z∣≤1/42^t|T_t-z|\le 1/4. The remaining steps are rounding and residue bookkeeping, a standard calculation.

Uses

lemElementary arithmetic operations have linear-space residue procedureslemMultiplication with linear clock-gap storageclaimFirst-order reciprocal expansion with quadratic error

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Exact stream via elementary ops and multiplication" rests on claim-lem-arith-reciprocal-1