lemmaroutine

Elementary arithmetic operations have linear-space residue procedures

Averaging, max, min, shifts have residue procedures in O(t+1)O(t+1) local space
base clock and record bounds for composite arithmetic
Lemma·lem:arith-elementary·§10.2 Truncations, comparisons, and binary arithmetic

Statement (paper)

The normalized operations of taking a pair average, a maximum or minimum, and a fixed binary shift admit deterministic integers satisfying Equation . Their residue procedures, for any fixed qq, have the following properties. There are constants C0,C1C_0,C_1 such that an operand place jj obeys j≤t+C0j\leq t+C_0, its suspended local record has length at most C0+C1(t−j)C_0+C_1(t-j), and the intrinsic local space is O(t+1)O(t+1). Fixed finite compositions of these normalized operations have the same bounds, with enlarged constants. Fixed Boolean operations on returned digit codes, including sign decoding and conditional selection of code bits, add only constant local overhead.

In plain English

Pair averaging, maximum, minimum and a fixed binary shift on normalized values have deterministic integer approximations satisfying the paper's approximation bound. For any fixed qq, their residue procedures request operand places j≤t+C0j\leq t+C_0, suspend local records of length at most C0+C1(t−j)C_0+C_1(t-j), and use O(t+1)O(t+1) intrinsic local space; fixed finite compositions and fixed Boolean operations on returned digit codes (sign decoding, conditional selection of code bits) keep these bounds with larger constants.

Why it's here

This sets the basic clock, suspended-record and intrinsic-space bounds for the simplest arithmetic gates, applying the path-only storage accounting of the gate-evaluation lemma. The reciprocal, rank, bounded-sum and interface results build on it, since they compose these operations with only enlarged constants and so can reuse the same bounds.
Classified routine:
These are the standard online/streaming digit-by-digit procedures for averaging, max/min and shifting binary-expansion values. They are combined with the paper's path-only storage accounting from the gate-evaluation lemma, which amounts to bookkeeping of carry lookahead and constant-overhead record sizes.

Uses

lemDepth-first circuit evaluation uses path-only storage

Used by

lemReciprocal with early-word storagelemOrder statistics have linear-space residue procedureslemBalanced sums and scalings stay within local boundsclaimClipped reciprocal approximation has exact streamsclaimSuffix branch holds no coefficient wordclaimOne clock coefficient works throughout

Sources

PaperOpen
Section
§10.2 Truncations, comparisons, and binary arithmetic
Page
—
Label
lem:arith-elementary
Line
sections/arithmetic.tex:156
Leannot aligned

Phase 2 aligns this node to a Lean declaration.