claimroutineinferred_dep

Layout permutation by moves and chunk exchanges

Layout

L

costs

O(Tp[dK+pK^{\tau-1}])

via slot moves and chunk swaps

groups chunks so each round sees

D

consecutive chunks

Claim·§6.2 A layout on which the parallel layers apply·inside lemCost and accuracy of synthetic transform

Statement (paper)

Put

D=d-1

b=(\ell-1)\bmod K

and

q=\lfloor(\ell-1)/K\rfloor

. Moving to a prefix the at most

D(b+1)=O(dK)

listed slots (the slots

(i,\ell-1)

of the length-

2^\ell

axes, then the slots

(i,h)

for

h=b-1,\ldots,0

), and then exchanging at most

Dq-1

width-

K

address chunks to reorder the remaining

q

chunks of each axis from axis-major to chunk-major order, defines a positional permutation

L

of record addresses that preserves polynomial suffixes. Constructing

L

and its inverse

L^{-1}

, and applying either to the disk grid array, costs

O\bigl(Tp\,[dK+pK^{\tau-1}]\bigr)

In plain English

With

D=d-1

b=(\ell-1)\bmod K

and

q=\lfloor(\ell-1)/K\rfloor

, moving the

O(dK)

listed slots to a prefix and then exchanging at most

Dq-1

width-

K

address chunks (axis-major to chunk-major order) gives a positional permutation

L

of record addresses that preserves polynomial suffixes. Building

L

and

L^{-1}

and applying either to the disk grid array costs

O(Tp[dK+pK^{\tau-1}])

Why it's here

This fixes the layout on which the parallel layers act: the low slots sit in a prefix and the remaining address bits are grouped by chunk index across axes, so each round sees a group of

D

consecutive chunks. The cost bound comes from using linear-time digit moves for the prefix slots and the chunk-swap lemma, at

O(Vu^\tau)

per swap with

u=K

, for the at most

Dq-1

exchanges.

Classified routine:

Direct bookkeeping consequence of the paper's elementary digit-scan lemma (linear-time digit moves) and chunk-swap lemma (O(Vu^τ) per swap), applied at most Dq−1 times to rearrange the address layout.

Uses

lemSwapping binary address chunks in O(Vu^τ)lemElementary digit scans run in linear time

Used by

claimEach layout round meets layer hypothesesclaimPrefix-slot rounds evaluated bit by bitclaimTwiddle rotations without coefficient sortingclaimFull procedures include layout conjugation

Sources

PaperOpen

Section: §6.2 A layout on which the parallel layers apply
Page: —
Label: —
Line: sections/06-transforms.tex:233

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Construct layout permutation L by moves and exchanges" rests on lem:chunk-swap
info
inferred_dep
outline: "Construct layout permutation L by moves and exchanges" rests on lem:elementary-streams