The full dual account

Abstract

Two mutually unbiased measurements connect the full coherence tax to entropy freedom.

The dimension d is a positive natural number. Density states are positive semidefinite complex matrices with trace one. Z and X are complete rank-one projective contexts; their projectors form record measurements. MutuallyUnbiased means ReTr(Z_j X_k) = 1/d for every pair of outcomes. unreadState denotes the sum of P_j rho P_j over a context. The zero-Hamiltonian Gibbs state omega is I/d. All logarithms are natural. Freedom means relative entropy to omega; the tax of a measurement is relative entropy from its input to its actual output.

Theorem 1.1 (A Z-fixed state pays its full freedom in X).

$$\forall d\in PositiveNatural,Z\in \mathrm{RankOneContext}\left(d\right),X\in \mathrm{RankOneContext}\left(d\right),rho\in \mathrm{DensityState}\left(d\right),sigma\in \mathrm{DensityState}\left(d\right),\left(\mathrm{IsRecordMeasurement}\left(Z\right)\wedge \left(\mathrm{IsRecordMeasurement}\left(X\right)\wedge \left(\mathrm{MutuallyUnbiased}\left(Z,X\right)\wedge \left(\mathrm{unreadState}\left(Z,rho\right)=rho\wedge \mathrm{unreadState}\left(X,rho\right)=sigma\right)\right)\right)\right)\Rightarrow \left(sigma=\mathrm{gibbsState}\left(0\right)\wedge \left(\mathrm{quantumRelativeEntropy}\left(rho,sigma\right)=\mathrm{quantumRelativeEntropy}\left(rho,\mathrm{gibbsState}\left(0\right)\right)\wedge \left(\mathrm{quantumRelativeEntropy}\left(rho,sigma\right)=\log \left(d\right)-\mathrm{vonNeumannEntropy}\left(rho\right)\wedge \left(\mathrm{vonNeumannEntropy}\left(sigma\right)-\mathrm{vonNeumannEntropy}\left(rho\right)=\mathrm{quantumRelativeEntropy}\left(rho,sigma\right)\wedge \left(\mathrm{unreadState}\left(X,rho\right)=rho\iff rho=\mathrm{gibbsState}\left(0\right)\right)\right)\right)\right)\right)$$

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

Citation. John Watrous (2018). The Theory of Quantum Information — spectral calculus, reductions and entropy. URL: https://cs.uwaterloo.ca/~watrous/TQI/TQI.pdf.

Commentary.

Mutual unbiasedness makes the composition of the two measurements completely depolarizing. Since Z already fixes rho, the actual X output sigma must be omega. The Gibbs entropy identity then makes the X tax equal to log(d) minus the input entropy, and to the entropy gained in that measurement. If X also fixes rho, rho itself is omega; the converse follows from the same output equality. The proof also covers dimension one, where trace normalization fixes the only entry.

Theorem 1.2 (Every state lies on the entropy and freedom segment).

$$\forall d\in PositiveNatural,rho\in \mathrm{DensityState}\left(d\right),0\le \mathrm{vonNeumannEntropy}\left(rho\right)\wedge \left(0\le \mathrm{quantumRelativeEntropy}\left(rho,\mathrm{gibbsState}\left(0\right)\right)\wedge \mathrm{vonNeumannEntropy}\left(rho\right)+\mathrm{quantumRelativeEntropy}\left(rho,\mathrm{gibbsState}\left(0\right)\right)=\log \left(d\right)\right)$$

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

Citation. John Watrous (2018). The Theory of Quantum Information — spectral calculus, reductions and entropy. URL: https://cs.uwaterloo.ca/~watrous/TQI/TQI.pdf.

Commentary.

The eigenvalues of a density state form a probability distribution, and its von Neumann entropy is their Shannon entropy. The finite entropy bounds give zero at the lower end and log(d) at the upper end. The Gibbs identity supplies the complementary freedom. Thus any trajectory of density states lies on this segment point by point; no dynamical law or parametrization of time is assumed.

References

• Truth anchor: D5/S3/Quantum/Divergence/DualAccountFull.dual_account_full
• Truth anchor: D5/S3/Quantum/Divergence/DualAccountFull.entropy_freedom_segment
• Dependency: D5/S3/Entropy/EntropyNonneg
• Dependency: D5/S3/Quantum/Divergence/GibbsVariationalIdentity
• Dependency: D5/S3/Quantum/Sharpness/FreeNegentropyBudget
• Dependency: D5/S3/Quantum/Tomography/MutuallyUnbiasedDiagonalPlanes