Theorem 1: the new constrained four-party entropy inequality

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.constrained_fourParty

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

prove2quantum

Let $\rho_{ABCD}$ be a positive semidefinite complex density matrix of trace one on four finite-dimensional tensor factors $A,B,C,D$ , each of positive dimension (dimension one is allowed). Every $S(X)$ is the base-two von Neumann entropy of the actual $X$ marginal of this same state, with $0\log_2 0=0$ . For disjoint groups write $S(X\mid Y)=S(XY)-S(Y)$ , $I(X;Y)=S(X)+S(Y)-S(XY)$ , and $I(X;Z\mid Y)=S(XY)+S(YZ)-S(XYZ)-S(Y)$ . If $I(A;C\mid B)=I(B;C\mid A)=I(A;B\mid D)=0$ , then

I(C;D)\ge I(C;AB).

This bounds the correlation of $C$ with $AB$ by its correlation with $D$ under the three specified SSA equalities.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P97

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P97

attribute [local instance] Classical.propDecidable Classical.decEq

local notation "A" => ({0} : Finset (Fin 4))

local notation "B" => ({1} : Finset (Fin 4))

local notation "C" => ({2} : Finset (Fin 4))

local notation "D" => ({3} : Finset (Fin 4))

/-- PDF p.3, Theorem 1 (proof pp.3–5): the constrained four-party inequality. -/
theorem constrained_fourParty (q : FourPartyState) (hc : Constraints (fourPartyEntropyBits q)) :
    mutualValue (fourPartyEntropyBits q) C (A ∪ B) ≤ mutualValue (fourPartyEntropyBits q) C D := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P97

end

Source

A new inequality for the von Neumann entropy, arXiv:quant-ph/0406162v1, PDF p. 3, Theorem 1

Read-back

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

Let $q$ be any four-party state: it specifies positive natural-number dimensions $d_i$ for $i\in\Omega=\{0,1,2,3\}$ , and a positive semidefinite complex matrix $\rho$ of trace $1$ , indexed by $\prod_{i\in\Omega}\{0,\ldots,d_i-1\}$ . Dimensions equal to $1$ are allowed. For each subset $s\subseteq\Omega$ , let $\rho_s$ be the matrix obtained by summing over equal row and column coordinates outside $s$ , and write

H_s=-\operatorname{Re}\operatorname{tr}\bigl(f(\rho_s)\bigr), \qquad f(u)=u\log_2u,

where $f(\rho_s)$ uses functional calculus and $0\log_2 0=0$ . Let $A,B,C,D$ denote the fixed subsets of $\Omega$ referenced in the declaration; their elements are not specified in the supplied code. Concatenated subscripts denote unions, so $H_{ABC}=H_{A\cup B\cup C}$ . If

H_{AB}+H_{BC}-H_{ABC}-H_B=0,\qquad H_{AB}+H_{AC}-H_{ABC}-H_A=0,\qquad H_{AD}+H_{BD}-H_{ABD}-H_D=0,

then

H_C+H_{AB}-H_{ABC}\le H_C+H_D-H_{CD}.

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