claimroutine

Exchange high digits to form row field

Swapping top ρ=O(log⁡e)\rho=O(\log e) digits builds a row field divisible by WkW^k
creates the divisible row field for power-width swaps
Claim·§4.3 Removing width and row restrictions·inside lemSwapping binary address chunks in O(Vu^τ)

Statement (paper)

For all sufficiently large ee, with k=⌈log⁡me⌉k=\lceil\log_m e\rceil and ρ=⌈klog⁡W/(2log⁡q)⌉\rho=\lceil k\log W/(2\log q)\rceil, one has 1≤ρ<e1\le\rho<e and ρ=O(log⁡(2e))\rho=O(\log(2e)). Interchanging the top ρ\rho digits of the two chunks and joining the resulting high parts transforms the field order (h+,h−,g,d+,d−)(h^+,h^-,g,d^+,d^-) into (d+,h+,h−,g,d−)(d^+,h^+,h^-,g,d^-) in O(Vρ)O(V\rho) steps, preserving the order of the remaining digits and the gap field, so that the first two fields form a row field of range R=q2ρ≥WkR=q^{2\rho}\ge W^k before both remaining chunks. Appending zero rows separately within each preceding prefix brings the row count to R′=Wk⌈R/Wk⌉<2RR'=W^k\lceil R/W^k\rceil<2R, so that the padded logical volume is less than 2V2V.

In plain English

For large ee, with k=⌈log⁡me⌉k=\lceil\log_m e\rceil and ρ=⌈klog⁡W/(2log⁡q)⌉\rho=\lceil k\log W/(2\log q)\rceil, we have 1≤ρ<e1\le\rho<e and ρ=O(log⁡(2e))\rho=O(\log(2e)). Interchanging the top ρ\rho digits of the two chunks and joining the high parts turns the order (h+,h−,g,d+,d−)(h^+,h^-,g,d^+,d^-) into (d+,h+,h−,g,d−)(d^+,h^+,h^-,g,d^-) in O(Vρ)O(V\rho) steps, giving a row field of range R=q2ρ≥WkR=q^{2\rho}\ge W^k ahead of both remaining chunks. Padding with zero rows within each prefix then makes the row count R′=Wk⌈R/Wk⌉<2RR'=W^k\lceil R/W^k\rceil<2R, so the padded volume is below 2V2V.

Why it's here

This step creates a row field whose range is a multiple of WkW^k by moving only ρ=O(log⁡e)\rho=O(\log e) digits, which costs O(Vρ)O(V\rho) instead of a full chunk exchange. The padded row count R′R' is then common to all rows, which the next claim (base-m pieces via power-width interchanges) needs. The digit moves are carried out with the elementary linear-time stream operations.
Classified routine:
Bookkeeping step inside the chunk-swap lemma: it performs ρ=O(log e) digit interchanges, each costing O(V) by the elementary linear-time stream operations lemma, and pads with zero rows. This is a parameter calculation plus a direct application of that earlier lemma, not a new idea.

Uses

lemElementary digit scans run in linear time

Used by

claimBase-m pieces via power-width interchanges

Sources

PaperOpen
Section
§4.3 Removing width and row restrictions
Page
—
Label
—
Line
sections/04-swap.tex:304
Leannot aligned

Phase 2 aligns this node to a Lean declaration.