Formalize Open Quantum Problem #4: Catalytic majorization

### What is the conjecture

This is problem [#4](https://oqp.iqoqi.oeaw.ac.at/catalytic-majorization) 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). It is **solved** (see the [Solved Quantum Problems list](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)).

> **Problem (Open Quantum Problem #4: “Catalytic majorization”).**
> Give an efficient criterion deciding when a bipartite pure state transformation that is *impossible* under LOCC becomes possible in the presence of a *catalyst* state that is returned unchanged.
> Equivalently (in the classical reformulation): given probability vectors `p, q`, decide when there exists a probability vector `r` such that
> `(p ⊗ r) ≺ (q ⊗ r)`,
> where `≺` denotes the usual **majorization** order.

Concretely, let `p = (p₁,…,pₙ)` and `q = (q₁,…,qₙ)` be **probability vectors** (`pᵢ ≥ 0`, `∑ᵢ pᵢ = 1`, similarly for `q`). Write `p^↓` for the vector sorted in non-increasing order. Then:

* **Majorization**: `p ≺ q` iff for all `k = 1,…,n`,
`∑_{i=1}^k p^↓_i ≤ ∑_{i=1}^k q^↓_i` and equality holds at `k = n`.
* **Catalytic majorization** (also called **trumping**): `p ≺_cat q` iff there exists some dimension `c` and a probability vector `r ∈ ℝ^c` such that `(p ⊗ r) ≺ (q ⊗ r)`.

The key point from quantum information theory is that, by Nielsen’s theorem, LOCC convertibility of bipartite pure states is characterized by majorization of the corresponding Schmidt/eigenvalue vectors; allowing a catalyst corresponds exactly to catalytic majorization.

**Solved statement to formalize (Klimesh / Turgut, 2007):** the OQP page gives an explicit necessary-and-sufficient condition in terms of (classical) **Rényi entropies** plus one additional log-product functional. In one common formulation (as stated on the OQP page), under mild non-degeneracy/zero-entry assumptions, the following are equivalent:

* `∃ r` such that `(p ⊗ r) ≺ (q ⊗ r)`;
* strict inequalities `H_α(p) > H_α(q)` for all real `α ≠ 0`, together with `f₀(p) > f₀(q)`, where
`H_α` is the classical Rényi entropy and `f₀(p) = ∑ᵢ log pᵢ` (with appropriate conventions/extended reals when zero entries occur).

The OQP page also records a simpler characterization if one only asks for **approximate** catalytic convertibility (allowing an ε-perturbation of `q`), in which case the condition reduces to `H_α(p) ≥ H_α(q)` for all `α ∈ ℝ`.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #4)](https://oqp.iqoqi.oeaw.ac.at/catalytic-majorization)
* [Solved Quantum Problems list (shows #4 solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
* [Werner/Krüger snapshot of the problem list (2005)](https://arxiv.org/abs/quant-ph/0504166)

Key solution references (as cited on the OQP page):

* M. Klimesh, [“Inequalities that Collectively Completely Characterize the Catalytic Majorization Relation”](https://arxiv.org/abs/0709.3680)
* S. Turgut, [“Necessary and Sufficient Conditions for the Trumping Relation”](https://arxiv.org/abs/0707.0444)

Background (for motivation / definitions):

* M. A. Nielsen, [LOCC convertibility ⇔ majorization (1999)](https://arxiv.org/abs/quant-ph/9811053)
* D. Jonathan & M. B. Plenio, [entanglement catalysis phenomenon (1999)](https://arxiv.org/abs/quant-ph/9905071)

### Prerequisites needed

* Finite probability vectors; sorting (`p^↓`), tensor/Kronecker products of vectors (`p ⊗ r`)
* Majorization theory (any equivalent definition is fine: sorted partial sums, doubly stochastic matrices, convex-function characterization)
* Basic real analysis / information theory: Rényi entropies `H_α`, including handling special cases `α = 0, 1` and (optionally) `α < 0`
* Some care around **zero components** (logs / ranks / extended-real values), depending on which exact statement is formalized
* (Optional, for motivation) Schmidt coefficients, LOCC transformations of bipartite pure states

### [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

The issue names no repository files or tests. Start by reading the Klimesh and Turgut references and the repository's existing formalized statements, then choose the precise Rényi-entropy and zero-entry conventions to encode. Done means the catalytic-majorization result is added as a compiling Lean formalization.

Written by the indexing model from the issue text.