Corollary 5: nonzero rays I and II are not entropic

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.rays_not_entropic

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)$ . In the coordinate order $(A,B,C,D,AB,AC,AD,BC,BD,CD,ABC,ABD,ACD,BCD,ABCD)$ , define the two formal entropy vectors by

v_1=(3,3,2,2,4,3,3,3,3,4,4,4,3,3,2),\qquad v_2=(3,3,3,3,4,4,4,4,4,6,5,5,5,5,2).

Set the empty coordinate to zero. Mutual information and conditional mutual information of these formal vectors mean the corresponding linear combinations of their coordinates. For every $t>0$ ,

(S(X))_{X\ne\varnothing}\notin\{t v_1,t v_2\}.

Both positive rays satisfy all basic inequalities and the three constraints $I(A;C\mid B)=I(B;C\mid A)=I(A;B\mid D)=0$ , but have $I(C;D)<I(C;AB)$ , so they lie in the slice removed by the new inequality within that constrained face. This excludes exact finite-dimensional realization, with no assertion about approximating these rays by entropic vectors.

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, Corollary 5: neither nonzero ray is exactly entropic in finite
systems. The zero endpoint is excluded, and no assertion about limit points is made. -/
theorem rays_not_entropic (q : FourPartyState) (t : ℝ) (ht : 0 < t) :
    (¬ ((∀ s, fourPartyEntropyBits q s = t * rayOne s) ∨ (∀ s, fourPartyEntropyBits q s = t * rayTwo s))) ∧
    (∀ h ∈ ({rayOne, rayTwo} : Set (Finset (Fin 4) → ℝ)),
      BasicInequalities (fun s => t * h s) ∧ Constraints (fun s => t * h s) ∧
      mutualValue (fun s => t * h s) C D < mutualValue (fun s => t * h s) 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. 6, Corollary 5

Read-back

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

Let $q$ be any four-party state, 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\}$ . For $s\subseteq\Omega$ , put $H_s^q=-\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$ . Define real functions $r_1,r_2$ on these subsets using the mask $m(s)=\sum_{i\in s}2^i$ :

\begin{array}{c|rrrrrrrrrrrrrrrr} m(s)&0&1&2&3&4&5&6&7&8&9&10&11&12&13&14&15\\ \hline r_1(s)&0&3&3&4&2&3&3&4&2&3&3&4&4&3&3&2\\ r_2(s)&0&3&3&4&3&4&4&5&3&4&4&5&6&5&5&2 \end{array}

Let $A,B,C,D$ be the fixed subsets of $\Omega$ referenced in the declaration, whose elements are not supplied, and use concatenated subscripts for unions. For every real $t>0$ , neither $H_s^q=t\,r_1(s)$ for every subset $s$ , nor $H_s^q=t\,r_2(s)$ for every subset $s$ . Moreover, for each $r\in\{r_1,r_2\}$ , the function $F_s=t\,r(s)$ satisfies all of

\begin{gathered} F_\varnothing=0,\qquad F_x\ge0\quad\text{for every }x\subseteq\Omega,\\ F_{x\cup y}-F_y+F_x\ge0 \quad\text{for every disjoint }x,y,\\ F_{z\cup x}-F_x+F_{z\cup y}-F_y\ge0 \quad\text{for every pairwise disjoint }x,y,z,\\ F_x+F_y-F_{x\cup y}\ge0 \quad\text{for every disjoint }x,y,\\ F_{x\cup y}+F_{y\cup z}-F_{x\cup y\cup z}-F_y\ge0 \quad\text{for every pairwise disjoint }x,z,y,\\ F_{AB}+F_{BC}-F_{ABC}-F_B=0,\qquad F_{AB}+F_{AC}-F_{ABC}-F_A=0,\qquad F_{AD}+F_{BD}-F_{ABD}-F_D=0,\\ F_C+F_D-F_{CD}<F_C+F_{AB}-F_{ABC}. \end{gathered}

All subset quantifiers include empty subsets.

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