Exact projective steering threshold of Werner states

Open

QAlgorithms.Papers.Independent.Intakethird100.P62.werner_threshold

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

prove2quantum

Let $d\ge2$ be an integer and let $\eta\in\mathbb R$ make the following operator a density matrix on $\mathbb C^d\otimes\mathbb C^d$ :

W_d^\eta=\frac{d-1+\eta}{d-1}\frac{I}{d^2}-\frac{\eta}{d-1}\frac{F}{d}, \qquad F(u\otimes v)=v\otimes u.

The physical parameter interval is $-(d-1)/(d+1)\le\eta\le1$ . With all local projective measurements allowed, and arbitrary mixed or pure hidden quantum states in a common continuous LHS ensemble,

W_d^\eta\text{ is steerable from Alice to Bob} \quad\Longleftrightarrow\quad \eta>1-\frac1d.

Equality is nonsteerable. This identifies the exact projective steering boundary, including the physical negative-parameter range.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P62

Formal statement

noncomputable section

open MeasureTheory

open scoped BigOperators Matrix.Norms.Elementwise

open QAlgorithms.Papers.Independent.Information100.P60 (Mat)

namespace QAlgorithms.Papers.Independent.Intakethird100.P62

attribute [local instance] Classical.propDecidable Classical.decEq

attribute [local instance] QAlgorithms.Papers.Independent.Intakethird100.P62.matrixContinuousENorm

attribute [local instance] QAlgorithms.Papers.Independent.Intakethird100.P62.matrixMeasurable

/-- arXiv:quant-ph/0612147v3, PDF p.3, (8)--(11) and the definition of
eta_steer above (9). The iff uses all projective observables; equality is
nonsteerable. The defective auxiliary single-outcome (10) is not assumed. -/
theorem werner_threshold (d : ℕ) (hd : 2 ≤ d) (eta : ℝ)
    (hphysical : IsDensityMatrix (wernerEta d eta)) :
    Steerable (wernerEta d eta) ↔ 1 - 1 / (d : ℝ) < eta := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P62

end

Source

Steering, Entanglement, Nonlocality, and the EPR Paradox, arXiv:quant-ph/0612147v3, PDF p. 3, (i) Werner States: exact projective steering threshold

Read-back

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

For every natural number $d\ge2$ and every real $\eta$ , set $p=(d-1+(d+1)\eta)/(2d)$ , let $F(u\otimes v)=v\otimes u$ , put $P_+=(I+F)/2$ and $P_-=I-P_+$ , and define

W_{d,\eta}=\frac{2(1-p)}{d(d+1)}P_+ +\frac{2p}{d(d-1)}P_-.

Assume that $W_{d,\eta}$ is positive semidefinite and has trace $1$ . Then $W_{d,\eta}$ is steerable if and only if $1-1/d<\eta$ . Here steerability means that there do not exist a measurable space $\Omega$ , a probability measure $\mu$ , a measurable and $\mu$ -integrable family of density matrices $\sigma_\omega$ on $\mathbb C^d$ , and response functions $r_{A,x}(\omega)$ for every projective measurement $A=(A_x)_{x=0}^{d-1}$ , such that each response is measurable and nonnegative, $\sum_xr_{A,x}(\omega)=1$ for every $A,\omega$ , every $r_{A,x}\sigma$ is integrable, and

\operatorname{Tr}_1\!\bigl(W_{d,\eta}(A_x\otimes I_d)\bigr) =\int_\Omega r_{A,x}(\omega)\sigma_\omega\,d\mu(\omega).

These projective measurements consist of $d$ pairwise orthogonal Hermitian idempotents summing to $I_d$ , with zero projectors allowed, and $(\operatorname{Tr}_1 Z)_{u,v}=\sum_iZ_{(i,u),(i,v)}$ . No separate range restriction on $\eta$ is assumed beyond the density-matrix hypothesis; the strict inequality excludes equality at the stated threshold.

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