Remark 3: strict and tight examples exist

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.strict_and_tight_examples

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)$ . There exists a state obeying $I(A;C\mid B)=I(B;C\mid A)=I(A;B\mid D)=0$ for which the inequality is strict, and there exists a state obeying the same constraints for which it is tight:

\exists\rho:\ I(C;D)>I(C;AB),\qquad \exists\sigma:\ I(C;D)=I(C;AB).

The two existential states may use different finite local dimensions. This demonstrates both behaviors within the constrained class.

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: both strictness and equality occur among states obeying
all three constraints. The witnesses may have different finite local dimensions. -/
theorem strict_and_tight_examples :
    (∃ q : FourPartyState, Constraints (fourPartyEntropyBits q) ∧
      mutualValue (fourPartyEntropyBits q) C (A ∪ B) < mutualValue (fourPartyEntropyBits q) C D) ∧
    (∃ q : FourPartyState, 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. 5, Remark 3

Read-back

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

A four-party state $q$ consists of positive natural-number dimensions $d_i$ , indexed by $\Omega=\{0,1,2,3\}$ , and a positive semidefinite complex matrix $\rho$ of trace $1$ on the register $\prod_i\{0,\ldots,d_i-1\}$ ; dimensions equal to $1$ are permitted. Define $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$ . Here $A,B,C,D$ are the fixed subsets of $\Omega$ referenced in the declaration, whose elements are not supplied, and concatenated subscripts denote unions. The theorem asserts both of the following existence statements, with the state chosen separately in each:

\begin{aligned} &\exists q:\quad H_{AB}^q+H_{BC}^q-H_{ABC}^q-H_B^q=0,\quad H_{AB}^q+H_{AC}^q-H_{ABC}^q-H_A^q=0,\quad H_{AD}^q+H_{BD}^q-H_{ABD}^q-H_D^q=0,\\[-2pt] &\hspace{55mm} H_C^q+H_{AB}^q-H_{ABC}^q < H_C^q+H_D^q-H_{CD}^q;\\[4pt] &\exists q:\quad H_{AB}^q+H_{BC}^q-H_{ABC}^q-H_B^q=0,\quad H_{AB}^q+H_{AC}^q-H_{ABC}^q-H_A^q=0,\quad H_{AD}^q+H_{BD}^q-H_{ABD}^q-H_D^q=0,\\[-2pt] &\hspace{55mm} H_C^q+H_{AB}^q-H_{ABC}^q = H_C^q+H_D^q-H_{CD}^q. \end{aligned}

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