Closing result: partial discarding inside the third cluster preserves mutual information

Open

QAlgorithms.Papers.Independent.Intakethird100.P63.partialDiscard_preservesInformation

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.

Let $A,B,R$ be nonempty pairwise disjoint clusters partitioning a finite party set. Suppose the component reductions on $A$ and $B$ are biorthogonal across distinct active labels, and every active component satisfies $I(A:B)_{\rho^k}=I(A:BR)_{\rho^k}$ . For every subset $D\subseteq R$ ,

I(A:BR)_\rho=I(A:B(R\setminus D))_\rho=I(A:B)_\rho,

where juxtaposition denotes union of disjoint clusters and $I(X:Y)=S_X+S_Y-S_{X\cup Y}$ . The clusters $A,B$ may themselves be composite. This includes retaining all of $R$ and discarding all of it.

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)

/-- Closing unnumbered result, PDF p.8: in the Theorem 2 family, every intermediate
discard inside the third cluster preserves mutual information. The endpoint parties
may themselves be composite clusters. Empty D and D=R are included. -/
theorem partialDiscard_preservesInformation {n : ℕ}
    (e : DiscreteDensityEnsemble (Fin n → ℕ)) (A B R : Cluster n)
    (hA : A.Nonempty) (hB : B.Nonempty) (hR : R.Nonempty)
    (hAB : Disjoint A B) (hAR : Disjoint A R) (hBR : Disjoint B R)
    (hcover : A ∪ B ∪ R = Finset.univ)
    (hbio : Biorthogonal e A B)
    (hfinite : FiniteSubsystemEntropies (herbutMixture e))
    (hssa : ∀ k, 0 < e.weight k →
      clusterMutualInformation (e.component k) A B = clusterMutualInformation (e.component k) A (B ∪ R))
    (D : Cluster n) (hD : D ⊆ R) :
    clusterMutualInformation (herbutMixture e) A (B ∪ R) = clusterMutualInformation (herbutMixture e) A (B ∪ (R \ D)) ∧
    clusterMutualInformation (herbutMixture e) A (B ∪ (R \ D)) = clusterMutualInformation (herbutMixture e) A B := 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 closing result: partial discarding inside the third cluster also preserves mutual information

Read-back

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

For any $n\in\mathbb N$ , let $e$ consist of nonnegative summable real weights $w_k$ with sum $1$ and complex kernels $X_k$ on $\mathbb N^n$ . Whenever $w_k>0$ , require that $X_k$ admit an entrywise expansion $X_k(x,y)=\sum_r u_r(x)\overline{v_r(y)}$ by square-summable vectors with $\sum_r\|u_r\|\|v_r\|<\infty$ , have real nonnegative finite quadratic forms, and have a summable real diagonal of sum $1$ ; zero-weight components are unrestricted. Define $X(x,y)=\sum_k w_kX_k(x,y)$ . For each set $C\subseteq\{0,\ldots,n-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$ . Define $H(Y)$ as the infimum in $[0,\infty]$ of $\sum_r[-a_r\log a_r]_+$ over expansions $Y=\sum_r a_rq_rq_r^*$ with nonnegative summable weights of sum $1$ and square-summable vectors whose positive-weight members are unit and mutually orthogonal; zero-weight vectors are unrestricted, $[t]_+=\max(t,0)$ , and an empty infimum is $+\infty$ . Put $S_Y(C)=\operatorname{toReal}H(Y_C)$ , where $\operatorname{toReal}(+\infty)=0$ , and $J_Y(C,E)=S_Y(C)+S_Y(E)-S_Y(C\cup E)$ . Let $A,B,R$ be nonempty, pairwise disjoint sets of coordinates with $A\cup B\cup R=\{0,\ldots,n-1\}$ ; these hypotheses in particular force $n\ge3$ . Assume that for distinct $k,l$ with $w_k,w_l>0$ , both $C=A$ and $C=B$ satisfy $\sum_z(X_k)_C(a,z)(X_l)_C(z,b)=0$ for all $a,b$ . Assume also that $H(X_C)\ne+\infty$ for every coordinate set $C$ , including the empty set, and that every positive-weight component satisfies

J_{X_k}(A,B)=J_{X_k}(A,B\cup R).

Then, for every coordinate set $D\subseteq R$ , including $D=\varnothing$ and $D=R$ , both equalities hold:

J_X(A,B\cup R)=J_X\bigl(A,B\cup(R\setminus D)\bigr), \qquad J_X\bigl(A,B\cup(R\setminus D)\bigr)=J_X(A,B).

No finiteness assumption is imposed on component marginal entropies; the component equalities use the stated conversion of infinite entropy to $0$ .

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