lemmaroutine

Approximate integers give exact digit streams

Integers with ∣Nt−2tz∣<2|N_t-2^tz|<2 yield an exact digit stream via residues mod 2q2^q
makes primitives exact, so errors do not accumulate
Lemma·lem:arith-residue-stream·§10.1 Streams, records, and uniformity

Statement (paper)

Suppose ∣z∣≤1|z|\leq1 and, for each t≥0t\geq0, a deterministic integer Nt(z)N_t(z) satisfies ∣Nt(z)−2tz∣<2. |N_t(z)-2^tz|<2. Set z0=N0(z),zt=Nt(z)−2Nt−1(z)(t≥1). z_0=N_0(z),\qquad z_t=N_t(z)-2N_{t-1}(z)\quad(t\geq1). Then zt∈Az_t\in\mathcal A and these digits represent zz exactly. For any fixed integer q≥4q\geq4, each output digit is determined by the required NtN_t residues modulo 2q2^q.

In plain English

If integers Nt(z)N_t(z) satisfy ∣Nt(z)−2tz∣<2|N_t(z)-2^tz|<2 for ∣z∣≤1|z|\leq1, then the differences z0=N0z_0=N_0, zt=Nt−2Nt−1z_t=N_t-2N_{t-1} are digits in A\mathcal A that represent zz exactly. For any fixed q≥4q\geq4, each digit is determined by the residues of the needed NtN_t modulo 2q2^q.

Why it's here

This lets every primitive be specified by cheap approximations NtN_t and still produce an exact digit stream, which is what the reciprocal lemma and the interface theorem rely on when composing primitives. The digits telescope, so ∑t≤Tzt2−t=NT2−T→z\sum_{t\le T}z_t2^{-t}=N_T2^{-T}\to z. The error bound makes each ztz_t small, and a small integer is recovered from its residue modulo 2q2^q once q≥4q\geq4, so only low-order bits of NtN_t need to be kept.
Classified routine:
This is the standard conversion from integer approximations to a redundant signed-digit expansion, as in exact real arithmetic (e.g., Avizienis-style redundant digits and Boehm-type approximation functions). Telescoping and bounding each digit is direct, and recovering a small integer from its residue mod 2q2^q is elementary.

Uses

Nothing else in the paper

Used by

lemReciprocal with early-word storagethmUniform numerical interface for arithmetic recipesclaimCoefficient digits via integer arithmeticclaimPrimitives compose into exact streams

Sources

PaperOpen
Section
§10.1 Streams, records, and uniformity
Page
—
Label
lem:arith-residue-stream
Line
sections/arithmetic.tex:57
Leannot aligned

Phase 2 aligns this node to a Lean declaration.