Formalize Open Quantum Problem #1: All the Bell inequalities

### What is the conjecture
This is problem [#1](https://oqp.iqoqi.oeaw.ac.at/all-the-bell-inequalities) 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).

> **Problem (Open Quantum Problem #1: “All the Bell inequalities”).**
> Find all linear inequalities characterizing the existence of joint probability distributions for all variables in a correlation experiment.

A standard “Bell scenario” is parameterized by natural numbers:
- `N`: number of subsystems (parties),
- `M`: number of observables (measurement choices) per subsystem,
- `K`: number of outcomes per observable.

For each measurement setting `x ∈ {1,…,M}^N`, one observes outcome probabilities
`p(a | x)` where `a ∈ {1,…,K}^N`. Altogether one has `(MK)^N` probabilities (subject to normalization constraints).

Classically (“local realistic theory”), these probabilities arise as marginals of a single **joint distribution** over all `N*M` observables, i.e. over assignments of `K` outcomes to each observable. Equivalently, the set of “local” behaviors forms a **convex polytope** whose vertices correspond to deterministic assignments, and the desired inequalities are the **facet-defining linear inequalities** of this polytope (“Bell inequalities”).

The Open Quantum Problem page suggests several concrete sub-goals, e.g.:
- find complete facet descriptions for other small values of `(N,M,K)` (beyond `(2,2,2)` / CHSH),
- develop efficient ways of generating genuinely new inequalities (not convex combinations of lower-order ones),
- find infinite families of inequalities (possibly with symmetries),
- restrict to “full correlation functions” (ignoring marginal constraints),
- specialize to **correlation inequalities** (notably `K = 2`, outcomes ±1) and study quantum violations.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site(Problem #1)](https://oqp.iqoqi.oeaw.ac.at/all-the-bell-inequalities)

Key related references mentioned on the problem page:
- A. Peres, “All the Bell inequalities” (Found. Phys. 29, 589 (1999); arXiv: quant-ph/9807017)
- R. F. Werner and M. M. Wolf, “All multipartite Bell correlation inequalities for two dichotomic observables per site” (Phys. Rev. A 64, 032112 (2001); arXiv: quant-ph/0102024)
- I. Pitowsky and K. Svozil, numerical facet enumerations for small cases (see links/citations on the OQP page)

### Prerequisites needed
- Finite probability distributions; joint distributions and marginals
- Basic convex geometry: convex hulls, polytopes, facets / supporting hyperplanes
- Linear inequalities / linear algebra; optionally some computational complexity background (facet enumeration is hard in general)

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)
* ams-81 (Quantum theory)
* ams-52 (Convex and discrete geometry)
* 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

Start with the linked Open Quantum Problems page and the cited Bell-inequality references to choose a precise, formalizable statement. Then inspect the repository's existing conjecture additions and Lean entry points, and define completion as a reviewed Lean formalization with the repository checks passing.

Written by the indexing model from the issue text.