Formalize Open Quantum Problem #21: Bell violation by tensoring

### What is the conjecture

This is problem [#21](https://oqp.iqoqi.oeaw.ac.at/bell-violation-by-tensoring) 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 Navascués–Vértesi, 2011; see below).

> **Problem (Open Quantum Problem #21: “Bell violation by tensoring”).**
> Can one find bipartite density operators `ρ_1, ρ_2`, neither of which violates any CHSH Bell inequality, with the property that `ρ_1 ⊗ ρ_2` does?

Concretely, for a bipartite state `ρ ∈ D(H_A ⊗ H_B)`, define the maximal **CHSH value**
`β_CHSH(ρ) := sup_{A_0,A_1,B_0,B_1} Tr[ ρ (A_0 ⊗ B_0 + A_0 ⊗ B_1 + A_1 ⊗ B_0 - A_1 ⊗ B_1) ]`,
where the supremum is over local observables `A_0, A_1` on `H_A` and `B_0, B_1` on `H_B` satisfying `A_x^2 = I` and `B_y^2 = I`.

Then:
- `β_CHSH(ρ) ≤ 2` means `ρ` does **not** violate the CHSH inequality,
- `β_CHSH(ρ) > 2` means `ρ` **does** violate CHSH,
- always `β_CHSH(ρ) ≤ 2√2` (Tsirelson bound).

If `ρ_1 ∈ D(H_{A_1} ⊗ H_{B_1})` and `ρ_2 ∈ D(H_{A_2} ⊗ H_{B_2})`, the tensor product `ρ_1 ⊗ ρ_2` is viewed as a bipartite state on
`(H_{A_1} ⊗ H_{A_2}) ⊗ (H_{B_1} ⊗ H_{B_2})`,
so the Bell test on the product may use **joint local measurements** on Alice’s combined system `A_1A_2` and Bob’s combined system `B_1B_2`.

The question is whether Bell nonlocality can be **activated by tensoring**, i.e. whether there exist states with
`β_CHSH(ρ_1) ≤ 2`, `β_CHSH(ρ_2) ≤ 2`, but `β_CHSH(ρ_1 ⊗ ρ_2) > 2`.

**Solved statement to formalize (Navascués–Vértesi, 2011):**
There exist two **two-qubit** states `ρ_1, ρ_2 ∈ D(C^2 ⊗ C^2)` such that for every `N ≥ 1`,

- `β_CHSH(ρ_1^{⊗N}) ≤ 2`,
- `β_CHSH(ρ_2^{⊗N}) ≤ 2`,

yet their mixed tensor product is CHSH-violating:
- `β_CHSH(ρ_1 ⊗ ρ_2) ≥ 2.023 > 2`.

Hence the answer to Problem #21 is **yes**: CHSH/Bell nonlocality can be activated by tensoring two individually CHSH-local states.

Moreover, the same paper also identifies a single CHSH-local state `ρ` such that `ρ^{⊗2}` is CHSH-violating.

**Important structural point (also highlighted on the OQP page):**
If a bipartite state `ρ_AB` admits a **2-symmetric extension** on one subsystem — e.g. there exists a state `ω_{AB_1B_2}` that is invariant under swapping `B_1` and `B_2`, with `Tr_{B_2}(ω_{AB_1B_2}) = ρ_{AB_1}` — then neither `ρ` nor any tensor power `ρ^{⊗N}` can violate any **two-setting** Bell inequality. Navascués–Vértesi exploit two states with symmetric extensions on different sides; each factor separately stays two-setting Bell-local under tensor powers, but the tensor product need not remain symmetrically extendible and can therefore violate CHSH.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #21)](https://oqp.iqoqi.oeaw.ac.at/bell-violation-by-tensoring)
- [Solved Quantum Problems list (shows #21 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 21”)

Key solution reference (as cited on the OQP page):
- M. Navascués and T. Vértesi, **“Activation of Non-Local Quantum Resources”**, *Phys. Rev. Lett.* 106, 060403 (2011); arXiv: [1010.5191](https://arxiv.org/abs/1010.5191)

Related / structural background mentioned on the OQP page (useful for a formalization roadmap):
- B. M. Terhal, A. C. Doherty and D. Schwab, **“Local Hidden Variable Theories for Quantum States”**, *Phys. Rev. Lett.* 90, 157903 (2003); arXiv: [quant-ph/0210053](https://arxiv.org/abs/quant-ph/0210053)

### Prerequisites needed

- Finite-dimensional quantum states and observables: density operators, tensor products, partial trace
- Bell inequalities / CHSH: local hidden variable models, CHSH operators, Tsirelson bound
- Tensor powers of bipartite states, and the fact that Bell tests on `ρ_1 ⊗ ρ_2` use joint local measurements on the combined local systems
- Symmetric extensions / shareability of bipartite states, and their relation to two-setting Bell locality
- Basic convexity / semidefinite-programming ideas (useful for symmetric-extension tests and the numerical search for examples)

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

- ams-81 (Quantum theory)
- ams-47 (Operator theory)
- 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

Start by reading the Navascués–Vértesi paper and the Open Quantum Problems entry for Problem #21, then inspect the repository's existing Lean formalizations of finite-dimensional quantum states, tensor products, CHSH inequalities, and symmetric extensions. Formalize the stated two-qubit existence result, including the tensor-power locality claims and the mixed-product CHSH violation, with supporting definitions and proofs where feasible.

Written by the indexing model from the issue text.