lemmaroutine

Atom ports: bounded rows with smooth witnesses

Rows are bounded-degree ports with smooth witnesses and incoming cap KcK_c
bounded-degree access ports for assembly, paths and recipes
Lemma·lem:atom-ports·§5.5 Actual ports and estimated assembly

Statement (paper)

All main and preparatory row tables, auxiliary scores, and the smooth witnesses just constructed have bounded values and bounded row support. Every row access class used for a main or preparatory output, or for access to its auxiliary score, has bounded size and a smooth witness equal to one on every exposed entry, including exposed entries of weight zero. A witness itself is needed as an analytical row function, without an additional requirement to expose its support through a further witness. For a correction or its preparatory table let AA be its pre-incoming class from Equation . Retain an exposed entry (x,y)∈A(x,y)\in A only when #{x′:Xu(x′)=1, (x′,y)∈A}≤Kc. \#\{x':X_u(x')=1,\ (x',y)\in A\}\le K_c. This deletion preserves all table values and gives at most K−1K-1 outgoing and at most KcK_c incoming exposed entries. These assertions hold separately for every computed version, provided that its values, ranks, scores, and access classes use the same final raw arrays and common task tuple. Access ports denote distinct entries: the implementation must expose each pair at most once and pair its incoming and outgoing ports consistently. Access to auxiliary scores alone has only the asserted row bound.

In plain English

All main and preparatory row tables, auxiliary scores and their smooth witnesses have bounded values and bounded row support, and each row access class has bounded size with a smooth witness equal to one on every exposed entry (including weight-zero ones). For corrections, keeping an exposed entry (x,y)(x,y) of the pre-incoming class AA only when at most KcK_c sources x′x' with Xu(x′)=1X_u(x')=1 hit yy leaves table values unchanged and yields at most K−1K-1 outgoing and at most KcK_c incoming exposed entries per port.

Why it's here

This turns the sparsity and exposure of Atom margins (which hold for arbitrary real raw estimates) into concrete bounded-degree access ports with smooth witnesses, including an incoming cap KcK_c enforced by deleting entries without changing values. These ports are what the assembly comparisons, path and recipe certificates and final row-class wrappers rely on. The statements hold separately for each computed version, provided it uses the same final raw arrays and common task tuple, and each exposed pair is exposed once with incoming and outgoing ports paired consistently.
Classified routine:
This is bookkeeping that follows directly from the Atom margins lemma (lem-atom-margins): it turns the sparse exposed classes into bounded-degree ports, and the incoming cap K_c is enforced by deleting entries in a way that leaves table values unchanged. It adds no new idea beyond that lemma.

Uses

lemAtom margins: sparse rows with exposed classes

Used by

lemAssembly of row and cutoff discrepancieslemImmediate candidates are short and well-formedlemEstimator recipes have regenerable records and bounded controllemControl records replay with later-salt independenceclaimEscape indicator bounded by witness discrepancyclaimFinal row classes and wrappers add fixed strataclaimEstimator edges determine descendant tuples

Sources

PaperOpen
Section
§5.5 Actual ports and estimated assembly
Page
—
Label
lem:atom-ports
Line
sections/atoms.tex:579
Leannot aligned

Phase 2 aligns this node to a Lean declaration.