Mixed-state tightness and failure of the support-projector choice

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.deterministicMixedTightness

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

prove2quantum

Let $\rho^{(1/2)}$ be the equal mixture of the three normalized qutrit vectors $(|01\rangle+|10\rangle)/\sqrt2$ , $(|02\rangle+|20\rangle)/\sqrt2$ , and $(|12\rangle+|21\rangle)/\sqrt2$ . Let $P$ be its support projector. With $E_1$ the one-copy exact positive-real-target PPT rate and $E_{\Gamma,0}$ its regularization, one has

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

Moreover, $\|T_B(P)\|_\infty=1$ , so the projector lower bound is $-\log_2\|T_B(P)\|_\infty=0<E_1(\rho^{(1/2)})$ . This genuinely mixed example makes the first three comparison inequalities equalities. LOCC achievability remains open in the source.

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]

/-- Mixed-state coincidence and failure of the R=P choice, PDF p.5,
with values from Proposition 5 on p.4. No LOCC achievability is asserted. -/
theorem deterministicMixedTightness :
    oneCopyExact (rhoAlpha (1/2)) = Real.logb 2 (3/2) ∧
    exactRegularized (rhoAlpha (1/2)) = Real.logb 2 (3/2) ∧
    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) ∧
    complexSpectralNorm (partialTranspose (supportProjector (rhoAlpha (1/2)))) = 1 ∧
    -Real.logb 2 (complexSpectralNorm (partialTranspose (supportProjector (rhoAlpha (1/2))))) = 0 ∧
    0 < oneCopyExact (rhoAlpha (1/2)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 5, Unnumbered result: mixed-state coincidence and failure of the projector choice

Read-back

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

On $\mathbb C^3\otimes\mathbb C^3$ , with standard basis $|ij\rangle$ , define $\rho=\tfrac16\sum_{i<j}(|ij\rangle+|ji\rangle)(\langle ij|+\langle ji|)$ , and let $P_\rho$ be the orthogonal projector onto its range. 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}}$ denote the Euclidean operator norm. Define $F_X(k)$ as 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$ , where $\preceq$ denotes positive semidefinite difference. Put $D(X)=\sup\{\log_2 k:k\in\mathbb R,\ k>0,\ F_X(k)=1\}$ , $D_{\mathrm{reg}}(X)=\sup_{m\ge1}D(X^{\otimes m})/m$ , and $\Gamma(X)=\sup\{r\in\mathbb R:F_{X^{\otimes n}}(2^{nr})\to1\}$ , without restricting $r$ to be nonnegative; tensor powers are defined entrywise by products, with zeroth power the scalar $1$ . Set $W(X)=\log_2\sup_R\operatorname{Re}\operatorname{tr}(X^\Gamma R)$ , where $R$ is Hermitian, $\|R\|_{\mathrm{op}}\le1$ , and $R^\Gamma\succeq0$ , and set $N(X)=\log_2\|X^\Gamma\|_1$ . All these suprema are real-valued. Then

D(\rho)=D_{\mathrm{reg}}(\rho)=\Gamma(\rho)=W(\rho)=\log_2\tfrac32,\qquad N(\rho)=\log_2\tfrac53,\qquad \log_2\tfrac32<\log_2\tfrac53,

and additionally

\|P_\rho^\Gamma\|_{\mathrm{op}}=1,\qquad -\log_2\|P_\rho^\Gamma\|_{\mathrm{op}}=0,\qquad 0<D(\rho).

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