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 (Finite diagonal functional calculus).

Lean statement: D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity.cfc_diagonal

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

Source. Repository-derived.

Commentary.

For every real function f and every finite real diagonal, actual complex matrix CFC applies f coordinatewise. The finite spectrum requires no global continuity assumption on f. The existing logarithm diagonal theorem consumes this extracted proof, and the Petz inverse-square-root coordinate argument also uses it. This is a shared organizing helper, not a separate mathematical gain.

Definition 1.2 (The diagonal star-algebra homomorphism).

$$\begin{gathered} \forall (n:\mathrm{Type})[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)],\mathrm{diagonalStarAlgHom}:\mathrm{StarAlgHom}\left(\mathbb{C},n\to \mathbb{C},\mathrm{Matrix}\left(n,n,\mathbb{C}\right)\right), \\ \mathrm{toAlgHom}\left(\mathrm{diagonalStarAlgHom}\right)=\mathrm{diagonalAlgHom}\left(\mathbb{C}\right)\wedge (\forall a:n\to \mathbb{C},\forall ij:n,\mathrm{diagonalStarAlgHom}\left(a,i,j\right)=\mathrm{ite}\left(i=j,a\left(i\right),0\right))\wedge \\ (\forall a:n\to \mathbb{C},\mathrm{diagonalStarAlgHom}\left(\mathrm{star}\left(a\right)\right)=\mathrm{star}\left(\mathrm{diagonalStarAlgHom}\left(a\right)\right)) \end{gathered}$$

Formalization. D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity.diagonalStarAlgHom (✓ std3).

Source. Repository-derived.

Commentary.

On a finite decidable carrier, diagonalStarAlgHom sends each complex coordinate function to its diagonal matrix. Its underlying algebra homomorphism is Matrix.diagonalAlgHom, and the star law is coordinatewise complex conjugation.

Theorem 1.3 (Entropy of the coordinate pinching).

$$\forall (n:\mathrm{Type})[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)],\forall \rho :\mathrm{DensityState}\left(n\right),\mathrm{vonNeumannEntropy}\left(\mathrm{basisPinchingState}\left(\rho \right)\right)=-(\sum _{i:n}\mathrm{Re}\left(\mathrm{densityMatrix}\left(\rho ,i,i\right)\right)\log \left(\mathrm{Re}\left(\mathrm{densityMatrix}\left(\rho ,i,i\right)\right)\right))$$

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

Source. Repository-derived.

Commentary.

The entropy of coordinate-basis pinching is the negative sum of each real diagonal entry times its real logarithm.

Theorem 1.4 (Entropy production equals deleted coherence).

$$\begin{array}{c}\forall (n:\mathrm{Type})[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)],\forall U:\mathrm{Matrix}\left(n,n,\mathbb{C}\right),\forall (hU:U\in \mathrm{unitaryGroup}\left(n,\mathbb{C}\right)),\forall \rho :\mathbb{N}\to \mathrm{DensityState}\left(n\right),\\ (\forall k:\mathbb{N},{\rho }_{k+1}=\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,hU,{\rho }_k\right)\right))\Rightarrow \\ (\forall k:\mathbb{N},(\mathrm{vonNeumannEntropy}\left({\rho }_{k+1}\right)-\mathrm{vonNeumannEntropy}\left({\rho }_k\right)=\mathrm{quantumRelativeEntropy}\left(\mathrm{unitaryConjugateState}\left(U,hU,{\rho }_k\right),\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,hU,{\rho }_k\right)\right)\right)\wedge 0\le \mathrm{quantumRelativeEntropy}\left(\mathrm{unitaryConjugateState}\left(U,hU,{\rho }_k\right),\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,hU,{\rho }_k\right)\right)\right)))\wedge \\ (\forall N:\mathbb{N},\mathrm{vonNeumannEntropy}\left({\rho }_N\right)-\mathrm{vonNeumannEntropy}\left({\rho }_0\right)=\sum _{k\in \mathrm{range}\left(N\right)}\mathrm{quantumRelativeEntropy}\left(\mathrm{unitaryConjugateState}\left(U,hU,{\rho }_k\right),\mathrm{basisPinchingState}\left(\mathrm{unitaryConjugateState}\left(U,hU,{\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.cfc_diagonal
• Truth anchor: D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity.diagonalStarAlgHom
• Truth anchor: D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity.entropy_production_coherence_deletion_identity
• Truth anchor: D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity.von_neumann_entropy_basisPinchingState
• Dependency: D5/S3/Divergence/GrandmotherTheorem
• Dependency: D5/S3/Quantum/Divergence/VonNeumannEntropyPinching
• Dependency: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow