lemmaroutine

Swapping binary address chunks in O(Vu^τ)

Swaps two

2^u

-sized address chunks of a bit array in

O(Vu^\tau)

steps

general axis-moving tool at sublinear cost per bit

Lemma·lem:chunk-swap·§4.3 Removing width and row restrictions

Statement (paper)

There exist fixed

0<\tau<1

and one fixed finite-alphabet multitape procedure with the following property. For positive integers

P,G,B

and

u\ge1

, it transforms an arbitrary bit array on

[P]\times[2^u]\times[G]\times[2^u]\times[B]

by the address permutation

(p,h,g,d,z)\longmapsto(p,d,g,h,z)

O(Vu^\tau)

steps, where

V=PG B\,2^{2u}

. The integers specifying the shape are part of the input. The time includes their processing, all padding and unpadding, and fixed-tape workspace cleanup. In particular,

B=1

is allowed.

In plain English

On a bit array indexed by

[P]\times[2^u]\times[G]\times[2^u]\times[B]

, the address permutation

(p,h,g,d,z)\mapsto(p,d,g,h,z)

can be done by one fixed multitape procedure in

O(Vu^\tau)

steps, where

V=PGB\,2^{2u}

and

\tau<1

is a fixed constant. The bound includes shape processing, padding, unpadding and cleanup, and allows

B=1

Why it's here

This turns the power-width interchange primitive, which only handles chunk widths

m^k

with a divisibility condition on the preceding row field, into an unrestricted chunk swap on binary-width chunks. The proof pads

2^u

to a radix-

q

range

q^e

, swaps the top

\rho=O(\log e)

digits to build a row field with the needed divisibility, then splits the remaining width in base

m

into power-width swaps. Later lemmas use it as the general tool for moving axes and bit fields at cost

O(Vu^\tau)

, sublinear in

u

per entry.

Classified routine:

Extends the power-width interchange proposition to arbitrary binary-width chunks by padding 2^u to q^e, fixing divisibility with a short top-digit swap, and splitting the width in base m. This is bookkeeping built on prop-power-interchange and the linear-time elementary digit scans.

Uses

lemElementary digit scans run in linear timepropPower-width chunk interchange in O(Ve^τ)

Used by

lemPacked XOR of selected address bitslemCost and accuracy of synthetic transformlemTensor resampling across d dimensionsclaimRotations cost O(V L^τ) via swapsclaimLayout permutation by moves and chunk exchangesclaimAxis exposure costs via chunk swapsclaimCRT address map via controlled shiftsclaimCost table yields the final time bound

Inside the proof

claimExchange high digits to form row fieldclaimBase-m pieces via power-width interchangesclaimPadding binary chunks to radix-q ranges

Sources

PaperOpen

Section: §4.3 Removing width and row restrictions
Page: —
Label: lem:chunk-swap
Line: sections/04-swap.tex:285

Leannot aligned

Phase 2 aligns this node to a Lean declaration.