Corollary: Complete equality on the declared interface

The ideal circuit implements ${\Psi }_{G,t}$ exactly, including every untouched reference. Its half-diamond error against that target is zero.

Proof. Conditioned on the timers the controller is independent of $\rho$ and applies the stated unitary with the stated record. Averaging gives the displayed linear channel. Tensoring with a reference identity preserves the equality.