Formalize Open Quantum Problem #30: Asymptotic Version of Birkhoff's Theorem

### What is the conjecture

This is problem [#30](https://oqp.iqoqi.oeaw.ac.at/asymptotic-version-of-birkhoffs-theorem) in Reinhard F. Werner's open-problems collection, later [maintained by a community of quantum researchers](https://oqp.iqoqi.oeaw.ac.at/).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (solved negatively by Haagerup–Musat; first in 2011, with a stronger follow-up in 2015; see below).

> **Problem (Open Quantum Problem #30: “Asymptotic Version of Birkhoff's Theorem”).**
> A classical theorem of Birkhoff says that every doubly stochastic matrix is a convex combination of permutation matrices.
> In the quantum setting, doubly stochastic matrices become doubly stochastic quantum channels, i.e. completely positive maps preserving both the trace and the identity. The direct quantum analogue is false, but perhaps it becomes true asymptotically under tensor powers.
> Decide whether for every doubly stochastic quantum channel `T`, the tensor powers `T^{⊗ n}` become arbitrarily well approximable by convex combinations of unitarily implemented channels.

Concretely, let `T : M_d(C) → M_d(C)` be a **doubly stochastic** quantum channel, i.e. a completely positive, trace-preserving, and unital map. Let
`Aut(M_d(C)) = { ad_U : x ↦ U x U^* | U ∈ U(d) }`
be the unitarily implemented channels, and for a set `A` of channels write
`d_cb(T, A) := inf_{R ∈ A} ||T - R||_cb`.
The **Birkhoff defect** of `T` is then
`d_B(T) := d_cb(T, conv(Aut(M_d(C))))`,
the cb-norm distance from `T` to the convex hull of unitary channels.

The asymptotic quantum Birkhoff conjecture asks whether
`d_B(T^{⊗ n}) → 0` as `n → ∞`
for every doubly stochastic channel `T`. Equivalently: can every doubly stochastic quantum channel become arbitrarily close, after taking enough tensor powers, to a convex combination of unitary conjugations on the large tensor-product system?

The OQP page also records a weaker Jamiołkowski-dualized variant: if a bipartite state on equal-dimensional systems has maximally mixed marginals, must large tensor powers of that state be approximable in trace norm by convex combinations of maximally entangled pure states?

**Solved statement to formalize (Haagerup–Musat, 2011; strengthened in 2015):**
The asymptotic quantum Birkhoff conjecture is **false**.

- In `Commun. Math. Phys. 303 (2011)`, Haagerup–Musat proved that for every `n ≥ 3` there exist `τ_n`-Markov maps on `M_n(C)` (equivalently, doubly stochastic / UCPT channels) that **do not** satisfy the asymptotic quantum Birkhoff property. In fact, any **non-factorizable** `τ_n`-Markov map `T : M_n(C) → M_n(C)` is a counterexample. Writing `FM(M_n(C))` for the set of factorizable maps, they show
`d_cb(T^{⊗ k}, FM(M_n(C)^{⊗ k})) ≥ d_cb(T, FM(M_n(C)))` for all `k ≥ 1`.
Since `conv(Aut(M_n(C)^{⊗ k})) ⊂ FM(M_n(C)^{⊗ k})`, a non-factorizable channel can never become asymptotically mixed-unitary.

- In `Commun. Math. Phys. 338 (2015)`, Haagerup–Musat strengthened the picture by giving even a **factorizable** counterexample: a factorizable UCPT Schur multiplier `T_B` on `M_6(C)` with `T_B ∉ conv(Aut(M_6(C)))`, and hence `T_B^{⊗ r} ∉ conv(Aut(M_{6^r}(C)))` for every `r ≥ 2`. More generally, for UCPT Schur multipliers `T : M_n(C) → M_n(C)` and `S : M_k(C) → M_k(C)`,
`d_cb(T ⊗ S, conv(Aut(M_{nk}(C)))) ≥ (1/2) d_cb(T, conv(Aut(M_n(C))))`.
So tensoring does not wash out the Birkhoff defect for these examples.

This means that the natural quantum analogue of Birkhoff's theorem fails not only exactly, but even asymptotically.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #30)](https://oqp.iqoqi.oeaw.ac.at/asymptotic-version-of-birkhoffs-theorem)
- [Solved Quantum Problems list (shows #30 solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
- U. Haagerup and M. Musat (2011), Section 6, which explicitly states the conjecture as “Problem 30 on R. Werner’s web page of open problems in quantum information theory”

Key solution references (as cited on the OQP page):
- U. Haagerup and M. Musat, **“Factorization and dilation problems for completely positive maps on von Neumann algebras”**, *Commun. Math. Phys.* 303, 555–594 (2011); arXiv: [1009.0778](https://arxiv.org/abs/1009.0778)
- U. Haagerup and M. Musat, **“An asymptotic property of factorizable completely positive maps and the Connes embedding problem”**, *Commun. Math. Phys.* 338, 721–752 (2015); arXiv: [1408.6476](https://arxiv.org/abs/1408.6476)

Related / background references mentioned on the OQP page (useful for a formalization roadmap):
- L. J. Landau and R. F. Streater, **“On Birkhoff’s theorem for doubly stochastic completely positive maps of matrix algebras”**, *Linear Algebra Appl.* 193, 107–127 (1993)
- M. Gregoratti and R. F. Werner, **“Quantum Lost and Found”**, *J. Mod. Opt.* 50, 915–933 (2003); arXiv: [quant-ph/0209025](https://arxiv.org/abs/quant-ph/0209025)
- A. Winter, **“On environment-assisted capacities of quantum channels”**, arXiv: [quant-ph/0507045](https://arxiv.org/abs/quant-ph/0507045)
- J. A. Smolin, F. Verstraete, and A. Winter, **“Entanglement of assistance and multipartite state distillation”**, *Phys. Rev. A* 72, 052317 (2005); arXiv: [quant-ph/0505038](https://arxiv.org/abs/quant-ph/0505038)

### Prerequisites needed

- Finite-dimensional matrix algebras `M_n(C)`; completely positive maps; trace-preserving and unital channels (`UCPT` / doubly stochastic channels)
- Completely bounded norm / cb-distance; convex hulls; tensor products and tensor powers of channels
- Unitarily implemented channels `ad_U`; mixed-unitary channels; Choi/Jamiołkowski correspondence
- Factorizable maps / exact factorizations through `M_n(C) ⊗ N` for a finite tracial von Neumann algebra
- Depending on the route one formalizes:
- the 2011 route uses non-factorizable maps and operator-algebraic arguments,
- the 2015 route uses Schur multipliers and an explicit lower bound preventing asymptotic mixed-unitarity

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

- ams-81 (Quantum theory)
- ams-46 (Functional analysis)
- ams-47 (Operator 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 by reading the Haagerup–Musat 2011 and 2015 papers and the Open Quantum Problems page cited in the issue, then inspect the repository's existing formalized conjectures for an appropriate entry point. Done means adding a precise formal statement capturing the negative asymptotic quantum Birkhoff result, with any required definitions and supporting proofs or references formalized.

Written by the indexing model from the issue text.