Proposition: State-specific telescope

Fix a complete referenced input. Let ${\rho }_j,{\tilde{\rho }}_j$ be the ideal and implemented states on the matching successive interfaces. If

and $d_{\mathrm{tr}}({\tilde{\rho }}_0,{\rho }_0)\le a_0$, then

This is a bound for the specified input, not a diamond-norm claim.

Proof. At each step insert $({\tilde{\Gamma }}_j\otimes {\mathrm{id}}_E)({\rho }_{j-1})$ between the implemented and ideal next states. Contractivity bounds the propagated preceding error; the displayed hypothesis bounds the new term. Induct.