claimroutineinferred_dep

Rotations cost O(V L^τ) via swaps

Rotations cost

O(VL^\tau)

via at most sixteen chunk swaps

gives the main

VL^\tau

term

Claim·§5.2 Packed changes of selected address bits·inside lemPacked XOR of selected address bits

Statement (paper)

Each of the (at most eight) rotations in

S_0

can be implemented on tapes in time

O(V L^\tau)

, including the (at most sixteen) chunk swaps used to move the target after its two controls and to undo this afterwards. Each swap costs

O(VL^\tau)

via Lemma and each rotation costs

O(V)

via Lemma , using local descriptors of

O(A_{\rm rect})

bits and with the offset routine running in

L^{O(1)}

time, so

S_0

is implemented in time

O(VL^\tau)

with the field-length list unchanged by completed swaps.

In plain English

The at most eight packed rotations making up

S_0

can be run on tapes in total time

O(VL^\tau)

, counting the at most sixteen chunk swaps that bring the target after its two controls and restore the order afterwards. The field-length list is unchanged once the swaps are completed.

Why it's here

Each chunk swap costs

O(VL^\tau)

by the chunk-swap lemma, and each rotation is a controlled shift costing

O(V)

by the ordered affine streams lemma, since its offset has

O(A_{\rm rect})

bits and is computed in

L^{O(1)}

time. With a constant number of swaps and rotations, this gives the

V L^\tau

term of the total time bound, which the final cost claim combines with the other terms.

Classified routine:

This is cost bookkeeping: a constant number of chunk swaps, each O(VL^τ) by the paper's chunk-swap lemma, plus a constant number of rotations, each O(V) by the ordered affine streams lemma, add up to the stated bound.

Uses

lemSwapping binary address chunks in O(Vu^τ)lemAffine updates on digit fields cost linear timeclaimPacked shifts match ideal XOR off bad set

Used by

claimTotal cost and asymptotic simplification

Sources

PaperOpen

Section: §5.2 Packed changes of selected address bits
Page: —
Label: —
Line: sections/05-layers.tex:353

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Rotations implemented by swaps and controlled shifts" rests on claim-lem-packed-selected-bit-rectangle-2