Proposition: Named-interface error composition

Suppose an implemented channel and decoder satisfy the declared comparisons

in half-diamond distance at their respective interfaces. Then a finite direct decoder certificate gives

capped at one. A decoder supplied by the residual theorem instead replaces $d\hat{r}(t)+b_{\mathrm{reg}}$ by the bound in (eq:recovery-certificate).

Proof. Insert the intermediate channels one at a time. Use the triangle inequality and contraction of diamond distance under CPTP pre- and postprocessing.