lemmaroutine

Elementary digit scans run in linear time

Four digit-level array rearrangements each run in O(V)O(V) time
linear-time tape toolbox for rearranging arrays
Lemma·lem:elementary-streams·§2.1 Array order and elementary scans

Statement (paper)

Fix a radix q≥2q\ge2. Each of the following operations on an array of volume VV takes O(V)O(V) steps on a fixed number of one-dimensional tapes: \begin{enumerate} \item any fixed permutation of the pair of digit values at two specified radix-qq positions, whether or not the positions are adjacent; \item moving one specified radix-qq digit to another position, preserving the order of the intervening positions; \item splitting on a specified radix-qq digit, applying a fixed pointwise map to aligned streams, and merging them back; \item for positive integers P,R,BP,R,B, within each prefix of an array on [P]×[R]×[B][P]\times[R]\times[B], splitting whole rows cyclically into a fixed number WW of streams, and, when WW divides RR, merging those streams in any fixed order of the row classes. \end{enumerate} The bounds include shape preparation, counter initialization and resets, and returning or clearing the visited portions of work tapes. Their constants may depend on the fixed radix, the fixed pointwise map, and the fixed number of row classes.

In plain English

For a fixed radix q≥2q\ge2 and an array of volume VV, four digit-level operations each take O(V)O(V) steps on a fixed number of one-dimensional tapes. They are permuting the digit values at two positions, moving one digit to another position, splitting on a digit with a pointwise map and merging, and cyclically splitting and merging whole rows in a [P]×[R]×[B][P]\times[R]\times[B] array.

Why it's here

This lemma is the toolbox of linear-time tape primitives that later lemmas and claims cite for rearranging arrays without paying extra overhead. Because the bounds include shape preparation, counters and tape cleanup, later arguments can use these operations as plain O(V)O(V) steps.
Classified routine:
Standard multitape Turing machine techniques: a fixed-radix digit permutation, split or merge can be done with a constant number of linear streaming passes using counters. This follows the usual tape-model data rearrangement arguments, as in the Schönhage–Strassen and Harvey–van der Hoeven tape implementations.

Sources

PaperOpen
Section
§2.1 Array order and elementary scans
Page
—
Label
lem:elementary-streams
Line
sections/02-streams.tex:60
Leannot aligned

Phase 2 aligns this node to a Lean declaration.