Corollary: Conditional operational approximation

Fix a datum and a representation supplied under Theorem thm:assembly. Suppose a compatible realization of Specification spec:transport supplies, for every $\zeta \in {\mathcal{T}}_D$ and $n$:

1. a finite complete protocol ${\Gamma }_{n,\zeta }:L(M)\to L(M\otimes F_{n,\zeta })$ and target (eq:full-target);

2. matched ideal and implemented factorizations with at most $H_n$ comparison steps, encoder and decoder allowances ${\alpha }_n,{\beta }_n$, complete step allowances at most ${ϵ}_n$, and

   $$d_{\diamond }({\overline{\Gamma }}_{n,\zeta },{\Theta }_{n,\zeta })\le {\mu }_n;$$

3. uniform endpoint estimates

   $$\Vert a_{n,\zeta }-T_D{\iota }_D(p){\Vert }_{\ast }+\Vert x_{n,\zeta }-x{\Vert }_2\le {\delta }_n,|{\tau }_{n,\zeta }-\tau |\le {\omega }_n;$$

4. the actual ledgers and proved bounds (eq:resource-bound);

5. a retained arrival register with calibrated absolute reading $z\mapsto {a^{\mathrm{arr}}}_{n,\zeta }(z)$. Its ideal marginal is supported on nonfailure codes obeying

   $$|{a^{\mathrm{arr}}}_{n,\zeta }(z)-t_{\zeta }|\le w_n.$$

All allowances are nonnegative. Uniformity is over the declared target set for this datum, not automatically over every admissible datum.

Set

Then

For every message-reference input, the complete actual output is within trace distance $e_n$ of the ideal referenced output. The same allowance bounds the logical referenced transport error and the residual reduction's distance from the input-independent ideal residual.

For every input, the probability of a failure code or an arrival reading outside the window in (P5) is at most $e_n$. The supplied protocol resource bounds remain ${\mathbf{r}}_{n,\zeta }\le {\mathbf{B}}_n(D)$.

If

the full and logical anchored endpoint errors converge uniformly to zero. If additionally $w_n\to 0$, the arrival readings concentrate in shrinking target windows with failure probability tending to zero.

These are endpoint conclusions. They assert neither exact finite-scale null attainment nor a global evolution at all intermediate times.

Proof. Lemma lem:telescoping bounds the implementation difference from the ideal factorization. The design allowance ${\mu }_n$ and the triangle inequality give (eq:channel-certificate).

Tensoring with an untouched reference and evaluating on a state gives the complete trace-distance bound. Partial traces are channels, so they give the logical and residual reduction bounds. In particular,

Insert the endpoint estimates into (eq:full-error)–(eq:logical-error) to prove (eq:endpoint-certificate).

The bad-code projector is an effect on the complete output. Its ideal probability is zero. Its actual probability differs from zero by at most the trace-distance allowance $e_n$. This proves the arrival statement.

Resource bounds are the supplied execution estimates, not a consequence of telescoping. The convergence assertions follow from the displayed inequalities.