claimroutineinferred_dep

Circuit on role streams realizes shear

Circuit on role streams performs

H\leftarrow H+D

on every row

gives the circuit-based shear used in the swap

Claim·§4.2 Transferring a finite circuit to address permutations·inside propPower-width chunk interchange in O(Ve^τ)

Statement (paper)

Executing the circuit on the

W

role streams, with

\Phi_{A_e}

applied to the role stream on every circuit edge

e

and each gate executed pointwise at matching addresses, and then merging the streams back to the original row order, realizes the shear

H\leftarrow H+D

on every original row, including rows assigned to scratch roles whose initial values were arbitrary.

In plain English

Running the circuit on the

W

role streams, applying the edge shears

\Phi_{A_e}

on each edge and gates pointwise at matching addresses, then merging the streams back to row order, performs

H\leftarrow H+D

on every original row, including scratch-role rows with arbitrary initial values.

Why it's here

This is the step where the finite circuit's rational-matrix data is turned into an actual shear on all rows. Because the circuit's net matrix difference is the identity from input to output role, the edge shears from the matrix-shear lemma, with their rank-bounded interchange counts, compose into

H\leftarrow H+D

, and it holds regardless of what the scratch rows held. The next claim then chains three such shears to swap the chunks.

Classified routine:

Direct consequence of the matrix-shear lemma composed along the circuit edges, with the role-stream split from the previous claim: linearity and the identity net matrix from input to output role give H<-H+D. This is bookkeeping that transfers a linear circuit's behaviour to the address-permutation setting.

Uses

lemMatrix shear via few interchangesclaimSplit rows cyclically into role streamspropBit network matrix interface and rank sum

Used by

claimThree shears interchange the two chunks

Sources

PaperOpen

Section: §4.2 Transferring a finite circuit to address permutations
Page: —
Label: —
Line: sections/04-swap.tex:158

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Circuit with shear frames yields H←H+D everywhere" rests on claim-prop-power-interchange-1
info
inferred_dep
outline: "Circuit with shear frames yields H←H+D everywhere" rests on prop:bit-motif-interface