claimroutineinferred_dep

Padding binary chunks to radix-q ranges

Padding [2u][2^u] to [qe][q^e] costs O(V)O(V) and gives O(Vuτ)O(Vu^\tau) overall
reduces binary chunks to the radix-qq case
Claim·§4.3 Removing width and row restrictions·inside lemSwapping binary address chunks in O(Vu^τ)

Statement (paper)

Let ee be the least integer with qe≥2uq^e\ge2^u. Padding each of the two chunk ranges numerically from [2u][2^u] to [qe][q^e], with zero in an entry if either chunk coordinate is invalid, increases the volume by a factor less than q2q^2 and costs O(V)O(V) steps; it preserves the order of the existing entries. After the interchange of the two padded chunks, scanning away the entries not having both chunk coordinates below 2u2^u recovers the desired binary array, and since e=O(u)e=O(u) the total time is O(Vuτ)O(Vu^\tau).

In plain English

Let ee be the least integer with qe≥2uq^e\ge2^u. Padding both chunk ranges from [2u][2^u] to [qe][q^e] with zeros costs O(V)O(V) steps and enlarges the volume by less than a factor q2q^2. After the swap, discarding the padded entries yields the desired binary array, for a total time of O(Vuτ)O(Vu^\tau).

Why it's here

This final step of the chunk-swap proof reduces the binary case [2u][2^u] to the radix-qq case, where the preceding claims already give a full chunk swap in time O(Veτ)O(Ve^\tau). Padding costs only a constant factor (<q2<q^2) in volume, and e=O(u)e=O(u) turns O(Veτ)O(Ve^\tau) into the claimed O(Vuτ)O(Vu^\tau) bound. Padding and unpadding preserve the order of existing entries, so removing the extra entries recovers exactly the permuted array.
Classified routine:
This is a standard padding/unpadding reduction from the binary range [2u][2^u] to the radix-qq range [qe][q^e]. It costs only a constant volume factor and plugs into the preceding radix-qq chunk-swap claims, with e=O(u)e=O(u) turning O(Veτ)O(Ve^\tau) into O(Vuτ)O(Vu^\tau).

Uses

claimBase-m pieces via power-width interchanges

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Binary chunks padded to radix-q ranges" rests on claim-lem-chunk-swap-2