Lemma: Record covariance

After designation of a root $s$, every later compiled gate commutes, as a conjugation channel, with pinching on $s$.

Proof. A gate touching $s$ can only use it as a computational control or a CNOT source, so it is block-diagonal in the basis of $s$. Every other gate acts away from $s$. In either case, conjugation commutes with the pinching.