lemmaroutine

Balanced sums and scalings stay within local bounds

Sums and averages over

2^{\kappa d}

terms stay within the local bounds

covers sum and scale stages of recipes

Lemma·lem:arith-sums-scales·§10.5 Indexed ranks, sums, scales, and structural leaves

Statement (paper)

Suppose an immediate descriptor domain has at most

2^{\kappa d}

terms, all required binary scale exponents have magnitude at most

\kappa d

, and every intermediate output has a known range bound

2^{\kappa d}

. A sum over an empty domain is zero, and an average is taken over a public nonempty domain. Balanced sums or averages of these terms, followed by the required known rescalings and bounded clipping, satisfy Equation and have intrinsic local space

O(d+t)

In plain English

If a descriptor domain has at most

2^{\kappa d}

terms, all binary scale exponents have magnitude at most

\kappa d

, and every intermediate output has range bound

2^{\kappa d}

, then balanced sums or averages of the terms, followed by the known rescalings and bounded clipping, satisfy the local bound of Equation (eq:arith-local-bound) and use

O(d+t)

intrinsic local space. An empty sum is zero, and averages are over a public nonempty domain.

Why it's here

This extends the elementary gate bounds from fixed finite compositions to sums and averages over exponentially many terms. Balancing keeps the summation depth proportional to

d

, while the range and scale bounds keep the extra precision within

O(d)

. The uniform numerical interface theorem and its clock-coefficient claim use it to cover the sum and scale stages of a recipe.

Classified routine:

Follows from the elementary gate bounds (lem-arith-elementary) by a standard balanced binary-tree summation argument. The depth is O(log of the number of terms) = O(d), and the per-level rounding error and the extra bits stay O(d) under the given range and scale bounds.

Uses

lemElementary arithmetic operations have linear-space residue procedures

Used by

thmUniform numerical interface for arithmetic recipesclaimOne clock coefficient works throughout

Sources

PaperOpen

Section: §10.5 Indexed ranks, sums, scales, and structural leaves
Page: —
Label: lem:arith-sums-scales
Line: sections/arithmetic.tex:640

Leannot aligned

Phase 2 aligns this node to a Lean declaration.