lemmaroutine

Reciprocal with early-word storage

Reciprocal on [a,b][a,b] meets the elementary bounds, long word only at early places
reciprocal primitive in the numerical interface
Lemma·lem:arith-reciprocal·§10.4 Reciprocals and the early-word convention

Statement (paper)

Fix constants 0<a≤b0<a\leq b. On inputs x∈[a,b]x\in[a,b], a reciprocal, after a fixed known normalization, has the same operand-clock, suspended-record, and intrinsic-space bounds as in Lemma . Its local record may contain an O(t+1)O(t+1)-bit word only while querying input places j≤⌊t/2⌋+O(1)j\leq\lfloor t/2\rfloor+O(1).

In plain English

For fixed constants 0<a≤b0<a\leq b, the reciprocal of a normalized input x∈[a,b]x\in[a,b] has the same operand-clock, suspended-record and intrinsic-space bounds as the elementary operations. Its local record may hold an O(t+1)O(t+1)-bit word only while querying input places j≤⌊t/2⌋+O(1)j\leq\lfloor t/2\rfloor+O(1).

Why it's here

The key idea is a first-order expansion of 1/(Cx)1/(Cx) around the truncation of xx at about t/2t/2 places. The error is quadratic, so only the early places are needed for the long coefficient word, and the rest is a linear function of the unread tail built from elementary operations and multiplication. Residue-stream conversion then yields exact digits. This lets reciprocals be composed in the uniform numerical interface without breaking the linear-space storage accounting.
Classified routine:
A first-order Newton-type expansion of 1/(Cx) around a truncation of x at about t/2 places, with quadratic error. The paper then assembles it from its earlier elementary-operation, multiplication and residue-stream lemmas, which makes it an adaptation of standard numerical-analysis technique to the paper's storage accounting.

Uses

lemElementary arithmetic operations have linear-space residue procedureslemMultiplication with linear clock-gap storagelemApproximate integers give exact digit streams

Used by

thmUniform numerical interface for arithmetic recipesclaimOne clock coefficient works throughout

Inside the proof

claimFirst-order reciprocal expansion with quadratic errorclaimClipped reciprocal approximation has exact streamsclaimCoefficient digits via integer arithmeticclaimEarly-word payment at early input placesclaimSuffix branch holds no coefficient word

Sources

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

Phase 2 aligns this node to a Lean declaration.