lemmaroutine

Matrix shear via few interchanges

Shear (H,D)↦(H+AD,D)(H,D)\mapsto(H+AD,D) costs rank AA interchanges plus O(V)O(V)
edge shear primitive for the circuit-based interchange
Lemma·lem:matrix-shear·§4.1 A matrix decomposition adapted to tape order

Statement (paper)

Let A\mathcal A be a fixed finite collection of rational m×mm\times m matrices. There is a fixed odd prime qq such that the following holds. Let H=(H1,…,Hm)H=(H_1,\ldots,H_m) and D=(D1,…,Dm)D=(D_1,\ldots,D_m) be two ordered groups of fields, every field ranging over [qb][q^b], with every HiH_i before every DjD_j. For A∈AA\in\mathcal A of rational rank aa, the permutation (H,D)⟼(H+AD,D)over Z/qbZ (H,D)\longmapsto(H+AD,D) \quad\text{over }\mathbb Z/q^b\mathbb Z can be performed with exactly aa interchanges of pairs of bb-digit fields and O(V)O(V) further work. Every interchange is between an HH field and a DD field. Spectators between any of the formal fields are allowed.

In plain English

For a fixed finite set of rational m×mm\times m matrices, there is a fixed odd prime qq such that for each AA of rank aa, the map (H,D)↦(H+AD,D)(H,D)\mapsto(H+AD,D) over Z/qbZ\mathbb Z/q^b\mathbb Z can be done with exactly aa interchanges of bb-digit fields, each between an HH field and a DD field, plus O(V)O(V) other work, even with spectators in between.

Why it's here

Factor A=E1ΠE2A=E_1\Pi E_2 using the lower-Bruhat factorization. The lower triangular parts E1,E2E_1,E_2 act as affine updates that use only earlier fields, so they cost O(V)O(V) by the affine-update lemma, and qq is chosen so the needed rational units are invertible mod qbq^b. The partial permutation Π\Pi with aa ones is the only part that needs interchanges, one per one. This gives the power-width interchange proposition its shear primitive for each circuit edge matrix at a cost counted by rank.
Classified routine:
Direct consequence of the lower-Bruhat factorization A=E_1ΠE_2 combined with the paper's affine-update lemma. Only the partial permutation Π needs interchanges, one per nonzero entry, which is a standard bookkeeping argument.

Uses

lemLower-Bruhat factorization of rational matriceslemAffine updates on digit fields cost linear time

Used by

propPower-width chunk interchange in O(Ve^τ)claimCircuit on role streams realizes shear

Sources

PaperOpen
Section
§4.1 A matrix decomposition adapted to tape order
Page
—
Label
lem:matrix-shear
Line
sections/04-swap.tex:48
Leannot aligned

Phase 2 aligns this node to a Lean declaration.