Lemma: Readout, forgetting, and consumed names

On every operator, including operators with an untouched reference,

Every output source observable acts on declared surviving output names. An operator on the consumed factor $S$ is not a surviving source operator unless a new output representation is explicitly supplied.

Proof. Expand

Readout returns ${\sum }_z|z⟩⟨z{|}_R\otimes X_{zz}$. Tracing $R$ gives ${\sum }_z{X}_{zz}={\mathrm{Tr}}_{S}X$. An untouched reference can be included in $B$.

The codomain in A:eq:readout contains no $S$-factor. A pullback through ${\mathcal{M}}_S^{\ast }$ is an input observable used to calculate an output expectation, not a restored output factor. A representation of an $S$-observable on $RB$ would be additional interface data.