Remark 4: SSA equality gives separability and nonnegative endpoint conditional entropy

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.ssa_endpoint_separable

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

prove2quantum

Let $\rho_{ABC}$ be a trace-one positive semidefinite density matrix on arbitrary finite-dimensional complex factors $A,B,C$ of positive dimension. All entropies are in bits and all marginals are actual partial traces of $\rho$ . Use $S(X\mid Y)=S(XY)-S(Y)$ and $I(X;Z\mid Y)=S(XY)+S(YZ)-S(XYZ)-S(Y)$ . Without assuming SSA equality,

2S(A\mid C)+I(A;C\mid B)=[S(A\mid B)+S(A\mid C)]+I(A;B\mid C)\ge0.

If $I(A;C\mid B)=0$ , then $\rho_{AC}$ is separable, meaning a finite convex combination of product density matrices, and $S(A\mid C)\ge0$ . This records the structural consequence while identifying the entropy conclusion as a consequence of the basic inequalities.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P97

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P97

attribute [local instance] Classical.propDecidable Classical.decEq

local notation "A" => ({0} : Finset (Fin 4))

local notation "B" => ({1} : Finset (Fin 4))

local notation "C" => ({2} : Finset (Fin 4))

local notation "D" => ({3} : Finset (Fin 4))

/-- PDF p.5, Remark 4: the identity and nonnegativity are unconditional; SSA
equality additionally implies separability of AC and S(A|C) ≥ 0. -/
theorem ssa_endpoint_separable {X Y Z : Type*}
    [Fintype X] [Fintype Y] [Fintype Z] [Nonempty X] [Nonempty Y] [Nonempty Z]
    (rho : Matrix (X × (Y × Z)) (X × (Y × Z)) ℂ) (hrho : IsDensityMatrix rho) :
    let sab := vnEntropy (marginalAB3 rho)
    let sac := vnEntropy (marginalAC3 rho)
    let sbc := vnEntropy (traceLeft rho)
    let sa := vnEntropy (traceRight (marginalAB3 rho))
    let sb := vnEntropy (traceLeft (marginalAB3 rho))
    let sc := vnEntropy (traceLeft (marginalAC3 rho))
    let sabc := vnEntropy rho
    let acGivenB := sab + sbc - sabc - sb
    let abGivenC := sac + sbc - sabc - sc
    (2 * (sac - sc) + acGivenB = (sab - sb) + (sac - sc) + abGivenC) ∧
    0 ≤ (sab - sb) + (sac - sc) + abGivenC ∧
    (acGivenB = 0 → Entanglement.IsSeparableDensity (marginalAC3 rho) ∧ 0 ≤ sac - sc) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P97

end

Source

A new inequality for the von Neumann entropy, arXiv:quant-ph/0406162v1, PDF p. 5, Remark 4

Read-back

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

For any finite, nonempty types $X,Y,Z$ , each equipped with a finite enumeration, and any positive semidefinite complex matrix $\rho$ of trace $1$ indexed by $X\times(Y\times Z)$ , define matrices

\begin{aligned} (\rho_{AB})_{(a,b),(a',b')}&=\sum_{c\in Z}\rho_{(a,(b,c)),(a',(b',c))},\\ (\rho_{AC})_{(a,c),(a',c')}&=\sum_{b\in Y}\rho_{(a,(b,c)),(a',(b,c'))},\\ (\rho_{BC})_{(b,c),(b',c')}&=\sum_{a\in X}\rho_{(a,(b,c)),(a,(b',c'))},\\ (\rho_A)_{a,a'}&=\sum_{b\in Y}(\rho_{AB})_{(a,b),(a',b)},\\ (\rho_B)_{b,b'}&=\sum_{a\in X}(\rho_{AB})_{(a,b),(a,b')},\\ (\rho_C)_{c,c'}&=\sum_{a\in X}(\rho_{AC})_{(a,c),(a,c')}. \end{aligned}

For each of these matrices $\sigma$ , put $S(\sigma)=-\operatorname{Re}\operatorname{tr}f(\sigma)$ , with $f(u)=u\log_2u$ applied by functional calculus and $0\log_2 0=0$ . Write $s_{AB}=S(\rho_{AB})$ , $s_{AC}=S(\rho_{AC})$ , $s_{BC}=S(\rho_{BC})$ , $s_A=S(\rho_A)$ , $s_B=S(\rho_B)$ , $s_C=S(\rho_C)$ , and $s_{ABC}=S(\rho)$ , and set

\alpha=s_{AB}+s_{BC}-s_{ABC}-s_B,\qquad \beta=s_{AC}+s_{BC}-s_{ABC}-s_C.

Then all three assertions hold:

\begin{gathered} 2(s_{AC}-s_C)+\alpha =(s_{AB}-s_B)+(s_{AC}-s_C)+\beta,\\ 0\le(s_{AB}-s_B)+(s_{AC}-s_C)+\beta,\\ \alpha=0\ \Longrightarrow\ \left[ \begin{array}{l} \displaystyle \exists m\in\mathbb N,\ w_0,\ldots,w_{m-1}\in\mathbb R,\ P_0,\ldots,P_{m-1}\in\mathbb C^{X\times X},\ Q_0,\ldots,Q_{m-1}\in\mathbb C^{Z\times Z}:\\ \displaystyle w_j\ge0\text{ for all }j,\quad \sum_{j=0}^{m-1}w_j=1,\quad P_j,Q_j\text{ are positive semidefinite and have trace }1\text{ for all }j,\\ \displaystyle \rho_{AC}=\sum_{j=0}^{m-1}w_j(P_j\otimes Q_j), \qquad 0\le s_{AC}-s_C. \end{array} \right] \end{gathered}

Here $(P_j\otimes Q_j)_{(a,c),(a',c')}=(P_j)_{a,a'}(Q_j)_{c,c'}$ . The weight normalization excludes $m=0$ . The quantity $s_A$ is defined but does not occur in these conclusions.

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