Theorem 1 double prime: all three purification variants

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.purification_variants

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)$ . Each of the following is a separate implication for this state:

If $I(A;C\mid B)=I(B;C\mid A)=I(A;B\mid CD)=0$ , then

S(C\mid AB)+S(C\mid ABD)\ge0.

If $S(C\mid A)+S(C\mid BD)=0$ , $I(A;C\mid BD)=0$ , and $S(A\mid D)+S(A\mid BC)=0$ , then

S(C\mid D)+S(C\mid BD)\le0.

If $S(B\mid A)+S(B\mid CD)=0$ , $S(A\mid B)+S(A\mid CD)=0$ , and $I(A;B\mid D)=0$ , then

S(D)+S(CD)\ge S(AB)+S(ABC).

These are the three purification reformulations of the constrained inequality; no purity assumption is imposed on $\rho_{ABCD}$ .

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 pp.6–7, Theorem 1 double prime: three separate implications, each with
its own three zero expressions. The purifying E in the proof is not input data.
Case (1) retains C|ABD; the inequality in case (2) is ≤. -/
theorem purification_variants (q : FourPartyState) :
    ((conditionalMutualValue (fourPartyEntropyBits q) A C B = 0 ∧ conditionalMutualValue (fourPartyEntropyBits q) B C A = 0 ∧
      conditionalMutualValue (fourPartyEntropyBits q) A B (C ∪ D) = 0) →
      0 ≤ entropyDifference (fourPartyEntropyBits q) C (A ∪ B) + entropyDifference (fourPartyEntropyBits q) C (A ∪ B ∪ D)) ∧
    ((entropyDifference (fourPartyEntropyBits q) C A + entropyDifference (fourPartyEntropyBits q) C (B ∪ D) = 0 ∧
      conditionalMutualValue (fourPartyEntropyBits q) A C (B ∪ D) = 0 ∧
      entropyDifference (fourPartyEntropyBits q) A D + entropyDifference (fourPartyEntropyBits q) A (B ∪ C) = 0) →
      entropyDifference (fourPartyEntropyBits q) C D + entropyDifference (fourPartyEntropyBits q) C (B ∪ D) ≤ 0) ∧
    ((entropyDifference (fourPartyEntropyBits q) B A + entropyDifference (fourPartyEntropyBits q) B (C ∪ D) = 0 ∧
      entropyDifference (fourPartyEntropyBits q) A B + entropyDifference (fourPartyEntropyBits q) A (C ∪ D) = 0 ∧
      conditionalMutualValue (fourPartyEntropyBits q) A B D = 0) →
      fourPartyEntropyBits q (A ∪ B) + fourPartyEntropyBits q (A ∪ B ∪ C) ≤ fourPartyEntropyBits q D + 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. 6, Theorem 1 double prime

Read-back

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

For every four-party state $q$ , consisting of positive natural-number dimensions $d_i$ for $i\in\Omega=\{0,1,2,3\}$ , allowing $d_i=1$ , and a positive semidefinite complex matrix $\rho$ of trace $1$ indexed by $\prod_i\{0,\ldots,d_i-1\}$ , 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$ . Let $A,B,C,D$ denote the fixed subsets of $\Omega$ referenced in the declaration; their elements are not supplied. Concatenated subscripts denote unions. The theorem asserts that all three of the following implications hold:

\begin{gathered} \left[ \begin{aligned} H_{AB}+H_{BC}-H_{ABC}-H_B&=0,\\ H_{AB}+H_{AC}-H_{ABC}-H_A&=0,\\ H_{ACD}+H_{BCD}-H_{ABCD}-H_{CD}&=0 \end{aligned} \right] \Longrightarrow 0\le (H_{ABC}-H_{AB})+(H_{ABCD}-H_{ABD}), \\[8pt] \left[ \begin{aligned} (H_{AC}-H_A)+(H_{BCD}-H_{BD})&=0,\\ H_{ABD}+H_{BCD}-H_{ABCD}-H_{BD}&=0,\\ (H_{AD}-H_D)+(H_{ABC}-H_{BC})&=0 \end{aligned} \right] \Longrightarrow (H_{CD}-H_D)+(H_{BCD}-H_{BD})\le0, \\[8pt] \left[ \begin{aligned} (H_{AB}-H_A)+(H_{BCD}-H_{CD})&=0,\\ (H_{AB}-H_B)+(H_{ACD}-H_{CD})&=0,\\ H_{AD}+H_{BD}-H_{ABD}-H_D&=0 \end{aligned} \right] \Longrightarrow H_{AB}+H_{ABC}\le H_D+H_{CD}. \end{gathered}

Each implication has its own three hypotheses; no purity assumption on $\rho$ appears.

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