Section 4, unnumbered: independence from the basic inequalities

Open

QAlgorithms.Papers.Independent.Intakethird100.P97.independent_of_basic

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

prove2quantum

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. The basic inequalities mean entropy nonnegativity, Araki–Lieb $S(XY)-S(Y)+S(X)\ge0$ , weak monotonicity $S(Z\mid X)+S(Z\mid Y)\ge0$ , mutual-information nonnegativity, and conditional-mutual-information nonnegativity, for every disjoint grouping of the four factors (empty groups included). For each $j\in\{1,2\}$ and every $t>0$ , the formal vector $h=t v_j$ satisfies

h\text{ satisfies all basic inequalities},\quad I_h(A;C\mid B)=I_h(B;C\mid A)=I_h(A;B\mid D)=0,\quad I_h(C;D)<I_h(C;AB).

These explicit countermodels establish that the constrained conclusion cannot follow from the basic linear inequalities and the three equalities alone.

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, §4: explicit linear countermodels to derivability from the basic
inequalities. Every positive multiple of either printed ray obeys all basic
inequalities and all three constraints but violates the new inequality. -/
theorem independent_of_basic :
    ∀ h ∈ ({rayOne, rayTwo} : Set (Finset (Fin 4) → ℝ)), ∀ t : ℝ, 0 < t →
      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, Section 4, unnumbered

Read-back

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

Let $\Omega=\{0,1,2,3\}$ , and define real-valued functions $r_1,r_2$ on its subsets by the mask $m(s)=\sum_{i\in s}2^i$ and the table

\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}

Here $A,B,C,D$ denote the fixed subsets of $\Omega$ referenced in the declaration; their elements are not specified in the supplied code. For every choice $r\in\{r_1,r_2\}$ and every real $t>0$ , put $F_s=t\,r(s)$ , with concatenated subscripts denoting unions. Then all the following conditions hold:

\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}

Every subset quantifier includes the empty set; no state is quantified in this assertion.

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