Theorem: Conditional endpoint certificate

Suppose Definition def:four is satisfied. After the specified access-preserving identifications, let $\mathcal{V}$ and $\hat{\mathcal{V}}$ be actual and proxy complete channels with

Let $\hat{\mathcal{C}}$ be the proxy complete complement, and suppose a feasible state ${\tau }_E$ satisfies

Then

The recovery bound is realized by a fixed proxy decoder, unless the constant-decoder cap is smaller.

If a separately supplied proxy decoder has normalized decoded Choi discrepancy

the same decoder on the actual accessible output has error at most

Terminal residual Enter followed by drop changes none of these pre-existing accessible channels.

Proof. Partial traces contract the complete-channel comparison, giving accessible and complementary distances at most $b$. Lemma lem:choi gives

The triangle inequality proves (eq:endleak). Proposition prop:approx supplies a proxy decoder with error at most $\sqrt{2de}$. Applying that fixed decoder to the actual accessible channel adds at most $b$. The constant decoder gives the alternative cap $a_d$. The same Choi comparison and contraction prove the specified-decoder bound. The final assertion is Theorem thm:drop.