Subadditivity of quantum states over time

Abstract

The Werner–Holevo channel on the maximally mixed five-level state gives a two-time pseudo-density matrix whose signed entropy exceeds the sum of its marginal entropies.

Definition 1.1 (Input-first Jamiołkowski matrix).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall E\in \mathrm{LinearMap}\left(\mathbb{C},\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{C}\right)\right),\mathrm{jamio}\left(E\right)=\sum _{i:\mathrm{Fin}\left(n\right)}(\sum _{j:\mathrm{Fin}\left(n\right)}(\mathrm{kronecker}\left(\mathrm{single}\left(i,j,1\right),E\left(\mathrm{single}\left(j,i,1\right)\right)\right)))$$

Formalization. D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.jamio (✓ std3).

Citation. James Fullwood and Arthur J. Parzygnat (2025). On Dynamical Measures of Quantum Information. DOI: 10.3390/e27040331. URL: https://doi.org/10.3390/e27040331.

Commentary.

The input factor precedes the output factor. The matrix unit inside the channel has its indices reversed: this is the Jamiołkowski convention of Fullwood and Parzygnat, rather than the Choi convention. The carrier is Fin n times Fin m, matching the factor order in rho tensor the output identity.

Definition 1.2 (Two-time pseudo-density matrix).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\forall E\in \mathrm{LinearMap}\left(\mathbb{C},\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{C}\right)\right),\mathrm{pdm}\left(rho,E\right)=\mathrm{smul}\left(\frac{1}{2},\mathrm{kronecker}\left(rho,(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{C}\right))\right)\cdot \mathrm{jamio}\left(E\right)+\mathrm{jamio}\left(E\right)\cdot \mathrm{kronecker}\left(rho,(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{C}\right))\right)\right)$$

Formalization. D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.pdm (✓ std3).

Citation. James Fullwood and Arthur J. Parzygnat (2025). On Dynamical Measures of Quantum Information. DOI: 10.3390/e27040331. URL: https://doi.org/10.3390/e27040331.

Commentary.

Equation (15) defines a quantum state over time by half the anticommutator of rho tensor the output identity with the Jamiołkowski matrix. The channel is a complex-linear map between full matrix algebras.

Definition 1.3 (Fullwood–Parzygnat subadditivity conjecture).

$$claim\iff (\forall n\in \mathbb{N},\forall m\in \mathbb{N},(1\le n)\Rightarrow ((1\le m)\Rightarrow (\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),(\mathrm{PosSemidef}\left(rho\right))\Rightarrow ((\mathrm{trace}\left(rho\right)=1)\Rightarrow (\forall iota\in \mathrm{Type},[\mathrm{Fintype}\left(iota\right)]\forall K\in iota\to \mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),(\sum _{k:iota}(\mathrm{conjTranspose}\left(K\left(k\right)\right)\cdot K\left(k\right))=1)\Rightarrow (\mathrm{entropy}\left(\mathrm{pdm}\left(rho,\mathrm{ofKraus}\left(K,K\right)\right)\right)\le \mathrm{entropy}\left(rho\right)+\mathrm{entropy}\left(\mathrm{ofKraus}\left(K,K\right)\left(rho\right)\right)))))))$$

Formalization. D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.claim (✓ std3).

Citation. James Fullwood and Arthur J. Parzygnat (2025). On Dynamical Measures of Quantum Information. DOI: 10.3390/e27040331. URL: https://doi.org/10.3390/e27040331.

Commentary.

Remark 1 of On Dynamical Measures of Quantum Information conjectures subadditivity on quantum states over time. Both dimensions are positive. The input is positive semidefinite with trace one, and the arbitrary finite Kraus family satisfies the completeness equation. ofKraus(K,K) is FiniteKrausChannel.PhyslibLeaf.MatrixMap.of_kraus, whose action is the sum of K_k X K_k adjoint. Thus the hypothesis gives a completely positive trace-preserving map. The bound uses ChenKatoBrandaoCMIRefutation.entropy: on Hermitian matrices it is PartialTraceMutualInformation.spectralEntropy, the sum of -lambda log |lambda| over the eigenvalues with multiplicity, including zero contributions at zero; its value on other matrices is zero. The bound compares this signed entropy of the two-time matrix with the entropies of the input and output states. Fullwood and Yang, arXiv:2608.28946v1, Section 6, also state the higher-dimensional question as open.

Theorem 1.4 (Functional calculus of an affine projection).

$$\forall n\in \mathrm{Type},[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall Q\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),(\mathrm{IsHermitian}\left(Q\right))\Rightarrow ((Q\cdot Q=Q)\Rightarrow (\forall f\in \mathbb{R}\to \mathbb{R},\forall a\in \mathbb{R},\forall b\in \mathbb{R},\mathrm{cfc}\left(f,\mathrm{smul}\left(a,(1:\mathrm{Matrix}\left(n,n,\mathbb{C}\right))\right)+\mathrm{smul}\left(b,Q\right)\right)=\mathrm{smul}\left(f\left(a\right),(1:\mathrm{Matrix}\left(n,n,\mathbb{C}\right))\right)+\mathrm{smul}\left(f\left(a+b\right)-f\left(a\right),Q\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.projection_cfc (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a Hermitian idempotent Q, the continuous functional calculus of a I + b Q is determined by f(a) on the complementary range and f(a+b) on the range of Q.

Theorem 1.5 (A five-level Werner–Holevo counterexample).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.result (✓ std3). ∎

Resolves. Problems/fullwood-parzygnat-2025-states-over-time-subadditivity (refuted) by D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.result.

Source. Repository-derived.

Acknowledgement. James Fullwood and Arthur J. Parzygnat (2025). On Dynamical Measures of Quantum Information. DOI: 10.3390/e27040331. URL: https://doi.org/10.3390/e27040331.

Commentary.

Let rho be the identity divided by five and use the ten Kraus operators (E_ij - E_ji)/2, one for each i < j. Their adjoint products sum to the identity. Their channel action is (trace(X) I - transpose(X))/4 and fixes rho. Use ProductUnitaryChoiSpectrum.omega 5, whose entries are one exactly on equal input and output indices, and let P be its outer product divided by five. ProductUnitaryChoiSpectrum.omega_dot_omega gives squared norm five; complex conjugation fixes this vector. P is a Hermitian idempotent of trace one. The Jamiołkowski matrix is (I - 5P)/4, and the two-time matrix is (I - 5P)/20. Its eigenvalues are -1/5 once and 1/20 twenty-four times. Apply CumulantRenyiDataProcessingRefutation.two_point_cfc to the self-adjoint involution H = 2P - I with a = -3/40 and b = -1/8. This evaluates the signed entropy ChenKatoBrandaoCMIRefutation.entropy through PathSpectralClassical.trace_cfc_eq_sum and gives log 5 + (6/5) log 4. Each marginal entropy is log 5. The excess is (1/5) log(4096/3125), which is strictly positive because 4096 > 3125. This contradicts the universal subadditivity bound.

References

• Truth anchor: D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.claim
• Truth anchor: D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.jamio
• Truth anchor: D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.pdm
• Truth anchor: D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.projection_cfc
• Truth anchor: D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.result
• Dependency: D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation
• Dependency: D5/S3/Quantum/QuantumChannels/ProductUnitaryChoiSpectrum
• Dependency: D5/S3/QuantumChannels/CumulantRenyiDataProcessingRefutation
• Dependency: D5/S3/Resource/LogDet/PathSpectralClassical