Theorem: Implemented recovery and complete residual

Under the declared comparisons,

For the complete predecoder residual,

A separate accessible collection allowance adds $e_{\mathrm{collection}}$ to recovery. It bounds a chosen complete postcollection residual only when an appropriate complete collection comparison is also supplied.

For the semicircle model, a sufficient analytical bound is

Proof. First replace actual preparation by ideal preparation while using the same actual full propagator. Contractivity costs at most $e_{\mathrm{prep}}$. The remaining comparison starts in the checked ideal sector and costs at most ${\Delta }_T$ by Theorem thm:C6. Thus the complete emitted channels differ by at most $e_{\mathrm{prep}}+{\Delta }_T$.

Partial trace gives the same accessible allowance. Replacing the decoder adds at most $e_{\mathrm{decoder}}$. Add the exact ideal recovery error of Theorem thm:C4.

For the residual, take the other partial trace and compare with (eq:residualtau). All preparation outputs are retained, so this is a complete comparison, not an accessible-only preparation estimate.

A separate collector adds its channel allowance by contractivity. Such a distance does not compare a preselected environmental dilation; that requires its own complete comparison KSW.

Finally use Theorem thm:C5 and Lemma lem:packetbound.