Proposition: Instrument-level observation criterion

The classical record laws of $\mathcal{F}$ and $\mathcal{G}$ agree for every input state if and only if

For a declared residual algebra $\mathcal{O}\subseteq L(K)$, the channels agree on all recorded residual observables ${\sum }_w|w⟩⟨w{|}_R\otimes B_w$, $B_w\in \mathcal{O}$, if and only if

Both are operator identities and therefore remain valid under an untouched reference extension.

Proof. The fine recorded probability of $w$ is

The coarse probability is $\mathrm{Tr}(\rho T^{\ast }(E_w))$. Equality for every state is equality of their Hermitian effects, proving A:eq:record-effects.

Pairing the $w$-block with $B$ gives the two pullbacks in A:eq:residual-effects. Equality against every state, first for self-adjoint $B$ and then by linearity, is equivalent to their operator equality. Tensoring these linear-map identities with a reference identity preserves them.