claimroutineinferred_dep

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

Depth-first recursion on fixed tapes costs

O(V)

bookkeeping per node

justifies the additive

O(V)

in the recurrence

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

Statement (paper)

With

W

role tapes, a fixed set of I/O and elementary-operation work tapes, one parking stack tape and a separate descriptor stack, the recursive calls at a node of logical volume

V

can be scheduled depth-first on these fixed tapes, the same tapes being used at every depth. The pushes, pops, copies, positioning operations and erasures around the fixed number

s

of child calls cost

O(V)

in total at that node, with cleanup confined to the region visited by the current call. This gives the additional

O(V)

term in , the factor

s/W

still being taken with respect to logical volume.

In plain English

The recursive child calls at a node of logical volume

V

can be run depth-first on a fixed set of tapes (W role tapes, I/O and work tapes, a parking stack and a descriptor stack), reused at every depth. The pushes, pops, copies, positioning and erasures around the

s

child calls cost

O(V)

in total at that node, with cleanup confined to the region the current call visits.

Why it's here

This supplies the additive

O(V)

overhead in the swap recurrence, so the recurrence

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

solved in the previous claim accounts for all tape bookkeeping. Because the same fixed tapes serve every depth and cleanup stays local, the recursion never needs a growing number of tapes, and the factor

s/W

remains measured in logical volume.

Classified routine:

Standard Turing-machine bookkeeping: a depth-first recursion on a fixed set of tapes with a stack, where each node pays linear overhead for its pushes, pops and cleanup. This is the usual technique for running recursive algorithms on multitape machines and adds nothing conceptually new.

Uses

claimRecurrence solves to O(e^τ) per volume

Used by

claimDescriptor processing fits within child volume

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Depth-first fixed-tape schedule costs O(V) per node" rests on claim-prop-power-interchange-4