Equation (22): purified/weak-monotonicity form of SSA

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.purifiedSSA

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

prove2quantum

Let $\rho_{1234}=|\psi\rangle\langle\psi|$ be any pure four-party state with $\|\psi\|=1$ , and form all marginals by partial trace. Then

S(\rho_4)+S(\rho_2)\le S(\rho_{12})+S(\rho_{14}).

Under this purification the displayed inequality is equivalent to SSA for $\rho_{123}$ . This records the purified weak-monotonicity form of SSA, including singular reduced states.

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]

/-- Equation (22), PDF pp.9,15: the purified weak-monotonicity inequality and its
pointwise equivalence to SSA of the complementary triple. Equation (36) omits S
in print; (22) and the purification argument determine the entropy reading. -/
theorem purifiedSSA [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] (psi : EuclideanSpace ℂ (A × (B × (C × D)))) (h : ‖psi‖ = 1) :
    let rho := pureDensity psi
    WeakMonotonicity (marginalABD rho) ∧
      (0 ≤ ssaGap (marginalABC rho) ↔ WeakMonotonicity (marginalABD 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. 9, Equation (22): purified/weak-monotonicity form of SSA

Read-back

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

For finite nonempty index types $A,B,C,D$ , each with decidable equality, and every Euclidean unit vector $\psi\in\mathbb C^{A\times(B\times(C\times D))}$ , form $\rho=|\psi\rangle\langle\psi|$ , whose entries are $\psi_x\overline{\psi_y}$ , and denote its reduced matrices by subscripts, obtained by summing over discarded indices. With $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ , where $f(x)=x\log x$ is applied by continuous functional calculus using natural logarithms and $\log0=0$ , the assertion is

S(\rho_D)+S(\rho_B)\le S(\rho_{AB})+S(\rho_{AD}),

together with the equivalence

0\le S(\rho_{AB})+S(\rho_{BC})-S(\rho_{ABC})-S(\rho_B) \quad\Longleftrightarrow\quad S(\rho_D)+S(\rho_B)\le S(\rho_{AB})+S(\rho_{AD}).

The first displayed inequality is precisely the stated weak-monotonicity condition on $\rho_{ABD}$ ; all four registers may be singletons.

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