Formalize Open Quantum Problem #45. Catalytic entropy conjecture

### What is the conjecture

This is problem [#45](https://oqp.iqoqi.oeaw.ac.at/catalytic-entropy-conjecture) on the [Open Quantum Problems site](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems). It was proposed in [P. Boes, J. Eisert, R. Gallego, M. P. Müller, and H. Wilming (2019)](https://arxiv.org/abs/1807.08773).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (exact conjecture solved by Wilming, 2022; an approximate variant was solved earlier in 2021; see below).

> **Problem (Open Quantum Problem #45: “Catalytic entropy conjecture”).**
> Consider a density matrix `ρ` on a finite-dimensional system `S`. Let `H(ω) = -tr(ω log ω)` be the von Neumann entropy.
> Prove or disprove that for any density matrix `ρ'` on the same system `S` such that `H(ρ') > H(ρ)` and `rank(ρ') ≥ rank(ρ)`, there exists a finite-dimensional system `C` (“catalyst”) with state `σ_C` and a unitary operator `U` on `S ⊗ C` such that the following holds:
> `tr_C[U (ρ ⊗ σ_C) U†] = ρ'`
> `tr_S[U (ρ ⊗ σ_C) U†] = σ_C`.

Concretely, if such `σ_C` and `U` exist, we say that the exact catalytic transition `ρ → ρ'` is possible. The final joint state on `S ⊗ C` need not factor as `ρ' ⊗ σ_C`: correlations between system and catalyst are allowed, as long as the system marginal is `ρ'` and the catalyst marginal is returned exactly unchanged.

The conjecture asks whether, aside from the trivial case where `ρ` and `ρ'` are already unitarily equivalent, exact catalytic transitions are completely characterized by two simple state parameters:
- strict increase of von Neumann entropy, and
- non-decrease of rank/support size.

A positive solution gives a single-shot operational characterization of von Neumann entropy, without appealing to an i.i.d. asymptotic limit or to external randomness.

**Solved statement to formalize (Wilming, 2022):**
For finite-dimensional density matrices `ρ, ρ'` on the same system that are **not unitarily equivalent**, the following are equivalent:
- there exist a finite-dimensional catalyst state `σ_C` and a unitary `U` on `S ⊗ C` such that
`tr_C[U (ρ ⊗ σ_C) U†] = ρ'`
and
`tr_S[U (ρ ⊗ σ_C) U†] = σ_C`;
- `H(ρ') > H(ρ)` and `rank(ρ') ≥ rank(ρ)`.

Wilming’s 2022 paper also proves an equivalent majorization-style formulation: for some finite `n`, the tensor power `ρ^{⊗ n}` majorizes a state `Ω` on `S^{⊗ n}` whose one-body marginals are all exactly `ρ'`, if and only if the same entropy/rank conditions hold. This provides the route from correlated many-copy constructions to the exact catalytic transition.

**Earlier approximate result (Wilming, 2021):**
The OQP page records that Wilming first solved an approximate variant of the conjecture: for arbitrary `ε > 0`, the exact requirement `tr_C[U (ρ ⊗ σ_C) U†] = ρ'` is relaxed to
`|| tr_C[U (ρ ⊗ σ_C) U†] - ρ' ||_1 ≤ ε`,
while the catalyst marginal is still returned exactly.

**Important caveat (also on the OQP page):**
The boundary case `H(ρ') = H(ρ)` remains open. It lies outside the original conjecture: the OQP page notes that such a transformation cannot be implemented with a finite-dimensional catalyst, though a suitable infinite-dimensional catalyst may still exist.

The 2022 exact solution also proves the analogous **classical** statement for finite probability vectors, with permutations replacing unitaries and Shannon entropy replacing von Neumann entropy.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #45)](https://oqp.iqoqi.oeaw.ac.at/catalytic-entropy-conjecture)
- [Solved Quantum Problems list (shows #45 solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)

Original problem / motivation:
- P. Boes, J. Eisert, R. Gallego, M. P. Müller, and H. Wilming, **“Von Neumann Entropy from Unitarity”**, *Phys. Rev. Lett.* 122, 210402 (2019); arXiv: [1807.08773](https://arxiv.org/abs/1807.08773)

Key solution references:
- H. Wilming, **“Entropy and reversible catalysis”**, *Phys. Rev. Lett.* 127, 260402 (2021); arXiv: [2012.05573](https://arxiv.org/abs/2012.05573)
(approximate variant, as recorded on the OQP page)
- H. Wilming, **“Correlations in typicality and an affirmative solution to the exact catalytic entropy conjecture”**, *Quantum* 6, 858 (2022); arXiv: [2205.08915](https://arxiv.org/abs/2205.08915)

Related / partial results mentioned on the OQP page (useful background for a formalization roadmap):
- The original 2019 paper provides partial solutions for transitions of the form `ρ ⊗ I/d → ρ' ⊗ I/d`, and under additional assumptions on the catalyst system
- R. Duan, Y. Feng, X. Li, and M. Ying, **“Multiple-copy entanglement transformation and entanglement catalysis”**, *Phys. Rev. A* 71, 042319 (2005)
- M. Klimesh, **“Inequalities that Collectively Completely Characterize the Catalytic Majorization Relation”**, arXiv: [0709.3680](https://arxiv.org/abs/0709.3680)
- S. Turgut, **“Necessary and Sufficient Conditions for the Trumping Relation”**, arXiv: [0707.0444](https://arxiv.org/abs/0707.0444)

### Prerequisites needed

- Finite-dimensional quantum mechanics: density matrices, tensor products, partial trace, unitary conjugation
- von Neumann entropy, rank/support, spectral decompositions
- Majorization theory for spectra / probability vectors, and its equivalent formulations
- Correlating catalysts: exact preservation of the catalyst marginal while allowing final system–catalyst correlations
- Trace norm / trace distance, if formalizing the approximate 2021 version as a stepping stone
- (Useful background) catalytic majorization / trumping and the classical probability-vector analogue

### [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 Wilming’s 2022 paper and the exact solved statement in the issue, then inspect the formal-conjectures repository for related quantum, matrix, entropy, and majorization formalizations. Done means adding a formal statement of the exact catalytic entropy result, with the required finite-dimensional definitions and any supporting lemmas represented in Lean.

Written by the indexing model from the issue text.