claimroutineinferred_dep

Telescoping dimension changes gives rank budget

Dimension changes telescope to Wm−2N+2LWm-2N+2L in absolute total
gives the rank-budget identity
Claim·§3.3 Subspaces attached to the gates·inside lemEdge residuals and rank budget

Statement (paper)

With L=IchL=Ich the total dimension loss on the IcIc decreasing central-wire edges, each of loss hh, the sum of absolute dimension changes satisfies ∑e∣dim⁡Uhead(e)−dim⁡Utail(e)∣=Wm−2N+2L\sum_{e}\bigl|\dim U_{\mathrm{head}(e)}-\dim U_{\mathrm{tail}(e)}\bigr|=Wm-2N+2L, since the signed sum of dimension changes telescopes at every gate to Wm−2NWm-2N.

In plain English

The total dimension loss on the IcIc decreasing central-wire edges is L=IchL=Ich, and the sum over all edges of ∣dim⁡Uhead(e)−dim⁡Utail(e)∣|\dim U_{\mathrm{head}(e)}-\dim U_{\mathrm{tail}(e)}| equals Wm−2N+2LWm-2N+2L.

Why it's here

The signed dimension changes telescope at each gate to Wm−2NWm-2N. By the edge residual table, the only decreasing edges are the central-wire edges from time 3 to time 4, each losing hh. Replacing the negative terms by their absolute values therefore adds 2L2L, which gives the rank-budget identity.
Classified routine:
Direct bookkeeping consequence of the edge residual table (previous claim): the signed dimension changes telescope at each gate, and converting the negative terms on the decreasing central-wire edges to absolute values adds twice the total loss.

Uses

claimEdge residual table; only center 3→4 decreases

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Telescoping dimension changes gives rank budget" rests on claim-lem-motif-residuals-1