Theorem: Exact state–instrument pairing

For every logical input state $\rho$,

More generally, for every observable $B$ on the retained quantum and setting outputs,

The same identities hold at every sufficiently fine scale under the instrument and observable comparison maps.

The effects $M_{ab}$ are products of commuting represented local pointer projections in the two measurement algebras.

Proof. Proposition prop:dilation identifies the operational channel with the partial trace of $U{\sigma }_{\rho }{U}^{†}$. The defining property of partial trace and cyclicity of trace give (eq:pairing) and (eq:selectivepairing).

Each single-wing pointer projection pulls back into its wing algebra. These two algebras commute by Theorem thm:microcausality. Their product is (eq:reporteffects).

At scale $n$, insert the physical blank state in the remaining factors. Lemma lem:obscomparison gives

The exact channel identity (eq:exactBelllimit) and exact observable comparison (eq:exactobservablelimit) then reproduce the same pairings.