Formalize Open Quantum Problem #19: Stronger Bell Inequalities for Werner states?

### What is the conjecture

This is problem [#19](https://oqp.iqoqi.oeaw.ac.at/stronger-bell-inequalities-for-werner-states) in [Reinhard F. Werner's collection](https://arxiv.org/abs/quant-ph/0504166), later [collected by a community of quantum researchers](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (solved by T. Vértesi, 2008; see below).

> **Problem (Open Quantum Problem #19: “Stronger Bell Inequalities for Werner states?”).**
> Find Bell inequalities which are stronger than the CHSH inequalities in the sense that they are violated by a wider range of Werner states.

Concretely, the OQP page recalls the family of Werner states
`ρ_W(d,p) = p * 2 P_asym / (d(d-1)) + (1-p) I / d^2`,
where `P_asym` is the projector onto the antisymmetric subspace of `C^d ⊗ C^d`.

In the qubit case `d = 2`, this reduces to
`ρ_p = p |ψ^-⟩⟨ψ^-| + (1-p) I / 4`,
where `|ψ^-⟩ = (|01⟩ - |10⟩) / √2`.

For the standard CHSH Bell inequality, the two-qubit Werner state is nonlocal whenever
`p > 1 / √2 ≈ 0.70710678`.

Thus a Bell inequality is “stronger than CHSH for Werner states” if it has a strictly smaller critical visibility `p_c < 1 / √2`, i.e. it detects nonlocality for some Werner states that do **not** violate CHSH.

The OQP page also records the useful reformulation from Acín–Gisin–Toner: when restricting to **correlation** Bell inequalities with dichotomic measurements, the two-qubit Werner state violates a Bell inequality iff
`p > 1 / K_G(3)`,
where `K_G(3)` is Grothendieck’s constant of order `3`. At the time the problem was posed, the best lower bound available was only `K_G(3) ≥ √2`, which again yielded just the CHSH threshold.

**Solved statement to formalize (Vértesi, 2008):**
Vértesi constructs an explicit family of bipartite correlation Bell inequalities `I_{n,n}` of the form
`I_{n,n} = Σ_{i=1}^n Σ_{j=1}^n ⟨A_i B_j⟩ + Σ_{1≤i √2`. Vértesi does exactly this. In particular:

- an explicit construction already gives `K_G(3) > √2` for `n = 30`, yielding a concrete Bell inequality with `m = n(n+1)/2 = 465` settings per party that is stronger than CHSH for two-qubit Werner states;
- a stronger optimized bound in the same paper gives
`K_G(3) ≥ 1.417241`,
hence the two-qubit Werner state `ρ_p` is nonlocal for
`p > 1 / 1.417241 ≈ 0.705596`,
improving the CHSH threshold `1 / √2 ≈ 0.707107`.

Equivalently: there exist Bell inequalities more efficient than CHSH for the two-qubit Werner family, so Gisin’s question has a positive answer.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #19)](https://oqp.iqoqi.oeaw.ac.at/stronger-bell-inequalities-for-werner-states)
- [Solved Quantum Problems list (shows #19 solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
- [Werner / Krüger–Werner arXiv list](https://arxiv.org/abs/quant-ph/0504166) (see “Problem 19”)

Key solution reference (as cited on the OQP page):
- T. Vértesi, **“More efficient Bell inequalities for Werner states”**, *Phys. Rev. A* 78, 032112 (2008); arXiv: [0806.0096](https://arxiv.org/abs/0806.0096)

Related / partial results mentioned on the OQP page (useful background for a formalization roadmap):
- A. Acín, N. Gisin and B. Toner, **“Grothendieck’s constant and local models for noisy entangled quantum states”**, *Phys. Rev. A* 73, 062105 (2006); arXiv: [quant-ph/0606138](https://arxiv.org/abs/quant-ph/0606138)
- D. Collins and N. Gisin, **“A Relevant Two Qubit Bell Inequality Inequivalent to the CHSH Inequality”**, *J. Phys. A* 37, 1775–1787 (2004); arXiv: [quant-ph/0306129](https://arxiv.org/abs/quant-ph/0306129)
- J. L. Krivine, lower bounds related to Grothendieck constants (*Adv. Math.* 31, 16 (1979))
- Later improvements to lower bounds on `K_G(3)` mentioned on the OQP page: B. Hua et al. (2015), S. Brierley, M. Navascués and T. Vértesi (2016)

### Prerequisites needed

- Bipartite quantum states; the singlet state; Werner states and their symmetry properties
- Bell scenarios with two parties and finitely many dichotomic observables
- Correlator Bell inequalities `⟨A_x B_y⟩`; local hidden-variable models; classical/local bounds; quantum violations
- CHSH inequality as the baseline example; optionally `I3322` as useful nearby background
- Grothendieck’s constant of order `3` and its relation to two-qubit Werner-state nonlocality
- Tsirelson / vector-representation viewpoint for correlation Bell inequalities (or at least the singlet-state inner-product formulation)
- Finite-dimensional linear algebra and basic optimization; optionally semidefinite-programming ideas if one wants to formalize the stronger quantitative bound

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

- ams-81 (Quantum theory)
- ams-52 (Convex and discrete geometry)
- ams-46 (Functional analysis)

### 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
---

No repository file, test, or entry point is identified in the issue. Start by reading Vértesi’s paper and the cited Open Quantum Problems material, then inspect formal-conjectures for conventions for quantum statements. Done means adding a Lean formalization of the stated Bell-inequality result and its stronger-than-CHSH consequence.

Written by the indexing model from the issue text.