Exact entanglement of the qutrit antisymmetric state

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.antisymmetricValues

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

prove2quantum

Let $F$ be the swap operator on $\mathbb C^3\otimes\mathbb C^3$ , defined by $F|ij\rangle=|ji\rangle$ , and define the normalized antisymmetric state $\sigma_3=(I-F)/6$ . Then

E_\Gamma(\sigma_3)=E_W(\sigma_3)=E_N(\sigma_3)=\log_2(5/3).

Here $E_\Gamma$ is the vanishing-error PPT rate, $E_W$ is the logarithm of SDP (7), and $E_N$ is logarithmic negativity. This contrasts with the symmetric-support example in Proposition 5.

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]

/-- Remark, PDF p.4: exact PPT entanglement values of the constructed
normalized qutrit antisymmetric state. -/
theorem antisymmetricValues :
    IsDensityMatrix qutritAntisymmetricState ∧
    entanglementGamma qutritAntisymmetricState = Real.logb 2 (5/3) ∧
    entanglementW qutritAntisymmetricState = Real.logb 2 (5/3) ∧
    entanglementN qutritAntisymmetricState = 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, Unnumbered Remark: exact entanglement of the normalized qutrit antisymmetric state

Read-back

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

Let $S$ be the swap matrix on $\mathbb C^3\otimes\mathbb C^3$ , defined by $S|ij\rangle=|ji\rangle$ , and put $\rho_-=(I-S)/6$ . For a bipartite matrix $X$ , define $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , and let $\|\cdot\|_{\mathrm{op}}$ be the Euclidean operator norm. Let $F_X(k)$ be the real supremum of $\operatorname{Re}\operatorname{tr}(XQ)$ over $Q$ satisfying $k>0$ , $0\preceq Q\preceq I$ , and $-k^{-1}I\preceq Q^\Gamma\preceq k^{-1}I$ , with $\preceq$ denoting positive semidefinite difference. Let $\Gamma(X)$ be the real supremum of all real $r$ , without a nonnegativity restriction, such that $F_{X^{\otimes n}}(2^{nr})\to1$ ; the zeroth tensor power is the scalar $1$ . Set $W(X)=\log_2\sup_R\operatorname{Re}\operatorname{tr}(X^\Gamma R)$ , with $R$ Hermitian, $\|R\|_{\mathrm{op}}\le1$ , and $R^\Gamma\succeq0$ , and set $N(X)=\log_2\|X^\Gamma\|_1$ . Then $\rho_-$ is positive semidefinite with trace $1$ , and

\Gamma(\rho_-)=W(\rho_-)=N(\rho_-)=\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