Remark 2: explicit SSA-equality mixtures of biorthogonal product components

Open

QAlgorithms.Papers.Independent.Intakethird100.P63.remark2_productComponents

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.

Let $(w_k,\sigma_{12}^k)$ be a discrete ensemble of two-party states, with both marginal families orthogonal across distinct positive-weight labels. For every active label choose any normalized third-party density $\tau_3^k$ . Set $\rho=\sum_k w_k(\sigma_{12}^k\otimes\tau_3^k)$ , a trace-norm convergent sum. Then

I(1:2)_\rho=I(1:23)_\rho,

where $I(A:B)=S_A+S_B-S_{A\cup B}$ . The third factors may coincide or differ. This constructs concrete members of the SSA-equality family.

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)

/-- Remark 2, PDF p.7: explicit SSA-equality states constructed from biorthogonal
two-party components and arbitrary third-party factors, which may coincide or differ. -/
theorem remark2_productComponents (e : DiscreteDensityEnsemble (Fin 2 → ℕ))
    (hbio : Biorthogonal e {0} {1}) (tau : ℕ → (Matrix ℕ ℕ ℂ))
    (htau : ∀ k, 0 < e.weight k → IsDensity (tau k))
    (hfinite : FiniteSubsystemEntropies (productMixture e tau)) :
    clusterMutualInformation (productMixture e tau) {0} {1} =
      clusterMutualInformation (productMixture e tau) {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. 7, Remark 2: concrete SSA-equality states from biorthogonal product components

Read-back

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

Let $e$ consist of nonnegative summable weights $w_k\in\mathbb R$ of sum $1$ and kernels $X_k$ on $\mathbb N^2$ , and let $\tau_k$ be arbitrary complex kernels on $\mathbb N$ . For every $k$ with $w_k>0$ , assume both $X_k$ and $\tau_k$ are density kernels: each has an entrywise expansion $\sum_r u_r(i)\overline{v_r(j)}$ by square-summable vectors with $\sum_r\|u_r\|\|v_r\|<\infty$ , all its finite quadratic forms are real and nonnegative, and its real diagonal is summable with sum $1$ . No density condition is required at zero weight. For a kernel $Y$ on $\mathbb N^q$ and a set $C\subseteq\{0,\ldots,q-1\}$ , define

Y_C(a,b)=\sum_{z:C^\complement\to\mathbb N}Y(a\sqcup z,b\sqcup z),

with $a,b:C\to\mathbb N$ and coordinate concatenation $a\sqcup z$ . Assume that for distinct positive-weight indices $k,l$ , both $C=\{0\}$ and $C=\{1\}$ satisfy $\sum_z(X_k)_C(a,z)(X_l)_C(z,b)=0$ for all $a,b$ . Define the three-coordinate kernel

T(x,y)=\sum_{k=0}^{\infty}w_k X_k\bigl((x_0,x_1),(y_0,y_1)\bigr)\tau_k(x_2,y_2).

For any kernel $Y$ , define $H(Y)\in[0,\infty]$ as the infimum of $\sum_r[-a_r\log a_r]_+$ over expansions $Y=\sum_r a_rq_rq_r^*$ , where the nonnegative weights are summable with sum $1$ , the vectors 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(T_C)\ne+\infty$ for every subset $C\subseteq\{0,1,2\}$ , including the empty set. With $S_Y(C)=\operatorname{toReal}H(Y_C)$ , where $+\infty$ converts to $0$ , and $J_Y(A,B)=S_Y(A)+S_Y(B)-S_Y(A\cup B)$ , the assertion is

J_T(\{0\},\{1\})=J_T(\{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