Theorem 1 prime: expanded entropy reformulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.expanded_entropy

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)$ . Assume

\begin{aligned} S(AB)+S(BC)-S(B)-S(ABC)&=0,\ S(CA)+S(AB)-S(A)-S(CAB)&=0,\ S(AD)+S(DB)-S(D)-S(ADB)&=0. \end{aligned}

Then

S(ABC)+S(D)\ge S(AB)+S(CD),\qquad I(ABC;D)\ge I(AB;CD).

The two conclusions express the same entropy inequality after cancellation. All reordered subsystem labels denote the same tensor factors.

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.6, Theorem 1 prime: expanded entropy and mutual-information forms.
Subsystem permutations are unions of the same factors, and no purity is assumed. -/
theorem expanded_entropy (q : FourPartyState)
    (hABC : fourPartyEntropyBits q (A ∪ B) + fourPartyEntropyBits q (B ∪ C) - fourPartyEntropyBits q B - fourPartyEntropyBits q (A ∪ B ∪ C) = 0)
    (hCAB : fourPartyEntropyBits q (C ∪ A) + fourPartyEntropyBits q (A ∪ B) - fourPartyEntropyBits q A - fourPartyEntropyBits q (C ∪ A ∪ B) = 0)
    (hADB : fourPartyEntropyBits q (A ∪ D) + fourPartyEntropyBits q (D ∪ B) - fourPartyEntropyBits q D - fourPartyEntropyBits q (A ∪ D ∪ B) = 0) :
    fourPartyEntropyBits q (A ∪ B) + fourPartyEntropyBits q (C ∪ D) ≤ fourPartyEntropyBits q (A ∪ B ∪ C) + fourPartyEntropyBits q D ∧
    mutualValue (fourPartyEntropyBits q) (A ∪ B) (C ∪ D) ≤ mutualValue (fourPartyEntropyBits q) (A ∪ B ∪ 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. 6, Theorem 1 prime

Read-back

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

Let $q$ be any four-party state: positive natural-number dimensions $d_i$ for $i\in\Omega=\{0,1,2,3\}$ , allowing dimensions equal to $1$ , together with a positive semidefinite complex matrix $\rho$ of trace $1$ indexed by $\prod_i\{0,\ldots,d_i-1\}$ . For each subset $s$ , define $H_s=-\operatorname{Re}\operatorname{tr}f(\rho_s)$ , where $\rho_s$ sums equal row and column coordinates outside $s$ , and $f(u)=u\log_2u$ is applied by functional calculus with $0\log_2 0=0$ . The symbols $A,B,C,D$ are the fixed subsets of $\Omega$ referenced in the declaration, whose elements are not specified in the supplied code; concatenated subscripts denote unions. Assuming all three equalities

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

the theorem asserts the conjunction

H_{AB}+H_{CD}\le H_{ABC}+H_D \quad\text{and}\quad H_{AB}+H_{CD}-H_{ABCD} \le H_{ABC}+H_D-H_{ABCD}.

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