claimroutineinferred_dep

Descriptor processing fits within child volume

Descriptor handling at each child is absorbed in

O(V_j)

shows descriptor cost adds nothing to the recurrence

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

Statement (paper)

Even when the payload is one bit, descriptor processing at a child of depth

j\le k_0=\log_m e_0

in a power-width call of width

e_0=m^{k_0}

and root volume

V_0

takes

(\log(2V_0))^{O(1)}=O(V_j)

time, where

V_j=V_0/W^j

is the volume of that child; in particular, it fits within the additional

O(V)

term at each node. This is because

V_j\ge q^{2e_0}

and

j\log W\le(\log_m e_0)\log W=O(e_0)=O(\log V_j)

, so that

\log V_0=\log V_j+j\log W=O(\log(2V_j))

In plain English

Even with a one-bit payload, processing the descriptor at a child of depth

j\le k_0=\log_m e_0

in a power-width call of width

e_0=m^{k_0}

and root volume

V_0

takes

(\log(2V_0))^{O(1)}=O(V_j)

time, where

V_j=V_0/W^j

is that child's volume. So it is absorbed by the additional

O(V)

term at each node.

Why it's here

This shows the descriptor handling left over from the depth-first schedule adds no new cost to the swap recurrence. The reason is that

V_j\ge q^{2e_0}

and

j\log W=O(e_0)=O(\log V_j)

, so

\log V_0=\log V_j+j\log W=O(\log(2V_j))

, and a polylogarithm in

V_0

is therefore bounded by

O(V_j)

Classified routine:

A direct bookkeeping calculation inside the proof. It bounds

\log V_0

O(\log V_j)

using

V_j\ge q^{2e_0}

and

j\log W=O(e_0)

, so the polylogarithmic descriptor cost is absorbed into the

O(V)

per-node term of the depth-first schedule (the previous claim).

Uses

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

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Descriptor processing absorbed by child volume" rests on claim-prop-power-interchange-5