Formalize Open Quantum Problem #27: The power of CGLMP inequalities

### What is the conjecture

This is problem [#27](https://oqp.iqoqi.oeaw.ac.at/the-power-of-cglmp-inequalities) in the [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems), in the same Bell-scenario framework as [Problem #26](https://oqp.iqoqi.oeaw.ac.at/bell-inequalities-holding-for-all-quantum-states).

> **Problem (Open Quantum Problem #27: “The power of CGLMP inequalities”).**
> In the setting of Problem #26, consider especially the case `(N,M,K)=(2,2,d)`.
>
> **Problem 27.A.**
> Show that every face of the local polytope `C`, which is not already contained in a face of the no-signalling polytope `P`, is of CGLMP type, i.e. of the form first written down by Collins–Gisin–Linden–Massar–Popescu, possibly lifted from lower dimensions by fusing together some outcomes.
>
> **Problem 27.B.**
> Numerically, the observables maximally violating the CGLMP inequality on a maximally entangled state are of a very specific form, involving measurements in the computational basis, transformed only by the discrete Fourier transform and diagonal unitaries. Show that this is necessarily the case. Show also that these measurements realize the highest resistance of violation to noise, and the best discrimination against classical realism in the sense of Kullback–Leibler divergence.

A standard formalization uses the bipartite Bell scenario `2×2×d`:

* Two parties Alice and Bob choose inputs `x,y ∈ {1,2}` and obtain outputs `a,b ∈ {0,…,d-1}`.
* A behavior is a conditional probability table `p(a,b | x,y)`.
* The **local polytope** `C = C_{2,2,d}` is the convex hull of deterministic strategies
`p(a,b|x,y) = δ_{a,f(x)} δ_{b,g(y)}`
with `f,g : {1,2} → {0,…,d-1}`.
* The **quantum set** `Q = Q_{2,2,d}` consists of behaviors of the form
`p(a,b|x,y) = Tr[ρ (A_x^a ⊗ B_y^b)]`,
so `C ⊂ Q ⊂ P`.
* The **no-signalling polytope** `P = P_{2,2,d}` is the set of behaviors satisfying positivity, normalization, and the usual no-signalling constraints.
* A **proper Bell inequality** in this setting is an affine inequality valid on `C` that is not already implied by the defining constraints of `P`.

The Collins–Gisin–Linden–Massar–Popescu (**CGLMP**) inequality is the canonical Bell inequality in this scenario. One convenient form (the one highlighted on the OQP page) is:

* For random variables `A_1,A_2,B_1,B_2 ∈ {0,…,d-1}`, define `m(t)=t mod d` in `{0,…,d-1}` and write `E` for expectation.
* Then every local model satisfies
`E(m(A_1-B_1)) + E(m(B_1-A_2)) + E(m(A_2-B_2)) + E(m(B_2-A_1-1)) ≥ d-1`.

Because Problem 27 is posed as two connected assertions, a natural formalization target is:

* **Problem 27.A (classification of nontrivial Bell faces/facets in `2×2×d`):**
show that every face of `C_{2,2,d}` not coming already from a face of `P_{2,2,d}` is of CGLMP type, up to the usual symmetries and up to liftings from smaller output alphabets by identifying / fusing outcomes.

* **Problem 27.B (optimality of the standard CGLMP measurements):**
fix the maximally entangled state
`|Φ_d⟩ = (1/√d) ∑_{j=0}^{d-1} |jj⟩`
on `C^d ⊗ C^d`, and optimize the CGLMP Bell functional over local complete von Neumann `d`-outcome measurements.
The conjecture is that any optimizer is, up to local symmetries, the standard Fourier-phase family (computational basis followed by the discrete Fourier transform and diagonal phase unitaries).

There are also two closely related optimization statements explicitly mentioned on the OQP page:

* **Noise resistance:** the same measurement family should maximize the critical visibility / resistance to white noise for CGLMP violation on `|Φ_d⟩`.
* **Statistical strength:** the same measurement family should maximize discrimination against local realism in the sense of the van Dam–Grunwald–Gill Kullback–Leibler divergence.

Partial results already recorded on the OQP page / later references:

* Masanes proved that the CGLMP inequality is indeed a facet of the local polytope in the `(2,2,d)` scenario.
* Lang–Vértesi–Navascués used SDP relaxations to show for `d=3` that the maximum violation on maximally entangled states of arbitrary dimension differs by at most `10^{-10}` from the local maximum found numerically by Durt–Kaszlikowski–Zukowski.
* Ioannou–Rosset later gave analytic sum-of-squares certificates proving the exact maximal quantum value for CGLMP in the cases `d=3,4`.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #27)](https://oqp.iqoqi.oeaw.ac.at/the-power-of-cglmp-inequalities)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)
* [Open Quantum Problems site (Problem #26, for the `N,M,K` setting and the `C ⊂ Q ⊂ P` picture)](https://oqp.iqoqi.oeaw.ac.at/bell-inequalities-holding-for-all-quantum-states)

Key related references (as listed on the OQP page):

* D. Collins, N. Gisin, N. Linden, S. Massar, and S. Popescu, “Bell inequalities for arbitrarily high dimensional systems” (Phys. Rev. Lett. 88, 040404 (2002); arXiv: quant-ph/0106024)
(introduces the CGLMP family)
* T. Durt, D. Kaszlikowski, and M. Zukowski, “Violations of local realism with quNits up to N=16” (Phys. Rev. A 64, 024101 (2001); arXiv: quant-ph/0101084)
(numerically identifies the special Fourier/phase measurement family and studies noise resistance)
* W. van Dam, P. Grunwald, and R. Gill, “The statistical strength of nonlocality proofs” (arXiv: quant-ph/0307125; IEEE Trans. Inf. Theory 51, 2812–2835 (2005))
(introduces the KL-divergence / statistical-strength viewpoint)
* A. Acín, R. Gill, and N. Gisin, “Optimal Bell tests do not require maximally entangled states” (Phys. Rev. Lett. 95, 210402 (2005); arXiv: quant-ph/0506225)
(detailed discussion of the problem and the role of non-maximally entangled states)
* Ll. Masanes, “Tight Bell inequality for d-outcome measurements correlations” (Quantum Inf. Comput. 3, 345–358 (2003); arXiv: quant-ph/0210073)
(proves that CGLMP is a facet of the local polytope)
* B. Lang, T. Vértesi, and M. Navascués, “Closed sets of correlations: answers from the zoo” (J. Phys. A 47, 424029 (2014))
(gives SDP upper bounds showing the `d=3` maximally-entangled-state optimum is achieved, up to computer precision, by the conjectured measurements)
* A. Acín, T. Durt, N. Gisin, and J. I. Latorre, “Quantum non-locality in two three-level systems” (Phys. Rev. A 65, 052325 (2002); arXiv: quant-ph/0111143)
(shows that higher CGLMP violations can be obtained with non-maximally entangled states while using the same measurement family)
* M. Navascués, S. Pironio, and A. Acín, “Bounding the set of quantum correlations” (Phys. Rev. Lett. 98, 010401 (2007); arXiv: quant-ph/0607119)
(the NPA hierarchy underlying several of the quantum upper bounds)
* M. Ioannou and D. Rosset, “Noncommutative polynomial optimization under symmetry” (arXiv:2112.10803)
(analytic sum-of-squares proofs of the exact CGLMP quantum bounds for `d=3,4`)

### Prerequisites needed

* Finite probability distributions and Bell scenarios (`p(a,b|x,y)`, local hidden-variable models)
* Basic convex geometry / polytope language: local polytope, no-signalling polytope, faces, facets, liftings
* Finite-dimensional quantum mechanics: projective measurements, maximally entangled states, Bell operators, Born rule
* Linear algebra on `C^d`: unitary matrices, discrete Fourier transform, diagonal phase operators
* (For the main partial results) semidefinite programming / NPA-type relaxations and sum-of-squares certificates
* (Optional) information-theoretic viewpoint on nonlocality via Kullback–Leibler divergence

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

* ams-81 (Quantum theory)
* ams-52 (Convex and discrete geometry)
* ams-94 (Information and communication theory)
* ams-68 (Computer science)

### 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 or test is named; start by examining how nearby conjectures, especially Problem #26, are formalized in Lean. Choose either 27.A or 27.B, then use the linked OQP statement and cited prerequisites to define a precise theorem. Done means a compiling Lean formalization of the selected option.

Written by the indexing model from the issue text.