Definitions for A new inequality for the von Neumann entropy

Definition

QAlgorithms_Papers_Independent_Intakethird100_P97

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

prove2quantum

The objects the formalized statements of A new inequality for the von Neumann entropy (arXiv:quant-ph/0406162) are stated in. Each was checked against the paper by a blind read-back and a moderator.

FullRegister: PDF pp.2–3: the complete tensor basis, with A,B,C,D numbered 0,1,2,3.
FourPartyState: PDF pp.1–3: a normalized finite-dimensional four-party complex density operator. Dimension one is allowed, dimension zero is excluded, and no purity is assumed.
fourPartyReduction: PDF p.2: the actual subsystem partial trace of the same joint matrix. This is a coordinate adapter to the frozen traceRight, allowing unequal local finite dimensions. Its empty subsystem has a singleton basis.
fourPartyEntropyBits: PDF pp.1–2: base-two von Neumann entropy of the actual marginal, with 0 log 0 = 0.
entropyDifference: PDF p.2: conditional entropy S(X|Y) = S(XY)-S(Y). Applications use disjoint groups of factors.
mutualValue: PDF p.2: mutual information of disjoint groups of factors.
conditionalMutualValue: PDF p.2: I(X;Z|Y), with the conditioning group as the last argument. All applications to states use three pairwise disjoint groups.
Constraints: PDF p.3, Theorem 1: the three SSA saturation constraints; no block or recovery structure obtained in the proof is included as an assumption.
constraintValue: PDF p.5, Remark 3: individual constraints in the order ABC, CAB, ADB.
subsetMask: PDF p.6, table: the mask uses A as bit 0, B as bit 1, C as bit 2, D as bit 3. For every subset of these four labels the mask is between 0 and 15.
rayOne: PDF p.6: ray I, in binary-mask order, with empty entry zero. The fallback cannot occur for a subset of Fin 4. This is a formal entropy vector, not a state.
rayTwo: PDF p.6: ray II, in binary-mask order, with empty entry zero.
BasicInequalities: PDF p.2, all five basic quantum inequalities, for every disjoint subsystem grouping (including empty groups). This is a linear constraint predicate on formal entropy vectors, not a claim that such a vector is entropic.
marginalAB3: PDF p.5, Remark 4: actual AB marginal of a tripartite state, tensor-ordered A,(B,C).
marginalAC3: PDF p.5, Remark 4: actual AC marginal of the same tripartite state.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Defs_Ensemble
import Definitions.Def_QAlgorithms_Defs_Measurement
import Definitions.Def_QAlgorithms_Defs_BipartiteSeparability

/-!
arXiv:quant-ph/0406162v1, Linden and Winter, PDF pp.1–7.
All entropies are in bits. Local dimensions are arbitrary positive integers.
Proposition 2 is recorded as reuse in items.json; Remark 3's unspecified generic
family and Conjecture 6 are deferred. No imported paper module is required.
-/

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P97

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF pp.2–3: the complete tensor basis, with A,B,C,D numbered 0,1,2,3. -/
abbrev FullRegister (dims : Fin 4 → ℕ) := (i : Fin 4) → Fin (dims i)

/-- PDF pp.1–3: a normalized finite-dimensional four-party complex density operator.
Dimension one is allowed, dimension zero is excluded, and no purity is assumed. -/
structure FourPartyState where
  dims : Fin 4 → ℕ
  dims_pos : ∀ i, 0 < dims i
  rho : Matrix (FullRegister dims) (FullRegister dims) ℂ
  density : IsDensityMatrix rho

/-- PDF p.2: the actual subsystem partial trace of the same joint matrix.
This is a coordinate adapter to the frozen traceRight, allowing unequal local
finite dimensions. Its empty subsystem has a singleton basis. -/
def fourPartyReduction {dims : Fin 4 → ℕ}
    (rho : Matrix (FullRegister dims) (FullRegister dims) ℂ) (s : Finset (Fin 4)) :
    Matrix ((i : {i : Fin 4 // i ∈ s}) → Fin (dims i.1))
      ((i : {i : Fin 4 // i ∈ s}) → Fin (dims i.1)) ℂ :=
  let join : (((i : {i : Fin 4 // i ∈ s}) → Fin (dims i.1)) ×
      ((i : {i : Fin 4 // i ∉ s}) → Fin (dims i.1))) → FullRegister dims :=
    fun x i => if h : i ∈ s then x.1 ⟨i, h⟩ else x.2 ⟨i, h⟩
  traceRight (fun x y => rho (join x) (join y))

/-- PDF pp.1–2: base-two von Neumann entropy of the actual marginal, with 0 log 0 = 0. -/
def fourPartyEntropyBits (q : FourPartyState) (s : Finset (Fin 4)) : ℝ :=
  vnEntropy (fourPartyReduction q.rho s)

/-- PDF p.2: conditional entropy S(X|Y) = S(XY)-S(Y).
Applications use disjoint groups of factors. -/
def entropyDifference (h : Finset (Fin 4) → ℝ) (x y : Finset (Fin 4)) : ℝ :=
  h (x ∪ y) - h y

/-- PDF p.2: mutual information of disjoint groups of factors. -/
def mutualValue (h : Finset (Fin 4) → ℝ) (x y : Finset (Fin 4)) : ℝ :=
  h x + h y - h (x ∪ y)

/-- PDF p.2: I(X;Z|Y), with the conditioning group as the last argument.
All applications to states use three pairwise disjoint groups. -/
def conditionalMutualValue (h : Finset (Fin 4) → ℝ) (x z y : Finset (Fin 4)) : ℝ :=
  h (x ∪ y) + h (y ∪ z) - h (x ∪ y ∪ z) - h y

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: the three SSA saturation constraints; no block or recovery
structure obtained in the proof is included as an assumption. -/
def Constraints (h : Finset (Fin 4) → ℝ) : Prop :=
  conditionalMutualValue h A C B = 0 ∧ conditionalMutualValue h B C A = 0 ∧ conditionalMutualValue h A B D = 0

/-- PDF p.5, Remark 3: individual constraints in the order ABC, CAB, ADB. -/
def constraintValue (h : Finset (Fin 4) → ℝ) (i : Fin 3) : ℝ :=
  if i = 0 then conditionalMutualValue h A C B else if i = 1 then conditionalMutualValue h B C A else conditionalMutualValue h A B D

/-- PDF p.6, table: the mask uses A as bit 0, B as bit 1, C as bit 2, D as bit 3.
For every subset of these four labels the mask is between 0 and 15. -/
def subsetMask (s : Finset (Fin 4)) : ℕ := ∑ i ∈ s, 2 ^ i.val

/-- PDF p.6: ray I, in binary-mask order, with empty entry zero. The fallback
cannot occur for a subset of Fin 4. This is a formal entropy vector, not a state. -/
def rayOne (s : Finset (Fin 4)) : ℝ :=
  ([0, 3, 3, 4, 2, 3, 3, 4, 2, 3, 3, 4, 4, 3, 3, 2] : List ℝ).getD (subsetMask s) 0

/-- PDF p.6: ray II, in binary-mask order, with empty entry zero. -/
def rayTwo (s : Finset (Fin 4)) : ℝ :=
  ([0, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 6, 5, 5, 2] : List ℝ).getD (subsetMask s) 0

/-- PDF p.2, all five basic quantum inequalities, for every disjoint subsystem
grouping (including empty groups). This is a linear constraint predicate on formal
entropy vectors, not a claim that such a vector is entropic. -/
def BasicInequalities (h : Finset (Fin 4) → ℝ) : Prop :=
  h ∅ = 0 ∧
  (∀ x, 0 ≤ h x) ∧
  (∀ x y, Disjoint x y → 0 ≤ entropyDifference h x y + h x) ∧
  (∀ x y z, Disjoint x y → Disjoint x z → Disjoint y z →
    0 ≤ entropyDifference h z x + entropyDifference h z y) ∧
  (∀ x y, Disjoint x y → 0 ≤ mutualValue h x y) ∧
  (∀ x z y, Disjoint x z → Disjoint x y → Disjoint z y → 0 ≤ conditionalMutualValue h x z y)

/-- PDF p.5, Remark 4: actual AB marginal of a tripartite state, tensor-ordered A,(B,C). -/
def marginalAB3 {X Y Z : Type*} [Fintype Z]
    (rho : Matrix (X × (Y × Z)) (X × (Y × Z)) ℂ) : Matrix (X × Y) (X × Y) ℂ :=
  fun x y => ∑ z, rho (x.1, (x.2, z)) (y.1, (y.2, z))

/-- PDF p.5, Remark 4: actual AC marginal of the same tripartite state. -/
def marginalAC3 {X Y Z : Type*} [Fintype Y]
    (rho : Matrix (X × (Y × Z)) (X × (Y × Z)) ℂ) : Matrix (X × Z) (X × Z) ℂ :=
  fun x y => ∑ z, rho (x.1, (z, x.2)) (y.1, (z, y.2))

/-- Sanity: tracing a zero matrix yields a zero matrix, not a normalized state. -/
example {dims : Fin 4 → ℕ} (s : Finset (Fin 4)) :
    fourPartyReduction (0 : Matrix (FullRegister dims) (FullRegister dims) ℂ) s = 0 := by
  funext x y
  simp [fourPartyReduction, traceRight]

/-- Sanity: the conditional-entropy expression is the source's entropy difference. -/
example (h : Finset (Fin 4) → ℝ) : entropyDifference h A C = h (A ∪ C) - h C := rfl

/-- Sanity: ray I's C and CD entries reproduce the printed table. -/
example : rayOne C = 2 ∧ rayOne (C ∪ D) = 4 := by
  simp [rayOne, subsetMask, Finset.sum_insert, Finset.sum_singleton]
  <;> norm_num

/-- Sanity: ray II's ABC and total entries reproduce the printed table. -/
example : rayTwo (A ∪ B ∪ C) = 5 ∧ rayTwo (A ∪ B ∪ C ∪ D) = 2 := by
  simp [rayTwo, subsetMask, Finset.sum_insert, Finset.sum_singleton]
  <;> norm_num

end QAlgorithms.Papers.Independent.Intakethird100.P97

Source

A new inequality for the von Neumann entropy, arXiv:quant-ph/0406162v1, https://arxiv.org/abs/quant-ph/0406162v1

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P97.BasicInequalities`

For any real-valued function $h$ on the subsets of $\Omega=\{0,1,2,3\}$ , this predicate means that all the following conditions hold:

\begin{gathered} h(\varnothing)=0,\qquad h(x)\ge 0\quad\text{for every }x\subseteq\Omega,\\ h(x\cup y)-h(y)+h(x)\ge0 \quad\text{whenever }x\cap y=\varnothing,\\ h(z\cup x)-h(x)+h(z\cup y)-h(y)\ge0 \quad\text{whenever }x,y,z\text{ are pairwise disjoint},\\ h(x)+h(y)-h(x\cup y)\ge0 \quad\text{whenever }x\cap y=\varnothing,\\ h(x\cup y)+h(y\cup z)-h(x\cup y\cup z)-h(y)\ge0 \quad\text{whenever }x,z,y\text{ are pairwise disjoint}. \end{gathered}

Every subset variable ranges over all subsets of $\Omega$ , including the empty set. No assumption that $h$ arises from a state or an entropy is part of this definition.

`QAlgorithms.Papers.Independent.Intakethird100.P97.Constraints`

For any real-valued function $h$ on the subsets of $\{0,1,2,3\}$ , this defines the conjunction of the three equalities

\begin{aligned} h(A\cup B)+h(B\cup C)-h(A\cup B\cup C)-h(B)&=0,\\ h(B\cup A)+h(A\cup C)-h(B\cup A\cup C)-h(A)&=0,\\ h(A\cup D)+h(D\cup B)-h(A\cup D\cup B)-h(D)&=0. \end{aligned}

Here $A,B,C,D$ are the subset symbols referenced in the declaration; their elements are not specified in the supplied declarations. No additional condition on $h$ is included.

`QAlgorithms.Papers.Independent.Intakethird100.P97.FourPartyState`

A four-party state consists of dimensions $d(i)\in\mathbb N$ for each $i\in\{0,1,2,3\}$ , a proof that every $d(i)>0$ , and a complex matrix $\rho$ whose rows and columns are indexed by assignments $u$ with $0\le u(i)<d(i)$ , together with the requirements that $\rho$ is positive semidefinite and $\operatorname{tr}\rho=1$ . Dimensions equal to $1$ are allowed.

`QAlgorithms.Papers.Independent.Intakethird100.P97.FullRegister`

For any function $d:\{0,1,2,3\}\to\mathbb N$ , this defines the full register as the set of assignments

\prod_{i=0}^{3}\{0,\ldots,d(i)-1\}.

Thus an assignment chooses one index below $d(i)$ for each of the four parties. No positivity condition is imposed here: if any $d(i)=0$ , the full register is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P97.conditionalMutualValue`

For any real-valued function $h$ on the subsets of $\{0,1,2,3\}$ and any three such subsets, supplied in the order $x,z,y$ , this defines

h(x\cup y)+h(y\cup z)-h(x\cup y\cup z)-h(y).

There are no assumptions on $h$ , and the subsets may overlap or be empty.

`QAlgorithms.Papers.Independent.Intakethird100.P97.constraintValue`

For any real-valued function $h$ on the subsets of $\{0,1,2,3\}$ and any index $i\in\{0,1,2\}$ , this defines

\begin{cases} h(A\cup B)+h(B\cup C)-h(A\cup B\cup C)-h(B),&i=0,\\ h(B\cup A)+h(A\cup C)-h(B\cup A\cup C)-h(A),&i=1,\\ h(A\cup D)+h(D\cup B)-h(A\cup D\cup B)-h(D),&i=2. \end{cases}

Here $A,B,C,D$ are the subset symbols referenced in the declaration; their elements are not specified in the supplied declarations. No assumptions are imposed on $h$ .

`QAlgorithms.Papers.Independent.Intakethird100.P97.entropyDifference`

For any real-valued function $h$ on the subsets of $\{0,1,2,3\}$ and any two such subsets $x,y$ , this defines

h(x\cup y)-h(y).

There are no assumptions on $h$ , and the subsets may overlap or be empty; in particular, the value is $0$ whenever $x\subseteq y$ .

`QAlgorithms.Papers.Independent.Intakethird100.P97.fourPartyEntropyBits`

For a four-party state $q$ , consisting of positive dimensions $d(0),\ldots,d(3)$ and a positive semidefinite complex matrix $\rho$ of trace $1$ indexed by full assignments, and any subset $s\subseteq\{0,1,2,3\}$ , this defines the real number

-\operatorname{Re}\operatorname{tr}\bigl(f(\rho_s)\bigr), \qquad f(t)=t\log_2 t,

where $f$ is applied by continuous functional calculus and

\rho_s(u,v)=\sum_w\rho(u\sqcup w,v\sqcup w)

sums over assignments on the parties outside $s$ . The function has $f(0)=0$ under the total logarithm convention used here. The subset $s$ may be empty or contain all four parties.

`QAlgorithms.Papers.Independent.Intakethird100.P97.fourPartyReduction`

For any dimensions $d:\{0,1,2,3\}\to\mathbb N$ , any complex matrix $\rho$ indexed by full assignments $u(i)<d(i)$ , and any subset $s\subseteq\{0,1,2,3\}$ , this defines a complex matrix $\rho_s$ indexed by assignments on $s$ , with entries

\rho_s(u,v)=\sum_{w\in\prod_{i\notin s}\{0,\ldots,d(i)-1\}} \rho(u\sqcup w,v\sqcup w),

where $u\sqcup w$ uses $u$ on $s$ and $w$ outside $s$ . No positivity, trace, or positive-dimension hypothesis is imposed. Empty sums are zero, while an assignment on an empty set of parties has exactly one possible value. In particular, $s=\varnothing$ gives a one-by-one matrix with entry $\operatorname{tr}\rho$ , and taking all four parties gives $\rho$ with its indices identified in the indicated way.

`QAlgorithms.Papers.Independent.Intakethird100.P97.marginalAB3`

For arbitrary types $X,Y,Z$ , with a specified finite enumeration of $Z$ , and any complex matrix $\rho$ whose row and column indices belong to $X\times(Y\times Z)$ , this defines a matrix on $X\times Y$ by

\bigl(\operatorname{marginalAB3}(\rho)\bigr)_{(a,b),(a',b')} = \sum_{c\in Z} \rho_{(a,(b,c)),(a',(b',c))} \qquad(a,a'\in X,\ b,b'\in Y).

Neither $X$ nor $Y$ is required to be finite or nonempty, and $\rho$ is not required to be positive semidefinite or normalized. The finite type $Z$ may be empty, in which case every entry of the resulting matrix is zero.

`QAlgorithms.Papers.Independent.Intakethird100.P97.marginalAC3`

For arbitrary types $X,Y,Z$ , with a specified finite enumeration of $Y$ , and any complex matrix $\rho$ whose row and column indices belong to $X\times(Y\times Z)$ , this defines a matrix on $X\times Z$ by

\bigl(\operatorname{marginalAC3}(\rho)\bigr)_{(a,c),(a',c')} = \sum_{b\in Y} \rho_{(a,(b,c)),(a',(b,c'))} \qquad(a,a'\in X,\ c,c'\in Z).

Neither $X$ nor $Z$ is required to be finite or nonempty, and $\rho$ is not required to be positive semidefinite or normalized. The finite type $Y$ may be empty, in which case every entry of the resulting matrix is zero.

`QAlgorithms.Papers.Independent.Intakethird100.P97.mutualValue`

For any real-valued function $h$ on the subsets of $\{0,1,2,3\}$ and any two such subsets $x,y$ , this defines

h(x)+h(y)-h(x\cup y).

There are no assumptions on $h$ or disjointness requirements on $x,y$ . Empty subsets are included; if either subset is empty, the value is $h(\varnothing)$ .

`QAlgorithms.Papers.Independent.Intakethird100.P97.rayOne`

For any subset $s\subseteq\{0,1,2,3\}$ , let $m=\sum_{i\in s}2^i$ . This defines the real number at zero-based position $m$ in the list

[0,3,3,4,2,3,3,4,2,3,3,4,4,3,3,2].

The lookup specifies a default value of $0$ for an out-of-range position, although every permitted subset gives $0\le m\le15$ , so that default is never used. In particular, the empty subset has value $0$ and the full subset has value $2$ .

`QAlgorithms.Papers.Independent.Intakethird100.P97.rayTwo`

For any subset $s\subseteq\{0,1,2,3\}$ , let $m=\sum_{i\in s}2^i$ . This defines the real number at zero-based position $m$ in the list

[0,3,3,4,3,4,4,5,3,4,4,5,6,5,5,2].

`QAlgorithms.Papers.Independent.Intakethird100.P97.subsetMask`

For any subset $s\subseteq\{0,1,2,3\}$ , this defines the natural number

\sum_{i\in s}2^i.

The empty subset has value $0$ , and the full subset has value $15$ ; every possible value lies between $0$ and $15$ , inclusive.

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