Theorem: Derived B4 transfer budget

In the global bounded-control model,

bounds the transfer trace distance, including all admitted spectators and references. For a support-only implementation, replace the last two terms by ${\zeta }_{\mathrm{low}}+2\sqrt{{q_h}^{K+1}}$.

Proof. First apply the same implemented extraction to the actual captured state and the ideal packet-in-memory state. Contractivity and Theorem thm:captureerror cost ${\xi }_{\mathrm{cap}}$. Replacing the independent register preparation costs $p_Q$. Now the input memory is the ideal packet, so Proposition prop:controlregimes supplies the appropriate control and tail terms. This ordering avoids making an unjustified geometric-tail claim about an imperfectly captured state.