Theorem 1 and abstract capstone: strong subadditivity with exact equality condition

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.strongSubadditivity

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

prove2quantum

Let $\rho_{123}>0$ be a trace-one state of three finite systems, and let every subscript denote its partial trace. Operators in a logarithm identity are extended by identity operators to the full system. Then

S(\rho_{123})+S(\rho_2)\le S(\rho_{12})+S(\rho_{23}),

with equality if and only if

\log\rho_{123}-\log\rho_{12}=\log\rho_{23}-\log\rho_2.

This characterizes exact saturation of strong subadditivity.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P51

Formal statement

noncomputable section

open scoped Matrix ComplexOrder ComplexConjugate Matrix.Norms.L2Operator

open MeasureTheory

namespace QAlgorithms.Papers.Independent.Intakethird100.P51

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact interfaces from the frozen accepted library; no local redeclarations.

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P56 (entropy holevo IsLaw)

open QAlgorithms.Papers.Independent.Information100.P27 (average)

open QAlgorithms.Papers.Independent.Dependency50.P21 (relativeEntropy marginalAB channelAdjoint)

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

open QAlgorithms.Papers.Independent.Gap48.P19 (shannonNats)

open QAlgorithms.Papers.Independent.Gap48.P33 (measurementInformation)

section Statements

variable {A B C D J K O : Type}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype J] [Fintype K] [Fintype O]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

variable [DecidableEq J] [DecidableEq K] [DecidableEq O]

/-- Theorem 1 and (3)–(4), PDF pp.3–4,12–13: SSA with its exact log equality condition. -/
theorem strongSubadditivity [Nonempty A] [Nonempty B] [Nonempty C] (rho : Mat (A × (B × C))) (h : FaithfulDensity rho) :
    0 ≤ ssaGap rho ∧ (ssaGap rho = 0 ↔ SSAlogCondition rho) := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intakethird100.P51

end

Source

Inequalities for Quantum Entropy: A Review with Conditions for Equality, arXiv:quant-ph/0205064v2, PDF p. 4, Theorem 1 and abstract capstone: strong subadditivity with exact equality condition

Read-back

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

For all nonempty finite index types $A,B,C$ with decidable equality and every positive definite complex matrix $\rho$ on $A\times(B\times C)$ with $\operatorname{tr}\rho=1$ , define

\Delta=S(\rho_{AB})+S(\rho_{BC})-S(\rho)-S(\rho_B), \qquad S(Z)=-\operatorname{Re}\operatorname{tr}f(Z),\quad f(x)=x\ln x,

where matrix functions use continuous functional calculus, $\rho_{AB}$ traces out $C$ , $\rho_{BC}$ traces out $A$ , and $\rho_B$ traces out both $A$ and $C$ . The theorem asserts $\Delta\ge0$ , together with the equivalence

\Delta=0 \quad\Longleftrightarrow\quad \log\rho-(\log\rho_{AB})\otimes I_C = I_A\otimes\log\rho_{BC}-I_A\otimes(\log\rho_B)\otimes I_C.

All tensor factors in this identity are arranged on $A\times(B\times C)$ , and each logarithm is the continuous-functional-calculus application of the natural real logarithm. Singleton registers are allowed; singular $\rho$ is excluded by positive definiteness.

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