lemmaroutine

Edge residuals and rank budget

Edge residuals: only central edges lose rank, total budget Wm−2N+2LWm-2N+2L
supplies residual bases and rank count for interfaces
Lemma·lem:motif-residuals·§3.3 Subspaces attached to the gates

Statement (paper)

Every edge joins comparable nondegenerate labels. The only decreasing edges are the central-wire edges from time 3 to time 4; their dimension loss is hh. Consequently, if cc is the number of central wires per invocation and WW the total number of wires, then L=Ich,∑e∣dim⁡Uhead(e)−dim⁡Utail(e)∣=Wm−2N+2L. L=Ich,\qquad \sum_{e}\bigl|\dim U_{\mathrm{head}(e)}- \dim U_{\mathrm{tail}(e)}\bigr| =Wm-2N+2L. For the binary label space, every nonzero orthogonal residual of an edge has an orthonormal basis.

In plain English

Every edge of the gate network joins comparable nondegenerate labels, and the only edges where label dimension drops are the central-wire edges from time 3 to time 4, each losing hh. With cc central wires per invocation and WW wires in total, the total loss is L=IchL=Ich and the sum of absolute dimension changes over all edges is Wm−2N+2LWm-2N+2L; over F2\mathbb F_2 every nonzero orthogonal residual of an edge has an orthonormal basis.

Why it's here

This lemma packages the edge-by-edge residual table into the facts later interface propositions need: control of the dimension loss, the rank-budget identity from telescoping, and orthonormal bases of the nonzero binary residuals. Those bases are what let the bit and complex motif interfaces factor each edge's transformation through basis vectors of the residual.
Classified routine:
A bookkeeping lemma: the dimension-loss count and the rank-budget identity follow by telescoping the paper's own edge-by-edge residual table, and the orthonormal-basis claim is a standard linear-algebra fact about the binary label space.

Uses

Nothing else in the paper

Used by

propBit network matrix interface and rank sumpropComplex network edges factor into translation kernelsclaimPhase-frame difference factors into translation kernels

Inside the proof

claimEdge residual table; only center 3→4 decreasesclaimTelescoping dimension changes gives rank budgetclaimNonzero binary residuals are nonalternatingclaimNonalternating binary spaces have orthonormal bases

Sources

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

Phase 2 aligns this node to a Lean declaration.