Observer Pullback Trace Identity

Abstract

Iterated channel evolution and Heisenberg pullback have equal trace readouts.

Theorem 1.1 (Channel iterates equal iterated effect pullbacks).

$$\begin{array}{c}\forall d:\mathrm{Type},\mathrm{Fintype}(d),\mathrm{DecidableEq}(d),\\ \varphi :\mathrm{QuantumChannel}(d,d),{\varphi }^{\ast }:\mathrm{CompletelyPositiveMap}(\mathrm{Matrix}(d,d,\mathbb{C}),\mathrm{Matrix}(d,d,\mathbb{C})),\\ (\forall X,A:\mathrm{Matrix}(d,d,\mathbb{C}),\mathrm{Tr}(\varphi (X)A)=\mathrm{Tr}(X{\varphi }^{\ast }(A))),\\ t:\mathrm{Nat},\rho :\mathrm{DensityState}(d),E:\mathrm{Matrix}(d,d,\mathbb{C}),\\ \mathrm{Tr}((\varphi {)}^t(\rho )E)=\mathrm{Tr}(\rho ({\varphi }^{\ast }{)}^t(E)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/ObserverPullbackTraceIdentity.observer_pullback_trace_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite carrier is the existing complex matrix algebra. The Schrodinger map is an existing completely positive trace-preserving quantum channel, and rho is an existing positive trace-one density state.

The Heisenberg map is completely positive and is related to the channel by the displayed one-step trace-duality premise. The effect may be any matrix, so physical effects are included without an extra restriction.

Induction moves one channel use across the trace pairing at each step. The two canonical iterate recursion laws identify the resulting expression with the same number of Heisenberg pullbacks.

References

• Truth anchor: D5/S3/Quantum/Dynamics/ObserverPullbackTraceIdentity.observer_pullback_trace_identity
• Dependency: D5/S3/Quantum/Fibers/FutureStatisticsEquivalence