claimroutine

Primitives compose into exact streams

Exact digit streams compose, so approximation errors never accumulate

gives compositionality of primitives in recipes

Claim·§10.6 The numerical interface·inside thmUniform numerical interface for arithmetic recipes

Statement (paper)

Each primitive construction defines deterministic integers

N_t

, and by Lemma these give exact streams. When primitives are composed, their operands are these exact streams, and each primitive's deterministic

N_t

approximates its own exact mathematical value, so numerical approximation errors are not accumulated along the recipe as statistical errors. The construction uses only residues of

N_t

and

N_{t-1}

and a constant number of output code bits, which adds only fixed overshoot and fixed local overhead.

In plain English

Each primitive is defined by deterministic integers

N_t

that, by the residue-stream lemma, yield an exact digit stream. Composing primitives therefore feeds exact streams as operands, so approximation errors do not accumulate along the recipe, and only residues of

N_t

and

N_{t-1}

plus a constant number of output code bits are needed.

Why it's here

This step of the interface theorem's proof turns the residue-stream lemma into a compositional guarantee: each primitive's

N_t

approximates its own exact value, and its output is an exact stream, so errors do not propagate to later stages. Because only residues of

N_t

and

N_{t-1}

and a constant number of code bits are used, the overhead is a fixed overshoot and fixed local length, which fits the bounds in the export inequality.

Classified routine:

Direct consequence of the residue-stream lemma (lem-arith-residue-stream), applied to each primitive in turn. It is compositional bookkeeping in the spirit of exact real arithmetic with redundant signed-digit streams.

Uses

lemApproximate integers give exact digit streams

Used by

Nothing in the paper

Sources

PaperOpen

Section: §10.6 The numerical interface
Page: —
Label: —
Line: sections/arithmetic.tex:787

Leannot aligned

Phase 2 aligns this node to a Lean declaration.