Remark 3: no proper subset of the three constraints suffices

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.constraints_irredundant

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)$ . Number the constraints $c_0=I(A;C\mid B)$ , $c_1=I(B;C\mid A)$ , and $c_2=I(A;B\mid D)$ . For every proper subset $T\subsetneq\{0,1,2\}$ there is such a state satisfying

c_i=0\quad(i\in T),\qquad I(C;D)<I(C;AB).

Thus every one of the three constraints is necessary for this implication. The printed second counterexample has three-bit kets on $BC$ ; the intended two-party kets are $|00\rangle$ and $|11\rangle$ .

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.5, Remark 3: every proper subset of the three constraints admits a
counterexample to the conclusion. Source correction: the printed second witness
has three-bit kets on BC; these must read |00> and |11> on that two-party register.
The theorem states irredundance itself and does not assume witness MI values. -/
theorem constraints_irredundant :
    ∀ t : Finset (Fin 3), t ≠ Finset.univ →
      ∃ q : FourPartyState, (∀ i ∈ t, constraintValue (fourPartyEntropyBits q) i = 0) ∧
        mutualValue (fourPartyEntropyBits q) C D < mutualValue (fourPartyEntropyBits q) C (A ∪ B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P97

end

Source

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

Read-back

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

Let $A,B,C,D$ be the fixed subsets of $\Omega=\{0,1,2,3\}$ referenced in the declaration; their elements are not specified in the supplied code. For a four-party state $q$ , its data are positive natural-number dimensions $d_i$ , allowing $d_i=1$ , and a positive semidefinite complex matrix $\rho$ of trace $1$ indexed by $\prod_i\{0,\ldots,d_i-1\}$ . Write $H_s^q=-\operatorname{Re}\operatorname{tr}f(\rho_s)$ , where $\rho_s$ is obtained by summing equal row and column coordinates outside $s$ , and $f(u)=u\log_2u$ is applied by functional calculus with $0\log_2 0=0$ ; concatenated subscripts denote unions. Define the three real numbers

\begin{aligned} c_0(q)&=H_{AB}^q+H_{BC}^q-H_{ABC}^q-H_B^q,\\ c_1(q)&=H_{AB}^q+H_{AC}^q-H_{ABC}^q-H_A^q,\\ c_2(q)&=H_{AD}^q+H_{BD}^q-H_{ABD}^q-H_D^q. \end{aligned}

For every proper subset $t\subsetneq\{0,1,2\}$ , there exists a four-party state $q$ such that $c_i(q)=0$ for every $i\in t$ , and

H_C^q+H_D^q-H_{CD}^q < H_C^q+H_{AB}^q-H_{ABC}^q.

The subset $t$ may be empty, in which case the conditions $c_i(q)=0$ impose no requirements. No value is prescribed for $c_i(q)$ when $i\notin t$ .

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