Proposition: Readout, recording, and discard

Define the coherent recording isometry

Then

and

Both identities hold with an arbitrary untouched reference.

Proof. Expand ${\rho }_{ST}={\sum }_{x,y}|x⟩⟨y{|}_S\otimes {\rho }_{xy}$. Tracing the recorded $S$ factor kills the terms with $x\ne y$ and leaves ${\sum }_x|x⟩⟨x{|}_K\otimes {\rho }_{xx}$, which is (eq:enter). Tracing $K$ gives ${\sum }_x{\rho }_{xx}$, the partial trace of the original state. Tensoring the calculation with a reference identity changes neither equality.