Prove2Me

Lemma 19: separability threshold for compressed Werner states

Open
QAlgorithms.Papers.Independent.Intakethird100.P19.werner_compressions

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

prove2quantum

All Hilbert spaces are finite-dimensional complex spaces with fixed product bases and positive local dimensions. States are positive semidefinite operators of trace one; pure kets have norm one. Let 2≤k<d2\le k<d and −(d+1)≤β≤d−1-(d+1)\le\beta\le d-1. Write FdF_d for the swap operator and

ρd(β)=Id2−β+1dFdd2−(β+1).\rho_d(\beta)=\frac{I_{d^2}-\frac{\beta+1}{d}F_d}{d^2-(\beta+1)}.

Then (P⊗Q)ρd(β)(P⊗Q)†(P\otimes Q)\rho_d(\beta)(P\otimes Q)^\dagger belongs to the separable positive cone for every pair of coisometries P,Q:Cd→CkP,Q:\mathbb C^d\to\mathbb C^k if and only if

β≤d−kk.\beta\le\frac{d-k}{k}.

Compressed operators need not be normalized and may be zero.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P19
Formal statement
noncomputable section

open QAlgorithms QAlgorithms.Entanglement Filter

open scoped Matrix ComplexOrder ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P19

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P19 (Bip)

open QAlgorithms.Papers.Independent.Information100.P69 (CP)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower SupportIncluded)

open QAlgorithms.Papers.Independent.Dependency50.P19 (epr)

/-- Lemma 19, PDF pp.21-22: all coisometry compressions of the Werner
state are separable exactly at the stated threshold. Outputs are not normalized. -/
theorem werner_compressions {k d : ℕ} (hk : 2 ≤ k) (hkd : k < d)
    (beta : ℝ) (hlo : -((d : ℝ) + 1) ≤ beta) (hhi : beta ≤ (d : ℝ) - 1) :
    (∀ P Q : Matrix (Fin k) (Fin d) ℂ, Coisometry P → Coisometry Q →
      IsSeparablePositive (localCoisometryCompression P Q (betaWernerState d beta))) ↔
        beta ≤ ((d : ℝ) - k) / k := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end
Source
Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 21, Lemma 19
Read-back

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

For natural numbers 2≤k<d2\le k<d and a real number β\beta satisfying −d−1≤β≤d−1-d-1\le\beta\le d-1, define the swap operator Fd∣i,j⟩=∣j,i⟩F_d|i,j\rangle=|j,i\rangle and

Wd,β=Id2−β+1dFdd2−β−1.W_{d,\beta}=\frac{I_{d^2}-\frac{\beta+1}{d}F_d}{d^2-\beta-1}.

Then every pair P,Q∈Ck×dP,Q\in\mathbb C^{k\times d} with PP†=QQ†=IkPP^\dagger=QQ^\dagger=I_k has

(P⊗Q)Wd,β(P⊗Q)†(P\otimes Q)W_{d,\beta}(P\otimes Q)^\dagger

separable positive across Ck:Ck\mathbb C^k:\mathbb C^k if and only if

β≤d−kk.\beta\le\frac{d-k}{k}.

Here separable positive means expressible as a finite sum ∑jwjAj⊗Bj\sum_j w_jA_j\otimes B_j, where wj≥0w_j\ge0 and the factors are positive semidefinite matrices of trace 11; there is no requirement that the weights sum to 11, and the empty sum is permitted. The dimensional hypotheses imply d≥3d\ge3, so the displayed denominators are nonzero throughout the specified parameter range.

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