Terminal readout and selective states

A spectator may be returned or consumed by terminal $\mathsf{Enter}$. The partial trace in eq:spectator-conclusion describes the accessible observation; it is not a term-level weakening rule.

Nonselective terminal readout of an entangled spectator preserves the original reduced state. Its conditional states need not be preserved. For

readout of the second factor leaves the first marginal $I/2$ when the outcome is ignored, but conditioning on the outcome gives $|0⟩⟨0|$ or $|1⟩⟨1|$.

Thus the theorem neither identifies the enlarged joint output with the original output nor permits a later geometric rule to read the spectator outcome without changing the comparison.