Theorem: Resource-accounted transport certificate

Suppose a frozen circuit has independently certified logical error $s$ against $\mathcal{U}$, and a realization satisfies Specification spec:transport. Let $b_{\mathrm{impl}}$ be the sum of all implementation allowances in (eq:totalbudget), excluding $s$. Its decoded logical channel $\Lambda$ obeys

If source-position, spatial-displacement, and elapsed-time errors are bounded by ${\delta }_a,{\delta }_x,w$, respectively, then for any declared comparison scales $\ell >0,{\tau }_0>0$,

A zero-probability ideal failure or out-of-window event has actual probability at most the error allowance only when that event belongs to the compared complete output channel.

Proof. Lemma lem:telescoping and the independent synthesis comparison give the first bound. The second is substitution of the declared geometric estimates. The event bound follows from trace-distance contractivity under measurement on the complete compared output.