Theorem: Certified quantum return

Suppose a finite complete proxy has comparison allowance

on the common, access-preserving output space. For a specified finite residual state $\hat{\sigma }$, set

Then

There exists a finite proxy decoder whose full CPTP extension satisfies

If a specified finite CPTP decoder has

then its full extension satisfies

Any prescribed observation after quantum return has the same upper allowance relative to its observation target.

Proof. Partial trace of the complete comparison gives allowance $b$ for each reduced channel. Lemma lem:bounds bounds the proxy leakage by $de$. Embed $\hat{\sigma }$ into the complete residual space and use the triangle inequality to obtain (eq:leakcertificate).

Equation (eq:KSW) supplies a finite decoder with error at most $\sqrt{2de}$. Let $P_R$ project onto its finite accessible ambient subspace. Extend it to the full accessible space by

The extension is CPTP and agrees on proxy outputs. Decoder contraction adds $b$, outside the square root, giving (eq:existcertificate).

For the specified decoder, (eq:choibound) gives the proxy allowance $d{r}_{\mathrm{dec}}$; the same extension adds $b$. Proposition prop:records proves the terminal-record statement.