claimroutine

Edge residual table; only center 3→4 decreases

Residual table: only central edges from time 3 to 4 lose dimension hh
computes edge residual dimensions for the rank budget
Claim·§3.3 Subspaces attached to the gates·inside lemEdge residuals and rank budget

Statement (paper)

With a=dim⁡A=hj−1a=\dim A=h^{j-1} and f=h3−jf=h^{3-j}, every edge joins comparable nondegenerate labels, and the orthogonal residual of each edge and its dimension are as given in the table: (a−1)(h−1)(a-1)(h-1) for X:in→2X:\mathrm{in}\to2 and Y:0→1Y:0\to1, h−1h-1 for X:2→3X:2\to3 and Y:4→5Y:4\to5, 00 for X:3→6X:3\to6, X:6→7X:6\to7, Y:in→0Y:\mathrm{in}\to0, Y:1→4Y:1\to4, (a−1)h(a-1)h for center source→1\to1, hh for center 1→31\to3, 3→43\to4, 4→64\to6, a−1a-1 for side source→0\to0, (a−1)(h−1)+1(a-1)(h-1)+1 for side 0→20\to2, h−2h-2 for side 2→52\to5, 11 for side 5→75\to7, and ah(f−1)ah(f-1) for scratch last→\tosink. Label dimension is nondecreasing along every edge except center 3→43\to4, which removes P⊗F⊗QP\otimes F\otimes Q of dimension hh, so the only decreasing edges are the central-wire edges from time 3 to time 4, each with dimension loss hh.

In plain English

With a=dim⁡A=hj−1a=\dim A=h^{j-1} and f=h3−jf=h^{3-j}, every edge joins comparable nondegenerate labels, and each edge's orthogonal residual has the dimension listed in the table (for example (a−1)(h−1)(a-1)(h-1), h−1h-1, 00, hh, (a−1)h(a-1)h, ah(f−1)ah(f-1)). Label dimension never decreases along an edge except on the central-wire edges from time 3 to time 4, which lose exactly hh dimensions.

Why it's here

This table is the computational core of the parent lemma. It gives the residual dimensions that the later claims need, and it shows that the only decreasing edges are the center 3→4 edges with loss hh. That feeds the telescoping rank-budget count and the check that nonzero binary residuals are nonalternating.
Classified routine:
A direct dimension computation over the specific motif's subspace labels: the residual dimensions follow from linear-algebra bookkeeping (orthogonal complements of tensor-product subspaces) for the gadget defined in the paper. It is a computational step inside the parent lemma, not a new idea.

Uses

Nothing else in the paper

Used by

claimTelescoping dimension changes gives rank budgetclaimNonzero binary residuals are nonalternating

Sources

PaperOpen
Section
§3.3 Subspaces attached to the gates
Page
—
Label
—
Line
sections/03-motifs.tex:366
Leannot aligned

Phase 2 aligns this node to a Lean declaration.