lemmaroutine

Assembly of row and cutoff discrepancies

Assembled output discrepancy is a constant times the ingredients' discrepancies

charges assembly errors to child discrepancies

Lemma·lem:atom-assembly·§5.6 Integrated losses and assembly bounds

Statement (paper)

Compare two versions with the same environment, rates, and task tuple. For a sparse normalized output write

H=P T g

and

H'=P'T'g'

, where

P,P'

are the pre-incoming clipped-ratio row functions (including their usage masks),

I,I'

are their auxiliary scores, and

g,g'

are their column multipliers. If

g,g'

are the prescribed smooth cutoffs of bounded vertex arrays

U_i,U_i'

, then

\mathfrak d_{u,f}(H,H')^s \le C\mathfrak d_{u,f}(P,P')^s +C\mathfrak d_{u,f}(I,I')^s +C\frac fu\sum_i\|U_i-U_i'\|_{f;s}^s.

For a sparse preparation omit the last term and use its unnormalized pre-incoming row function. The corresponding dense and detector row functions have no incoming or column-multiplier assembly cost. If

V_y,V_y'

are the detector trials formed from

\mathcal S_i,\mathcal S_i'

by their column order statistic, then

\|V-V'\|_{f;s}^s \le C\mathfrak d_{f,f}(\mathcal S_i,\mathcal S_i')^s.

In plain English

For two versions of a sparse normalized output

H=PTg

and

H'=P'T'g'

with the same environment, rates and task tuple, the

s

-th power of the discrepancy

\mathfrak d_{u,f}(H,H')

is at most a constant times the sum of the discrepancies of the row functions

P,P'

, of the auxiliary scores

I,I'

, and of

\frac fu\sum_i\|U_i-U_i'\|_{f;s}^s

for the vertex arrays behind the smooth cutoffs. Sparse preparations drop the last term, dense and detector row functions incur no assembly cost, and detector trials satisfy

\|V-V'\|_{f;s}^s\le C\mathfrak d_{f,f}(\mathcal S_i,\mathcal S_i')^s

Why it's here

This lemma shows that assembling an output from clipped-ratio rows, incoming normalization and column multipliers adds only constant-factor losses, so discrepancy of the assembled output is controlled by the discrepancies of its ingredients. It relies on the bounded rows and smooth witnesses from the atom ports lemma. The later coupling and error-reserve arguments use it to charge assembly errors to child discrepancies.

Classified routine:

Direct stability bookkeeping: combines the bounded rows and smooth witnesses from the atom-ports lemma with Lipschitz bounds for products, smooth cutoffs and order statistics, so assembly costs only constant-factor losses.

Uses

lemAtom ports: bounded rows with smooth witnesses

Used by

propError reserve after compression and clampingpropActual runs stay close to clean runsclaimCoupling recurrence from child charges

Sources

PaperOpen

Section: §5.6 Integrated losses and assembly bounds
Page: —
Label: lem:atom-assembly
Line: sections/atoms.tex:700

Leannot aligned

Phase 2 aligns this node to a Lean declaration.