Entropy Production by Coherence Deletion

Abstract

Unitary evolution followed by coordinate-basis pinching produces entropy equal to the deleted coherence, with nonnegative gains that telescope.

Theorem 1.1 (Entropy production equals deleted coherence).

$$\begin{array}{c}\forall n:\mathrm{Type},U:\mathrm{Matrix}\left(n,n,\mathbb{C}\right),\rho :\mathbb{N}\mapsto \mathrm{DensityState}\left(n\right),\\ \mathrm{Fintype}\left(n\right)\wedge \mathrm{DecidableEq}\left(n\right)\wedge U\in \mathrm{unitaryGroup}\left(n,\mathbb{C}\right)\wedge \\ \forall k\in \mathbb{N},{\rho }_{k+1}=\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,{\rho }_k\right)\right)\Rightarrow \\ (\forall k\in \mathbb{N},(\mathrm{vonNeumannEntropy}\left({\rho }_{k+1}\right)-\mathrm{vonNeumannEntropy}\left({\rho }_k\right)=\mathrm{quantumRelativeEntropy}\left(\mathrm{unitaryConjugateState}\left(U,{\rho }_k\right),\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,{\rho }_k\right)\right)\right)\wedge 0\le \mathrm{quantumRelativeEntropy}\left(\mathrm{unitaryConjugateState}\left(U,{\rho }_k\right),\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,{\rho }_k\right)\right)\right)))\wedge \\ (\forall N\in \mathbb{N},\mathrm{vonNeumannEntropy}\left({\rho }_N\right)-\mathrm{vonNeumannEntropy}\left({\rho }_0\right)=\sum _{k<N}\mathrm{quantumRelativeEntropy}\left(\mathrm{unitaryConjugateState}\left(U,{\rho }_k\right),\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,{\rho }_k\right)\right)\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let U be a unitary complex matrix on a finite decidable carrier. Starting from a sequence of density states, assume each next state is obtained by conjugating with U and then deleting the off-diagonal entries in the fixed coordinate basis.

At every step, the entropy gain is exactly the quantum relative entropy from the evolved state to its pinched state, and this quantity is nonnegative. Summing these one-step identities gives the finite-horizon entropy balance.

References

• Truth anchor: D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity.entropy_production_coherence_deletion_identity
• Dependency: D5/S3/Divergence/GrandmotherTheorem
• Dependency: D5/S3/Quantum/Divergence/VonNeumannEntropyPinching
• Dependency: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow