Theorem: Exact complete transport

For every state ${\rho }_{A_{0}E}$, after tick $j$ the state is, under the fixed register identifications,

At the destination:

1. the logical channel is exactly ${\mathrm{id}}_{2^p}$, including every untouched reference;

2. all non-output route registers are jointly blank and payload independent;

3. arrival is at $e_B$;

4. every scheduled dependency is metric causal;

5. the protocol uses $m$ register SWAPs, $m$ ticks, and $m+1$ payload-sized registers.

Proof. The assertion at $j=0$ is the preparation. At tick $j$, $A_j$ is blank and independent; SWAP exchanges it with the entire $A_{j-1}$ tensor factor, including its correlations with $E$. The previous site becomes blank. This proves the invariant by induction.

The total time is $m\Delta T=L_{AB}/c$. Each active pair has separation $a=c\Delta T$, so Lemma lem:local-causal certifies all its endpoint dependencies. The counts follow from the printed schedule.