Formalize Open Quantum Problem #5: Maximally entangled mixed states

### What is the conjecture
This is problem [#5](https://oqp.iqoqi.oeaw.ac.at/maximally-entangled-mixed-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).

> **Problem (Open Quantum Problem #5: “Maximally entangled mixed states”).**
> Among all density operators of two qubits with the same spectrum, the states maximizing **entanglement of formation**, **relative entropy of entanglement**, and **negativity** coincide (Verstraete–Audenaert–De Moor).
> Is this true for *arbitrary* entanglement monotones?

More concretely, we work with two-qubit density matrices `ρ` on `C^2 ⊗ C^2` (positive semidefinite, trace `1`). Fix a spectrum
`λ = (λ1 ≥ λ2 ≥ λ3 ≥ λ4)` with `λi ≥ 0` and `λ1+…+λ4 = 1`, and consider the isospectral set
`S_λ = { ρ : spec(ρ) = λ }`.

For an entanglement monotone `E` (i.e. a function on bipartite states that does not increase under LOCC / local operations), one can ask for
`max_{ρ ∈ S_λ} E(ρ)`.
Verstraete–Audenaert–De Moor identify a canonical LU-equivalence class of “maximally entangled mixed states” (MEMS) for each fixed spectrum `λ` that simultaneously maximizes three standard entanglement measures (EoF, REE, negativity). The open question asks whether the *same* LU-class maximizes **every** entanglement monotone.

The Open Quantum Problem page also mentions natural variants, e.g.:
- higher-dimensional bipartite systems (beyond `2 ⊗ 2`),
- weaker spectral constraints (e.g. only fixing the largest eigenvalue, or the entropy).

**Status note (useful for formalization):** de Vicente (2024) gives a negative answer in general: for certain fixed spectra, a “maximally entangled mixed state for that spectrum” need not exist (in the strong sense of being maximal for all entanglement monotones / under suitable free operations). This suggests a good formalization target might be the original conjecture statement *plus* a formal counterexample / “solved by negative answer” entry.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #5)](https://oqp.iqoqi.oeaw.ac.at/maximally-entangled-mixed-states)
- [Open Quantum Problems index](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)
- [Werner’s original 2005 list (arXiv: quant-ph/0504166)](https://arxiv.org/abs/quant-ph/0504166)

Key related reference mentioned on the problem page:
- F. Verstraete, K. Audenaert, and B. De Moor, “Maximally entangled mixed states of two qubits” (arXiv: [quant-ph/0011110](https://arxiv.org/abs/quant-ph/0011110); Phys. Rev. A 64, 012316 (2001))

Later progress / resolution (negative answer):
- J. I. de Vicente, “Maximally entangled mixed states for a fixed spectrum do not always exist” (arXiv: [2402.05673](https://arxiv.org/abs/2402.05673); Phys. Rev. Lett. 133, 050202 (2024))

### Prerequisites needed
- Finite-dimensional linear algebra over `C`: Hermitian/PSD matrices, trace, eigenvalues/spectrum, unitary conjugation
- Basic quantum information: density operators, two-qubit systems, local unitaries
- Standard entanglement measures (EoF / REE / negativity) and the definition/axioms of an **entanglement monotone**
- (If formalizing the 2024 negative result) CPTP maps, separable states, and “non-entangling” operations / LOCC-style monotonicity arguments

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)
* ams-81 (Quantum theory)
* ams-15 (Linear and multilinear algebra; matrix theory)
* ams-94 (Information and communication 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 Verstraete–Audenaert–De Moor paper and the de Vicente 2024 paper, then compare them with Open Quantum Problems #5. Formalize the original fixed-spectrum conjecture or a precise counterexample/negative-answer entry, with the relevant definitions and a statement whose completion is checked in the repository's Lean development.

Written by the indexing model from the issue text.