claimroutine

Split rows cyclically into role streams

Splits rows cyclically into

W

identically shaped role streams

setup for running the circuit on role streams

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

Statement (paper)

Within each prefix preceding the row field, the whole rows can be split cyclically into

W

role streams, by writing the original row number as

r=Wg+(w-1)

with

1\le w\le W

, so that stream

w

has row number

g

. These streams all have exactly the same remaining shape, including the full ranges of

H

and

D

; each has logical volume

V/W

, and its row count is divisible by

W^{k-1}

In plain English

In each prefix before the row field, the whole rows can be split cyclically into

W

role streams by writing the row number as

r=Wg+(w-1)

with

1\le w\le W

. Every stream has the same remaining shape (including the full ranges of

H

and

D

), logical volume

V/W

, and a row count divisible by

W^{k-1}

Why it's here

This is the setup step of the proof: it uses the cyclic row split from the elementary stream toolbox to separate the

W

roles into identically shaped streams, so the circuit can later run on them at matching addresses. The divisibility of the row count by

W^{k-1}

follows from the row field length being divisible by

W^k

, which lets the same argument be repeated on the smaller streams.

Classified routine:

Direct application of the cyclic row split from the paper's elementary stream toolbox (lem-elementary-streams), with the shape, volume, and divisibility checks being bookkeeping from the row field length being divisible by W^k.

Uses

lemElementary digit scans run in linear time

Used by

claimCircuit on role streams realizes shear

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.