claimroutineinferred_dep

Base-m pieces via power-width interchanges

Base-mm pieces swap the remaining width in O(Veτ)O(Ve^\tau) total
covers arbitrary width via power-width interchanges
Claim·§4.3 Removing width and row restrictions·inside lemSwapping binary address chunks in O(Vu^τ)

Statement (paper)

With R′=Wk⌈R/Wk⌉<2RR'=W^k\lceil R/W^k\rceil<2R the common padded row length, write e−ρ=∑j=0kajmje-\rho=\sum_{j=0}^{k}a_jm^j with 0≤aj<m0\le a_j<m and partition each remaining chunk into aja_j consecutive pieces of width mjm^j. Applying Proposition  to each corresponding pair of pieces, with the same row field of length R′R' divisible by every WjW^j, interchanges the two remaining chunks, preserves row addresses (so padded rows stay zero and genuine rows are not mixed with padded ones), and costs in total O(V)∑jajmjτ=O(Veτ)O(V)\sum_j a_jm^{j\tau}=O(Ve^\tau). Moreover, computing the piece list and all new shapes costs O(V)O(V) in total, and each call leaves its work tapes clean.

In plain English

After the row field of length R′R' is formed, write e−ρ=∑jajmje-\rho=\sum_j a_j m^j in base mm and split each remaining chunk into aja_j pieces of width mjm^j. Interchanging corresponding pieces with the power-width primitive swaps the two remaining chunks in O(Veτ)O(Ve^\tau) total time, without altering row addresses.

Why it's here

The power-width interchange only handles chunk widths that are powers of mm, so this step covers the arbitrary remaining width e−ρe-\rho by splitting it into base-mm pieces. Because R′R' is divisible by every WjW^j, each piece swap is valid, and the costs sum to O(V)∑jajmjτ=O(Veτ)O(V)\sum_j a_j m^{j\tau}=O(Ve^\tau). Together with the high-digit exchange from the previous claim, this gives a full chunk swap, and the piece list and shapes cost only O(V)O(V) to compute.
Classified routine:
A base-m decomposition of the remaining width, followed by repeated application of the power-width interchange (prop-power-interchange) and a geometric-sum cost bound, is a standard reduction from arbitrary widths to power widths.

Uses

propPower-width chunk interchange in O(Ve^τ)claimExchange high digits to form row field

Used by

claimPadding binary chunks to radix-q ranges

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Base-m pieces via power-width interchanges cost O(Ve^τ)" rests on claim-lem-chunk-swap-1