Entropy under entrywise modulus in dimension three

Abstract

Entrywise modulus increases trace-log entropy for positive semidefinite three-by-three matrices.

Theorem 1.1 (Spectral trace-log formula).

$$\forall n\in \mathrm{Type},[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall A\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\forall hA\in Matrix.IsHermitian\left(A\right),-(Complex.re\left(Matrix.trace\left(A\cdot CFC.log\left(A\right)\right)\right))=-(\sum _{i:n}(Matrix.IsHermitian.eigenvalues\left(hA,i\right)\cdot Real.log\left(Matrix.IsHermitian.eigenvalues\left(hA,i\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entropy_eq_spectrum (✓ std3). ∎

Source. Repository-derived.

Commentary.

Hermitian functional calculus expresses trace-log entropy as the sum over all real eigenvalues, with multiplicity.

Definition 1.2 (Entrywise complex modulus).

$$\forall G\in \mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{C}\right),\mathrm{entryModulus}\left(G\right)=Matrix.map\left(G,fun(z:\mathbb{C})\mapsto (\Vert z\Vert :\mathbb{C})\right)$$

Formalization. D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus (✓ std3).

Source. Repository-derived.

Commentary.

Matrix.map embeds the norm of every complex entry back into the complex numbers.

Theorem 1.3 (Diagonal entries are unchanged).

$$\forall G\in \mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{C}\right),\forall i\in \mathrm{Fin}\left(3\right),(Matrix.PosSemidef\left(G\right))\Rightarrow (\mathrm{entryModulus}\left(G\right)\left(i,i\right)=G\left(i,i\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_diag (✓ std3). ∎

Source. Repository-derived.

Commentary.

Positive semidefinite matrices have nonnegative real diagonal entries.

Theorem 1.4 (Trace is unchanged).

$$\forall G\in \mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{C}\right),(Matrix.PosSemidef\left(G\right))\Rightarrow (Matrix.trace\left(\mathrm{entryModulus}\left(G\right)\right)=Matrix.trace\left(G\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_trace (✓ std3). ∎

Source. Repository-derived.

Commentary.

The diagonal identity preserves the sum of diagonal entries.

Theorem 1.5 (Positivity in dimension three).

$$\forall G\in \mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{C}\right),(Matrix.PosSemidef\left(G\right))\Rightarrow (Matrix.PosSemidef\left(\mathrm{entryModulus}\left(G\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_posSemidef (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first two elementary spectral coefficients are fixed and the determinant increases. Their nonnegativity excludes a negative eigenvalue.

Theorem 1.6 (The modulus entropy inequality).

$$\forall G\in \mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{C}\right),(Matrix.PosSemidef\left(G\right))\Rightarrow (-(Complex.re\left(Matrix.trace\left(G\cdot CFC.log\left(G\right)\right)\right))\le -(Complex.re\left(Matrix.trace\left(\mathrm{entryModulus}\left(G\right)\cdot CFC.log\left(\mathrm{entryModulus}\left(G\right)\right)\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_entropy_mono (✓ std3). ∎

Source. Repository-derived.

Commentary.

For three nonnegative eigenvalues with fixed mass and second elementary symmetric function, entropy increases with their product. Shifted logarithmic sums have ordered derivatives and equal limits at infinity. Entrywise modulus preserves the first two spectral coefficients and increases the determinant. No trace normalization or invertibility is required.

References

• Truth anchor: D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entropy_eq_spectrum
• Truth anchor: D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus
• Truth anchor: D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_diag
• Truth anchor: D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_entropy_mono
• Truth anchor: D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_posSemidef
• Truth anchor: D5/S3/Quantum/Divergence/ThreeByThreeModulusEntropy.entryModulus_trace
• Dependency: D5/S3/Quantum/Matrix/CartesianVariance
• Dependency: D5/S3/Resource/LogDet/PathSpectralClassical