Theorem: Operational departure certificate

Suppose the two participating preparations have complete record errors $e_{\theta },e_0$ for the same declared test. Then

The right-hand side may be replaced by its positive part.

More generally, if an independently specified bounded field effect $E$ is compared with the compressed register effect

and that finite effect is implemented with the same type of certificate, then

Here $J$ is the finite low-number encoding. The second assertion does not claim that every $F_E$ is a single setting of the constructed product-basis family.

Proof. An effect expectation changes by at most the record trace distance. Apply this once for each preparation and use the reverse triangle inequality. The ideal probabilities equal the expectations of $E_{\mathbf{a}}$, proving (eq:discrimination).

For the second assertion, the embedded carrier is within $t(p_{\mathbf{a}})$ of the original state by Lemma lem:coherenttail. Its expectation of $E$ equals the register expectation of $F_E$, since the ideal carrier is supported in the low-number box. Add both coherent errors before the record comparisons.