Finite Kraus Instrument Born Marginal

Abstract

Finite normalized Kraus instruments have the expected one-step Born marginal.

Theorem 1.1 (A finite Kraus branch has the Born weight of its effect).

$$\begin{gathered} \forall n,X,A,R:\mathrm{Type}, \\ \mathrm{Fintype}(n),\mathrm{Nonempty}(n),\mathrm{DecidableEq}(n), \\ \mathrm{Fintype}(A),\mathrm{Fintype}(R), \\ K:\{K:X\to A\to R\to \mathrm{Matrix}(n,n,\mathbb{C})\mid \forall x\in X,\sum _{a\in A}\sum _{r\in R}\mathrm{star}(K(x,a,r))\cdot K(x,a,r)=\mathrm{identityMatrix}(n)\}, \\ \rho :\mathrm{DensityState}(n), \\ \forall x:X,a:A, \\ \mathrm{let}S:\mathrm{Matrix}(n,n,\mathbb{C})=\mathrm{matrix}(\rho ), \\ B:\mathrm{Matrix}(n,n,\mathbb{C})=\sum _{r\in R}K(x,a,r)\cdot S\cdot \mathrm{star}(K(x,a,r)), \\ E:\mathrm{Matrix}(n,n,\mathbb{C})=\sum _{r\in R}\mathrm{star}(K(x,a,r))\cdot K(x,a,r); \\ \mathrm{Tr}(B)=\mathrm{bornProbability}(S,E). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FiniteKrausInstrumentBornMarginal.finite_kraus_instrument_born_marginal (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public Kraus family is normalized at every setting, so its outcome branches form a finite-dimensional instrument. The input uses the canonical positive trace-one density-state carrier.

Each branch and effect is constructed by a finite Kraus sum. Trace linearity and cyclicity move the outer Kraus operator across the trace, yielding the canonical Born trace pairing.

References

• Truth anchor: D5/S3/Quantum/Measurement/FiniteKrausInstrumentBornMarginal.finite_kraus_instrument_born_marginal
• Dependency: D5/S3/Quantum/Divergence/QuantumRelativeEntropyDefectComposition
• Dependency: D5/S3/Quantum/Measurement/StaticEffectSequentialSeparation