claimroutineinferred_dep

Recurrence solves to O(e^τ) per volume

Recurrence

F_k\le(s/W)F_{k-1}+O(1)

gives

O(e^\tau)

per volume

solves the swap cost recurrence

Claim·§4.2 Transferring a finite circuit to address permutations·inside propPower-width chunk interchange in O(Ve^τ)

Statement (paper)

Let

F_k

be a uniform upper bound for time divided by logical volume for the interchange of two chunks of

e=m^k

radix-

q

digits each, so that

F_0=O(1)

and

F_k\le(s/W)F_{k-1}+O(1)

. Since

s/W<m^\tau

, it follows that

F_k=O(m^{k\tau})=O(e^\tau)

, with the implied constant independent of

k

and of all field lengths.

In plain English

F_k

is the worst-case ratio of time to logical volume for interchanging two chunks of

e=m^k

radix-

q

digits, then

F_0=O(1)

and

F_k\le(s/W)F_{k-1}+O(1)

. Because

s/W<m^\tau

, this gives

F_k=O(m^{k\tau})=O(e^\tau)

with a constant independent of

k

and the field lengths.

Why it's here

The three-shear swap reduces one interchange at level

k

to circuit-driven shears whose recursive calls, after dividing by volume, contribute a factor

s/W

times the level-

(k-1)

cost plus linear overhead. Since

s/W<m^\tau

, the geometric recurrence grows at most like

m^{k\tau}

, which yields the

O(Ve^\tau)

time bound claimed in the proposition once the fixed-tape schedule cost per node is accounted for.

Classified routine:

Unrolling the linear recurrence

F_k\le(s/W)F_{k-1}+O(1)

with ratio

s/W<m^\tau

gives a geometric sum bounded by

O(m^{k\tau})

. This is a standard recurrence calculation that uses the shear decomposition from the previous claim.

Uses

claimThree shears interchange the two chunks

Used by

claimDepth-first fixed-tape schedule costs O(V)

Sources

PaperOpen

Section: §4.2 Transferring a finite circuit to address permutations
Page: —
Label: —
Line: sections/04-swap.tex:197

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Volume-normalized recurrence gives O(e^τ)" rests on claim-prop-power-interchange-3