theoremroutine

Uniform numerical interface for arithmetic recipes

Bounded arithmetic recipes have exact digit streams with j≤t+cdj\le t+cd and records ad+b(t−j)ad+b(t-j)
black-box numerical interface for the controller construction
Theorem·thm:arith-interface·§10.6 The numerical interface

Statement (paper)

Fix the digit alphabet, positive reciprocal intervals, and constants bounding the following recipe class. A recipe at slack d≥1d\geq1 has a fixed number of stages built from bounded arithmetic operations, fixed piecewise formulas using maxima, minima and clipping, the reciprocals of Lemma , indexed ranks as in Lemma , and sums and known scales as in Lemma . The stage and descriptor descriptions are generated from the root parameters by index computations using O(B+d+t)O(B+d+t) scratch and no operand queries, and the total non-reduction dependency depth is bounded independently of dd. Each indexed domain has size 2O(d)2^{O(d)} and descriptors of length O(d)O(d). Discrete domain and validity decisions are structural leaves or buffered tests with their own fixed precision conventions. Public coefficient leaves have exact normalized digit procedures using O(B+d+t)O(B+d+t) shared scratch and making no operand or recursive graph queries. Then each normalized recipe value has a deterministic exact A\mathcal A-stream. For its digit at clock tt there are uniform constants a,b,ca,b,c such that every requested operand digit jj satisfies j≤t+cd,total suspended local binary record length≤ad+b(t−j). j\leq t+cd,\qquad \text{total suspended local binary record length} \leq ad+b(t-j). An output code bit satisfies the same bounds. A structural leaf is requested at clock zero and has suspended local length at most ad+btad+bt. The maximum intrinsic local record length is O(d+t)O(d+t). All gate, digit and descriptor addresses can be regenerated from root parameters and the saved local records using O(B+d+t)O(B+d+t) shared scratch and no recursive graph calls. When d,t=O(B)d,t=O(B) this is O(B)O(B) scratch. If a public rational coefficient has O(B)O(B)-bit numerator and denominator that can be generated in O(B)O(B) scratch, its queried digits in this clock range also require only that shared O(B)O(B) scratch.

In plain English

Every recipe in the bounded class (fixed stages built from bounded arithmetic, clipping, reciprocals, ranks, sums and scales, with 2O(d)2^{O(d)}-size domains and bounded depth) has an exact digit stream. Requested operand digits satisfy j≤t+cdj\leq t+cd and suspended local length at most ad+b(t−j)ad+b(t-j), and all addresses are regenerable in O(B+d+t)O(B+d+t) shared scratch without recursive graph calls.

Why it's here

This packages the elementary, reciprocal, rank, sum and buffered-test lemmas into one export bound (eq:arith-export) that later constructions can use without re-checking each arithmetic step. Exact residue streams stop errors from accumulating, a single clock coefficient bb lets the clock-gap terms telescope across nested stages so only an O(d)O(d) overshoot accumulates, and path-only depth-first storage keeps addresses regenerable in shared scratch.
Classified routine:
Packages the preceding lemmas (residue streams, reciprocals, ranks, sums/scales, buffered tests, depth-first path-only gate evaluation) into a single export bound. This is bookkeeping: it composes them and lets the clock-gap terms telescope across a bounded number of stages, in the style of online/redundant-digit exact real arithmetic.

Uses

lemApproximate integers give exact digit streamslemBalanced sums and scalings stay within local boundslemReciprocal with early-word storagelemFinite buffered comparison test for sumslemDepth-first circuit evaluation uses path-only storage

Used by

thmController interfaces have restoring O(B)-space implementationslemEstimator recipes have regenerable records and bounded controllemControl records replay with later-salt independencethmDeterministic logspace approximation of acceptance probabilityclaimInductive construction of total restoring proceduresclaimImmediate paths and factor values certifiedclaimCandidate domain and bucket sumsclaimFinite acyclic stratum ordering within groupclaimUniform generation and arithmetic record boundsclaimNumerical places recovered with one scratchclaimTruncated digits give accurate dyadic values

Inside the proof

claimPrimitives compose into exact streamsclaimOne clock coefficient works throughoutclaimStructural leaves and buffered tests use fixed precisionclaimAddresses regenerable from saved choicesclaimPublic coefficients via shared-scratch division

Sources

PaperOpen
Section
§10.6 The numerical interface
Page
—
Label
thm:arith-interface
Line
sections/arithmetic.tex:742
Leannot aligned

Phase 2 aligns this node to a Lean declaration.