Formalize Open Quantum Problem #39: Steering bound for qubits and POVMs

### What is the conjecture

This is problem [#39](https://oqp.iqoqi.oeaw.ac.at/steering-bound-for-qubits-and-povms) in the community-maintained [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

Status: the core **two-qubit / arbitrary-POVM** version of this problem now appears to be solved. The OQP page still lists it as open, so the most natural formalization is probably the **resolved statement** for qubit Werner states together with the **remaining higher-dimensional extension** mentioned on the OQP page.

> **Problem (Open Quantum Problem #39: “Steering bound for qubits and POVMs”).**
> In steering, one asks whether the correlations of a bipartite state `ρ` can be explained by a classical hidden-variable model on Alice’s side together with genuine quantum states on Bob’s side.
> For the two-qubit Werner family
> `ρ_f = ((2-f) I + (2f-1) F)/6`,
> where `F` is the swap operator and `-1 ≤ f ≤ 1`,
> determine the critical value `f_s` such that the state admits such a model for all `f > f_s`, but is steerable for `f < f_s`.
> The question is whether allowing **general POVMs** on Alice’s side gives a strictly different threshold from allowing only **projective measurements**.

A standard formalization is in terms of **assemblages** and **local-hidden-state (LHS) models**:

* Alice and Bob share a bipartite state `ρ_AB ∈ D(C^2 ⊗ C^2)`.

* If Alice performs a POVM `M^x = {M_{a|x}}_a`, Bob’s corresponding subnormalized conditional states are
`σ_{a|x} = Tr_A[(M_{a|x} ⊗ I) ρ_AB]`.

* The state `ρ_AB` is **unsteerable from Alice to Bob** for a class of measurements `𝓕` iff there exist:
* a hidden-variable space `Λ`,
* a probability measure `μ` on `Λ`,
* quantum states `τ_λ ∈ D(C^2)` for Bob,
* response functions `p(a|x, λ)`,
such that for every measurement `x ∈ 𝓕` and outcome `a`,
`σ_{a|x} = ∫_Λ p(a|x, λ) τ_λ dμ(λ)`.

* In this problem, `𝓕` is either:
* all **projective qubit measurements** (`PVMs`), or
* all **qubit POVMs**.

It is also standard to write the same two-qubit Werner family as
`ρ_W(r) = r |Ψ^-⟩⟨Ψ^-| + (1-r) I/4`,
where `|Ψ^-⟩ = (|01⟩ - |10⟩)/√2`.
Using `F = I - 2|Ψ^-⟩⟨Ψ^-|`, one gets the parameter conversion
`r = (1 - 2f)/3`
and equivalently
`f = (1 - 3r)/2`.

Basic facts:

* The Werner state is **separable** iff `r ≤ 1/3`, equivalently iff `f ≥ 0`.

* For **projective measurements**, the steering threshold is known to be
`r_s^{PVM} = 1/2`,
equivalently
`f_s^{PVM} = -1/4`.

The original open question was:

* **Main question:** determine the critical threshold for **general POVMs**,
`r_s^{POVM}` (equivalently `f_s^{POVM}`),
and decide whether POVMs are strictly more powerful than projective measurements for steering two-qubit Werner states.

A very useful equivalent reformulation is via **measurement incompatibility**:

* Define the noisy version of a qubit POVM `{M_a}_a` by
`M_a^r = r M_a + (1-r) Tr(M_a) I / 2`.

* Then the Werner steering question is equivalent to asking for which `r` **every noisy qubit POVM is jointly measurable**.

Resolved statement to formalize (recommended):

* `r_s^{POVM} = 1/2`, equivalently `f_s^{POVM} = -1/4`.

* Therefore **POVMs and projective measurements are equally powerful** for steering the two-qubit Werner family:
`ρ_W(r)` is unsteerable for all qubit POVMs iff `r ≤ 1/2`,
and steerable already with projective measurements when `r > 1/2`.

* Equivalently, **all noisy qubit POVMs are jointly measurable iff `r ≤ 1/2`**.

Natural remaining open direction (explicitly suggested on the OQP page):

* Extend the question from **two-qubit Werner states** to **higher-dimensional Werner states**, and determine the corresponding sharp steering / compatibility thresholds for arbitrary POVMs.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #39)](https://oqp.iqoqi.oeaw.ac.at/steering-bound-for-qubits-and-povms)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)

Foundational steering references:

* H. M. Wiseman, S. J. Jones, and A. C. Doherty, “Steering, entanglement, nonlocality, and the Einstein-Podolsky-Rosen paradox”
(Phys. Rev. Lett. 98, 140402 (2007); arXiv: [quant-ph/0612147](https://arxiv.org/abs/quant-ph/0612147))
* S. J. Jones, H. M. Wiseman, and A. C. Doherty, “Entanglement, EPR-correlations, Bell-nonlocality, and steering”
(Phys. Rev. A 76, 052116 (2007); arXiv: [0709.0390](https://arxiv.org/abs/0709.0390))

Original Werner-state background:

* R. F. Werner, “Quantum states with Einstein-Podolsky-Rosen correlations admitting a hidden-variable model”
(Phys. Rev. A 40, 4277–4281 (1989))

Steering / incompatibility viewpoint:

* R. Uola, T. Moroder, and O. Gühne, “Joint measurability of generalized measurements implies classicality”
(Phys. Rev. Lett. 113, 160403 (2014); arXiv: [1407.2224](https://arxiv.org/abs/1407.2224))

Key partial progress before the exact solution:

* H. Chau Nguyen, Antony Milne, Thanh Vu, and Sania Jevtic, “Quantum steering with positive operator valued measures”
(J. Phys. A: Math. Theor. 51, 435302 (2018); arXiv: [1706.08166](https://arxiv.org/abs/1706.08166))
(gives strong numerical evidence that the POVM threshold is `r = 1/2`)

Resolution / exact bound:

* Y. Zhang and E. Chitambar, “Exact Steering Bound for Two-Qubit Werner States”
(Phys. Rev. Lett. 132, 250201 (2024); arXiv: [2309.09960](https://arxiv.org/abs/2309.09960))
(proves the exact POVM steering threshold for two-qubit Werner states)

* M. J. Renner, “Compatibility of Generalized Noisy Qubit Measurements”
(Phys. Rev. Lett. 132, 250202 (2024); arXiv: [2309.12290](https://arxiv.org/abs/2309.12290))
(proves the exact compatibility threshold for all noisy qubit POVMs, yielding the same steering bound)

### Prerequisites needed

* Finite-dimensional quantum mechanics: density matrices, tensor products, trace / partial trace
* Qubit measurements: projective measurements, POVMs, Bloch-sphere parametrizations
* Quantum steering: assemblages, local-hidden-state models, steerability vs unsteerability
* Two-qubit Werner states and their standard parametrizations
* Basic linear algebra / matrix analysis and convexity
* (Very useful) joint measurability / measurement incompatibility and its relation to steering

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-81 (Quantum theory)
* ams-15 (Linear and multilinear algebra; matrix theory)
* ams-47 (Operator theory)
* ams-94 (Information and communication theory)

### Choose either option

* [ ] I plan on adding this conjecture to the repository
* [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---

Start with the recommended resolved statement and read Zhang and Chitambar’s exact-bound paper, alongside Renner’s compatibility result. Check the repository’s existing formalizations for quantum theory and Werner states, then formalize the r = 1/2 or f = -1/4 threshold; done means the stated two-qubit POVM result is proved in Lean, with any higher-dimensional extension scoped separately.

Written by the indexing model from the issue text.