Nonselective Marginalization

Abstract

The canonical finite recording map has a non-selective marginal equal to the sum of diagonal projective blocks.

Theorem 1.1 (Tracing out the recording register gives the unread update).

$$\forall S,A:\mathrm{Type},\mathrm{Fintype}\left(S\right)\wedge \mathrm{DecidableEq}\left(S\right)\wedge \mathrm{Fintype}\left(A\right)\wedge \mathrm{DecidableEq}\left(A\right)\wedge P:A\to \mathrm{Matrix}\left(S,S,\mathbb{C}\right),\forall a\in A,\mathrm{adjoint}(P(a))=P(a)\wedge \forall a\in A,b\in A,P(a)\cdot P(b)=\mathrm{ite}\left(a=b,P(a),0\right)\wedge \sum _{a\in A}P(a)=I\Rightarrow \mathrm{let}V:\mathrm{Matrix}\left(S\times A,S,\mathbb{C}\right),\forall i,a,j:S,\mathrm{entry}\left(V,\mathrm{pair}\left(i,a\right),j\right)=\mathrm{entry}\left(P(a),i,j\right);\mathrm{let}Tr:\mathrm{Matrix}\left(S\times A,S\times A,\mathbb{C}\right)\to \mathrm{Matrix}\left(S,S,\mathbb{C}\right),\forall X,i,j:S,\mathrm{entry}\left(Tr(X),i,j\right)=\sum _{a\in A}\mathrm{entry}\left(X,\mathrm{pair}\left(i,a\right),\mathrm{pair}\left(j,a\right)\right);Tr(Vrho{V}^{\ast })=\sum _{a\in A}P(a)(rho)(P(a)).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/NonselectiveMarginalization.nonselective_recording_marginal (✓ std3). ∎

Source. Repository-derived.

Commentary.

The system and outcome carriers are finite with decidable equality. Self-adjoint orthogonal projectors summing to the identity define the canonical recording matrix V((i,a),j) = P(a)(i,j).

The displayed partial-trace map sums equal outcome indices in each system matrix entry. Applied to V rho V^*, it therefore returns exactly the sum of the diagonal blocks P(a) rho P(a), for every complex system matrix rho.

The proof applies the frozen recording-isometry state-block theorem directly; no alternate recording or partial-trace primitive is introduced.

References

• Truth anchor: D5/S3/Quantum/Decoherence/NonselectiveMarginalization.nonselective_recording_marginal
• Dependency: D5/S3/Quantum/Decoherence/RecordingIsometry