Strict qutrit mixed-state family and an exact value

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.qutritFamily

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

prove2quantum

For $0<\alpha\le\tfrac12$ , define the qutrit state $\rho^{(\alpha)}=\tfrac13\sum_{m=0}^2|\psi_m\rangle\langle\psi_m|$ , where $\psi_0=\sqrt\alpha|01\rangle+\sqrt{1-\alpha}|10\rangle$ , $\psi_1=\sqrt\alpha|02\rangle+\sqrt{1-\alpha}|20\rangle$ , and $\psi_2=\sqrt\alpha|12\rangle+\sqrt{1-\alpha}|21\rangle$ . These are normalized states, and the PPT distillable rate $E_\Gamma$ , SDP measure $E_W$ , and logarithmic negativity $E_N$ satisfy

E_\Gamma(\rho^{(\alpha)})\le E_W(\rho^{(\alpha)})\le\log_2\bigl(1+\sqrt{\alpha(1-\alpha)}\bigr)<E_N(\rho^{(\alpha)})=\log_2\bigl(1+\tfrac43\sqrt{\alpha(1-\alpha)}\bigr).

In particular,

E_\Gamma(\rho^{(1/2)})=E_W(\rho^{(1/2)})=\log_2(3/2)<\log_2(5/3)=E_N(\rho^{(1/2)}).

This gives a strict improvement on the negativity bound. The upper bound for general $\alpha$ is not asserted to be attained.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P83

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P83

open QAlgorithms.Papers.Independent.Support50.P11 (Loewner)

open QAlgorithms.Papers.Independent.Dependency50.P32 (partialTranspose)

open QAlgorithms.Papers.Independent.Information100.P34 (supportProjector)

variable {A B C D : Type*}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

/-- Proposition 5 and its explicit bounds (11)–(12), PDF p.4.
The bound (12) is not asserted to be an equality for general alpha. -/
theorem qutritFamily (alpha : ℝ) (hpos : 0 < alpha) (hhalf : alpha ≤ 1/2) :
    IsDensityMatrix (rhoAlpha alpha) ∧
    entanglementGamma (rhoAlpha alpha) ≤ entanglementW (rhoAlpha alpha) ∧
    entanglementW (rhoAlpha alpha) ≤ Real.logb 2 (1 + Real.sqrt (alpha * (1-alpha))) ∧
    entanglementN (rhoAlpha alpha) = Real.logb 2 (1 + (4/3 : ℝ) * Real.sqrt (alpha * (1-alpha))) ∧
    entanglementW (rhoAlpha alpha) < entanglementN (rhoAlpha alpha) ∧
    entanglementGamma (rhoAlpha (1/2)) = Real.logb 2 (3/2) ∧
    entanglementW (rhoAlpha (1/2)) = Real.logb 2 (3/2) ∧
    entanglementN (rhoAlpha (1/2)) = Real.logb 2 (5/3) ∧
    Real.logb 2 (3/2) < Real.logb 2 (5/3) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 4, Proposition 5: strict mixed-state family and an exact value

Read-back

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

For every real $\alpha$ with $0<\alpha\le \tfrac12$ , let $|ij\rangle$ , $i,j\in\{0,1,2\}$ , be the standard basis of $\mathbb C^3\otimes\mathbb C^3$ , put $\psi_{ij}=\sqrt{\alpha}\,|ij\rangle+\sqrt{1-\alpha}\,|ji\rangle$ for $i<j$ , and define $\rho_\alpha=\tfrac13\sum_{i<j}|\psi_{ij}\rangle\langle\psi_{ij}|$ , where $|v\rangle\langle v|$ has entries $v_x\overline{v_y}$ . For a bipartite matrix $X$ , write $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , write $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , and let $\|X\|_{\mathrm{op}}$ be its Euclidean operator norm. Define $F_X(k)$ , for real $k$ , as the real supremum of $\operatorname{Re}\operatorname{tr}(XQ)$ over matrices satisfying $k>0$ , $0\preceq Q\preceq I$ , and $-k^{-1}I\preceq Q^\Gamma\preceq k^{-1}I$ , where $\preceq$ means that the difference is positive semidefinite. Define $\Gamma(X)$ as the real supremum of all $r\in\mathbb R$ such that $F_{X^{\otimes n}}(2^{nr})\to1$ as $n\to\infty$ ; there is no additional condition $r\ge0$ , and the tensor power at $n=0$ is the scalar $1$ . Define $W(X)=\log_2\sup_R\operatorname{Re}\operatorname{tr}(X^\Gamma R)$ , where $R$ ranges over Hermitian matrices with $\|R\|_{\mathrm{op}}\le1$ and $R^\Gamma\succeq0$ , and define $N(X)=\log_2\|X^\Gamma\|_1$ . Then $\rho_\alpha$ is positive semidefinite with trace $1$ , and

\Gamma(\rho_\alpha)\le W(\rho_\alpha) \le\log_2\!\left(1+\sqrt{\alpha(1-\alpha)}\right),\qquad N(\rho_\alpha)=\log_2\!\left(1+\tfrac43\sqrt{\alpha(1-\alpha)}\right),\qquad W(\rho_\alpha)<N(\rho_\alpha).

Moreover, including at the allowed endpoint $\alpha=\tfrac12$ ,

\Gamma(\rho_{1/2})=W(\rho_{1/2})=\log_2\tfrac32,\qquad N(\rho_{1/2})=\log_2\tfrac53,\qquad \log_2\tfrac32<\log_2\tfrac53.

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