propositionnovelunresolved_ref

Power-width chunk interchange in O(Ve^τ)

Swaps two mkm^k-digit chunks in O(Veτ)O(Ve^\tau) time, e=mke=m^k
power-width swap primitive for the general chunk swap
Proposition·prop:power-interchange·§4.2 Transferring a finite circuit to address permutations

Statement (paper)

Assume the fixed circuit data satisfy , and let qq be a prime as in Lemma  for its edge matrices, also avoiding the denominators of every assigned terminal and gate matrix MM. Choose a rational number τ∈(0,1)\tau\in(0,1) with s/W<mτs/W<m^\tau. For every e=mke=m^k, k≥0k\ge0, consider two disjoint contiguous address chunks of ee radix-qq digits each. Suppose a row field preceding both chunks has length divisible by WkW^k. There may be additional fields before and after the row field, between the chunks, and after them. The chunks can be interchanged in O(Veτ)O(Ve^\tau) time, preserving every other address field, on a fixed number of finite-alphabet tapes. The constant is independent of all field lengths and of the data.

In plain English

Given a fixed circuit satisfying the finite-shear contract and a suitable prime qq, two disjoint address chunks of e=mke=m^k radix-qq digits each can be swapped in O(Veτ)O(Ve^\tau) time on a fixed number of finite-alphabet tapes, where s/W<mτs/W<m^\tau and a row field before both chunks has length divisible by WkW^k. All other address fields are preserved and the constant does not depend on field lengths or data.

Why it's here

The proof splits rows into WW role streams, runs the circuit with edge shears from the matrix-shear lemma to get H←H+DH\leftarrow H+D, and chains three shears to swap the chunks. This gives the recurrence Fk≤(s/W)Fk−1+O(1)F_k\le (s/W)F_{k-1}+O(1), which solves to O(eτ)O(e^\tau) per unit volume. It is the power-width interchange primitive that the arbitrary-width chunk swap assembles into general interchanges and that the final cost table relies on.
Classified novel:
This is the paper's new recursive primitive for interchanging address chunks on a multitape Turing machine. It runs a fixed finite circuit through matrix shears, giving a recurrence that yields cost O(Ve^τ), sublinear in chunk length; standard transposition methods on Turing machines cost a full log factor and give nothing like this.

Uses

lemElementary digit scans run in linear timelemMatrix shear via few interchanges

Used by

lemSwapping binary address chunks in O(Vu^τ)claimBase-m pieces via power-width interchangesclaimCost table yields the final time bound

Inside the proof

claimSplit rows cyclically into role streamsclaimCircuit on role streams realizes shearclaimThree shears interchange the two chunksclaimRecurrence solves to O(e^τ) per volumeclaimDepth-first fixed-tape schedule costs O(V)claimDescriptor processing fits within child volume

Sources

PaperOpen
Section
§4.2 Transferring a finite circuit to address permutations
Page
—
Label
prop:power-interchange
Line
sections/04-swap.tex:129
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    Key step uses the common-frame identity eq:common-frame-identity from §3.2, which is not a labeled statement.