Exact projective steering threshold of isotropic states

Open

QAlgorithms.Papers.Independent.Intakethird100.P62.isotropic_threshold

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

prove2quantum

Let $d\ge2$ be an integer, let $|\Phi_d\rangle=d^{-1/2}\sum_{j=1}^d|j\rangle\otimes|j\rangle$ , and let $\eta\in\mathbb R$ make $W_d^\eta=(1-\eta)I/d^2+\eta|\Phi_d\rangle\langle\Phi_d|$ a density operator. Equivalently, $-1/(d^2-1)\le\eta\le1$ . Write $H_d=\sum_{j=1}^d1/j$ for the finite harmonic number. Then, for all local projective measurements,

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

Equality is nonsteerable. The hidden ensemble is shared by all Alice settings and may contain arbitrary mixed states and continuous mixtures.

This gives the exact isotropic projective steering boundary. The accepted library's isotropic density is precisely Eq. (12).

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 pp.3--4, (12)--(15): exact isotropic
projective-steering threshold. The accepted isotropic density uses the same-index
maximally entangled vector from (12). No incorrect arbitrary-complex-basis
identity from (13), and no defective auxiliary bound (14), is assumed. -/
theorem isotropic_threshold (d : ℕ) (hd : 2 ≤ d) (eta : ℝ)
    (hphysical : IsDensityMatrix
      (QAlgorithms.Papers.Independent.Information100.P60.isotropic d eta)) :
    Steerable (QAlgorithms.Papers.Independent.Information100.P60.isotropic d eta) ↔
      ((harmonic d : ℝ) - 1) / ((d : ℝ) - 1) < 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, (ii) Isotropic 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$ , let $\Omega_d=d^{-1/2}\sum_{i=0}^{d-1}e_i\otimes e_i$ and

\rho_{d,\eta}=\eta\,\Omega_d\Omega_d^\ast+\frac{1-\eta}{d^2}I_{d^2}.

Assume that $\rho_{d,\eta}$ is positive semidefinite and has trace $1$ . Then $\rho_{d,\eta}$ is steerable if and only if

\frac{H_d-1}{d-1}<\eta, \qquad H_d=\sum_{j=1}^{d}\frac1j.

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(\rho_{d,\eta}(A_x\otimes I_d)\bigr) =\int_\Omega r_{A,x}(\omega)\sigma_\omega\,d\mu(\omega).

A projective measurement here consists 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; equality at the displayed threshold does not satisfy the strict inequality.

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