Theorem 2: biorthogonal mixtures preserve SSA equality and yield correlated nonproduct cases

Open

QAlgorithms.Papers.Independent.Intakethird100.P63.theorem2_biorthogonalSSA

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. A discrete ensemble may have finitely or countably many components: its weights $w_k$ are nonnegative and sum to one, and each component with $w_k>0$ is a normalized density operator. Every mixture below is the computed trace-norm convergent sum $\rho=\sum_k w_k\rho^k$ . All component conditions concern positive-weight labels only.

For a tripartite ensemble suppose that for distinct active labels $k,l$ , both $\rho_1^k\rho_1^l=0$ and $\rho_2^k\rho_2^l=0$ . If every active component satisfies $I(1:2)_{\rho^k}=I(1:23)_{\rho^k}$ , then

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

Moreover, if at least two labels have positive weight and $\rho\ne\rho_{12}\otimes\rho_3$ , then

I(2:3)_\rho>0.

Here $I(A:B)=S_A+S_B-S_{A\cup B}$ and all subscripts denote actual marginals. The result gives SSA equality beyond independent-third-factor states.

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)

/-- Theorem 2, PDF pp.5,7: both SSA equality and positivity outside the aggregate
product exception (8). Finiteness of mixture marginals implies it for active components.
Zero labels do not count toward the condition of at least two terms. -/
theorem theorem2_biorthogonalSSA (e : DiscreteDensityEnsemble (Fin 3 → ℕ))
    (hbio : Biorthogonal e {0} {1})
    (hfinite : FiniteSubsystemEntropies (herbutMixture e))
    (hssa : ∀ k, 0 < e.weight k →
      clusterMutualInformation (e.component k) {0} {1} = clusterMutualInformation (e.component k) {0} {1, 2}) :
    clusterMutualInformation (herbutMixture e) {0} {1} = clusterMutualInformation (herbutMixture e) {0} {1, 2} ∧
    ((∃ k l, k ≠ l ∧ 0 < e.weight k ∧ 0 < e.weight l) →
      herbutMixture e ≠ productAcross (herbutMixture e) {0, 1} →
      0 < clusterMutualInformation (herbutMixture e) {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. 5, Theorem 2 (seed paper result): biorthogonal mixtures preserve SSA equality, with correlated nonproduct cases

Read-back

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

Let $e$ consist of nonnegative summable real weights $w_k$ , $k\in\mathbb N$ , with $\sum_k w_k=1$ , and complex kernels $K_k$ on $\mathbb N^3$ . For every $k$ with $w_k>0$ , require an entrywise expansion $K_k(i,j)=\sum_r a_r(i)\overline{b_r(j)}$ with square-summable vectors and $\sum_r\|a_r\|\|b_r\|<\infty$ , real nonnegative finite quadratic forms $\sum_{i,j\in F}\overline{z_i}K_k(i,j)z_j$ for every finite $F$ and arbitrary complex $z$ , and summable real diagonal of sum $1$ ; zero-weight components are unrestricted. For any kernel $K$ on $\mathbb N^3$ , define $R_C^K(x,y)=\sum_{z\in\mathbb N^{C^c}}K(x\oplus_C z,y\oplus_C z)$ . Define $H(Q)$ as the infimum in $[0,\infty]$ of $\sum_j\max\{-p_j\log p_j,0\}$ over representations $Q(a,b)=\sum_j p_j u_j(a)\overline{u_j(b)}$ , with nonnegative summable weights of sum $1$ and square-summable vectors that are unit and pairwise orthogonal at distinct positive-weight indices; an empty infimum is $+\infty$ . Put $S_K(C)=H(R_C^K).\mathrm{toReal}$ , with $+\infty$ converted to $0$ , and $I_K(A:B)=S_K(A)+S_K(B)-S_K(A\cup B)$ . Assume that, for all distinct $k,l$ with positive weights and for each $C=\{0\},\{1\}$ , the reduced kernels satisfy $\sum_z R_C^{K_k}(x,z)R_C^{K_l}(z,y)=0$ for every $x,y$ . Let $\bar K(x,y)=\sum_k w_kK_k(x,y)$ , assume $H(R_C^{\bar K})\ne+\infty$ for every $C\subseteq\{0,1,2\}$ , including the empty set, and assume $I_{K_k}(\{0\}:\{1\})=I_{K_k}(\{0\}:\{1,2\})$ for every positive-weight $k$ . Then

I_{\bar K}(\{0\}:\{1\})=I_{\bar K}(\{0\}:\{1,2\}).

In addition, if there exist two distinct positive-weight indices and $\bar K$ is unequal to the kernel $(x,y)\mapsto R_{\{0,1\}}^{\bar K}(x|_{\{0,1\}},y|_{\{0,1\}})R_{\{2\}}^{\bar K}(x_2,y_2)$ , then $0<I_{\bar K}(\{1\}:\{2\})$ . All kernel series use total infinite sums; finite subsystem entropies are assumed for $\bar K$ , with no such assumption on the individual components.

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