A completely positive trace-decreasing map can increase relative entropy

Open

QAlgorithms.Papers.Independent.Intakethird100.P46.trace_decrease_counterexample

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

On complex $2\times2$ matrices define $\Phi\left(\begin{smallmatrix}v&w\\x&y\end{smallmatrix}\right)=\operatorname{diag}(v/2,y)$ and fix the density matrices $\rho=\operatorname{diag}(1/3,2/3)$ and $\sigma=\operatorname{diag}(2/3,1/3)$ . The map is complex-linear, completely positive, and trace-nonincreasing on every positive matrix. Nevertheless, for literal unnormalized relative entropy in natural units,

D(\rho\Vert\sigma)=\frac{\log2}{3}<\frac{\log2}{2}=D(\Phi(\rho)\Vert\Phi(\sigma)).

The output operators have traces $5/6$ and $2/3$ and are not asserted to be normalized. This counterexample explains why trace nonincrease alone does not suffice for the Umegaki data-processing inequality.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P46

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P46

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms

open QAlgorithms.Papers.Independent.Dependency50.P13
  (IsTraceClass TraceClass IsPositive operatorTrace)

open QAlgorithms.Papers.Independent.Dependency50.P35 (Dominates)

open QAlgorithms.Papers.Independent.Bridge50.P49 (beigiSandwichedDivergence)

variable {H K : Type*}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]

/-- Müller-Hermes–Reeb, arXiv:1512.06117v3, PDF p.3, unnumbered counterexample.
Both INPUTS are density matrices. The CP trace-nonincreasing map produces
subnormalized operators, and the two literal relative entropies increase strictly. -/
theorem trace_decrease_counterexample :
    Entanglement.IsCompletelyPositive traceDecreaseMap ∧
    PositiveMatrixTraceNonincreasing traceDecreaseMap ∧
    IsDensityMatrix counterexampleRho ∧ IsDensityMatrix counterexampleSigma ∧
    finiteLiteralRelativeEntropy counterexampleRho counterexampleSigma =
      ((Real.log 2 / 3 : ℝ) : EReal) ∧
    ((Real.log 2 / 3 : ℝ) : EReal) < ((Real.log 2 / 2 : ℝ) : EReal) ∧
    finiteLiteralRelativeEntropy (traceDecreaseMap counterexampleRho)
      (traceDecreaseMap counterexampleSigma) = ((Real.log 2 / 2 : ℝ) : EReal) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P46

end

Source

Monotonicity of the Quantum Relative Entropy Under Positive Maps, arXiv:1512.06117v3, PDF p. 3, Unnumbered counterexample: trace nonincrease alone does not give relative-entropy monotonicity

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Define the complex linear map on $2\times2$ matrices and the two matrices

\Phi(X)= \begin{pmatrix}X_{00}/2&0\\0&X_{11}\end{pmatrix}, \qquad \rho=\begin{pmatrix}1/3&0\\0&2/3\end{pmatrix}, \qquad \sigma=\begin{pmatrix}2/3&0\\0&1/3\end{pmatrix}.

For finite matrices, define the extended-real quantity

D_{\mathrm{lit}}(A,B)= \begin{cases} \operatorname{Re}\operatorname{tr}\!\left(f(A)-A\log B\right), &\ker B\subseteq\ker A,\\ +\infty,&\text{otherwise}, \end{cases} \qquad f(t)=t\log t,

using continuous functional calculus and the natural logarithm, with $\log0=0$ . The declaration asserts all of the following: $\Phi$ is completely positive, meaning that for every natural number $r$ , including $r=0$ , applying $\Phi$ to every $2\times2$ block of any positive semidefinite matrix indexed by $\{0,\ldots,r-1\}\times\{0,1\}$ gives a positive semidefinite matrix; for every positive semidefinite $A$ , $\Phi(A)$ is positive semidefinite and $\operatorname{Re}\operatorname{tr}\Phi(A)\le\operatorname{Re}\operatorname{tr}A$ ; both $\rho$ and $\sigma$ are positive semidefinite with complex trace one; and

D_{\mathrm{lit}}(\rho,\sigma)=\frac{\log2}{3} <\frac{\log2}{2} =D_{\mathrm{lit}}(\Phi(\rho),\Phi(\sigma)).

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph