Environment Marginal Channel

Abstract

A finite controlled environment record reduces to its Gram entrywise channel.

Theorem 1.1 (Finite environment marginal is the record Gram channel).

$$\forall d\in Nat,e\in Nat,E\in \mathrm{Fin}\left(d\right)\to \left(\mathrm{Fin}\left(e\right)\to \mathbb{C}\right),rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{let}V:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right)\times \mathrm{Fin}\left(e\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall i:\mathrm{Fin}\left(d\right),a:\mathrm{Fin}\left(e\right),j:\mathrm{Fin}\left(d\right),\mathrm{entry}\left(V,\mathrm{pair}\left(i,a\right),j\right)=\mathrm{ite}\left(j=i,E\left(i\right)\left(a\right),0\right);\mathrm{let}T:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right)\times \mathrm{Fin}\left(e\right),\mathrm{Fin}\left(d\right)\times \mathrm{Fin}\left(e\right),\mathbb{C}\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall X:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right)\times \mathrm{Fin}\left(e\right),\mathrm{Fin}\left(d\right)\times \mathrm{Fin}\left(e\right),\mathbb{C}\right),i:\mathrm{Fin}\left(d\right),j:\mathrm{Fin}\left(d\right),\mathrm{entry}\left(T\left(X\right),i,j\right)=\sum _{a\in \mathrm{Fin}\left(e\right)}\mathrm{entry}\left(X,\mathrm{pair}\left(i,a\right),\mathrm{pair}\left(j,a\right)\right);\left(T\left(V\cdot \rho \cdot V^{\ast }\right)=\mathrm{recordChannel}\left(E,\rho \right)\wedge T\left(V\cdot \rho \cdot V^{\ast }\right)=\mathrm{hadamard}\left((i,j)\mapsto \mathrm{recordGram}\left(E,i,j\right),\rho \right)\right)\wedge \left(\forall i\in \mathrm{Fin}\left(d\right),j\in \mathrm{Fin}\left(d\right),\mathrm{entry}\left(T\left(V\cdot \rho \cdot V^{\ast }\right),i,j\right)=\mathrm{recordGram}\left(E,i,j\right)\cdot \mathrm{entry}\left(\rho ,i,j\right)\right)$$

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

Source. Repository-derived.

Commentary.

For finite system and environment coordinate sets, the displayed matrix V writes the environment amplitudes belonging to each system address. The displayed environment trace sums equal environment coordinates.

For every complex system matrix, tracing V rho V^* gives the canonical recordChannel and also the Hadamard product of rho with the canonical recordGram matrix. The final clause states the same calculation at each system-matrix entry.

References

• Truth anchor: D5/S3/Quantum/Decoherence/EnvironmentMarginalChannel.environment_marginal_channel
• Dependency: D5/S3/Quantum/FixedAlgebra/SingletonRecordClassicality