Equation (20): equivalence of the endpoint-exchanged SSA equalities

Open

QAlgorithms.Papers.Independent.Intakethird100.P63.eq20_equivalentEqualities

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

prove2quantum

All states below are positive trace-class density operators of trace one on completed complex Hilbert tensor products, represented in countable orthonormal coordinates. Finite dimensional systems are included. Entropies use natural logarithms and the convention $0\log 0=0$ . Every subsystem entropy occurring in an entropy difference is finite; this is the proof-supported finite-entropy reading of the source, and imposes no finite Hilbert dimension.

For every tripartite state $\rho$ , with $I(A:B)=S_A+S_B-S_{A\cup B}$ formed from its actual marginals,

I(1:2)_\rho=I(1:23)_\rho\quad\Longleftrightarrow\quad I(2:3)_\rho=I(12:3)_\rho.

Thus SSA equality in one endpoint orientation is equivalent to equality in the other. This is a general entropy identity; the biorthogonal family is an application.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P63

Formal statement

noncomputable section

open scoped ENNReal BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P63

attribute [local instance] Classical.propDecidable Classical.decEq

-- Reuse the accepted nuclear trace-class, positive, trace-one predicate verbatim.

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity)

open QAlgorithms.Papers.Independent.Dependency50.P13 (finiteRelativeEntropy)

/-- Unnumbered (20), PDF p.8: the endpoint-exchanged SSA equalities are equivalent
for every finite-entropy tripartite density, without an ensemble premise. -/
theorem eq20_equivalentEqualities (rho : (Matrix (Fin 3 → ℕ) (Fin 3 → ℕ) ℂ)) (hrho : IsDensity rho)
    (hfinite : FiniteSubsystemEntropies rho) :
    clusterMutualInformation rho {0} {1} = clusterMutualInformation rho {0} {1, 2} ↔
      clusterMutualInformation rho {1} {2} = clusterMutualInformation rho {0, 1} {2} := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P63

end

Source

On Mutual Information in Multipartite Quantum States and Equality in Strong Subadditivity of Entropy, arXiv:quant-ph/0311193v1, PDF p. 8, Unnumbered Eq. (20): equivalent SSA equality after exchanging the endpoint roles

Read-back

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

Let $\rho$ be a complex kernel on $\mathbb N^3$ admitting an entrywise expansion $\rho(x,y)=\sum_r u_r(x)\overline{v_r(y)}$ by square-summable vectors with $\sum_r\|u_r\|\|v_r\|<\infty$ , having real nonnegative finite quadratic forms, and having a summable real diagonal of sum $1$ . For $C\subseteq\{0,1,2\}$ , define $\rho_C(a,b)=\sum_{z:C^\complement\to\mathbb N}\rho(a\sqcup z,b\sqcup z)$ , where $a,b:C\to\mathbb N$ and coordinate concatenation fills the complementary coordinates with $z$ . For any kernel $Y$ , let $H(Y)$ be the infimum in $[0,\infty]$ of $\sum_r[-a_r\log a_r]_+$ over representations $Y=\sum_r a_rq_rq_r^*$ , where $a_r\ge0$ are summable with sum $1$ , all $q_r$ are square-summable, and positive-weight vectors are unit and mutually orthogonal; zero-weight vectors are unrestricted, $[t]_+=\max(t,0)$ , and an empty infimum is $+\infty$ . Assume $H(\rho_C)\ne+\infty$ for every $C$ , including the empty set. Define $S(C)=\operatorname{toReal}H(\rho_C)$ , with $+\infty$ converting to $0$ , and $J(A,B)=S(A)+S(B)-S(A\cup B)$ . Then the following is an equivalence:

J(\{0\},\{1\})=J(\{0\},\{1,2\}) \quad\Longleftrightarrow\quad J(\{1\},\{2\})=J(\{0,1\},\{2\}).

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