Formalize Open Quantum Problem #9: Reduction criterion implies majorization?

---
### What is the conjecture

This is problem [#9](https://oqp.iqoqi.oeaw.ac.at/reduction-criterion-implies-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).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (solved by T. Hiroshima, 2003; see below for the reference).

> **Problem (Open Quantum Problem #9: “Reduction criterion implies majorization?”).**
> The density matrix of any separable bipartite state is majorized by its reductions (Nielsen–Kempe).
> How does this **majorization criterion** fit into the standard implication chain of separability/entanglement criteria?
> In particular: does the **reduction criterion** imply the **majorization** criterion?

Concretely, let `ρ_AB` be a bipartite density operator on `H_A ⊗ H_B` (finite-dimensional), with reduced states
`ρ_A = tr_B(ρ_AB)` and `ρ_B = tr_A(ρ_AB)`.

**(1) Reduction criterion.**
`ρ_AB` satisfies the reduction criterion if both operator inequalities hold:
- `ρ_A ⊗ I_B − ρ_AB ≥ 0`,
- `I_A ⊗ ρ_B − ρ_AB ≥ 0`.

Equivalently, in positive-map language, letting the **reduction map** be `R(X) = tr(X) I − X`,
the criterion is `(id ⊗ R)(ρ_AB) ≥ 0` and `(R ⊗ id)(ρ_AB) ≥ 0`.

**(2) Majorization criterion.**
Let `λ(ρ)` denote the vector of eigenvalues of `ρ`, sorted in non-increasing order. For vectors `p, q ∈ ℝ^d`
with the same sum, write `p ≺ q` (majorization) if for all `k = 1,…,d`,
`∑_{i=1}^k p_i^↓ ≤ ∑_{i=1}^k q_i^↓` (and equality at `k = d`).

To compare `λ(ρ_AB)` (length `d_A d_B`) with `λ(ρ_A)` (length `d_A`), one can pad the shorter vector with zeros
to length `d_A d_B` (equivalently, work with the standard “weak submajorization” conventions used in the OQP discussion).

Then the **majorization criterion** is:
- `λ(ρ_AB) ≺ λ(ρ_A)` (after padding to equal length),
- `λ(ρ_AB) ≺ λ(ρ_B)` (after padding to equal length).

This is known to hold for **separable** states (`ρ_AB` separable ⇒ majorization holds).

**Original open question (now solved):**
- Does `reduction(ρ_AB)` imply `majorization(ρ_AB)`?

**Solved statement to formalize (Hiroshima, 2003):**
- **Theorem:** If `ρ_AB` satisfies the reduction criterion, then it satisfies the majorization criterion:
`λ(ρ_AB) ≺ λ(ρ_A)` and `λ(ρ_AB) ≺ λ(ρ_B)` (with the standard padding/weak-majorization convention).
- As a consequence, violation of the majorization criterion gives a **sufficient condition for distillability**
(since violation of majorization implies violation of the reduction criterion, and violation of reduction implies distillability).

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #9)](https://oqp.iqoqi.oeaw.ac.at/reduction-criterion-implies-majorization)
- [Solved Quantum Problems list (marks #9 as solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
- O. Krüger & R. F. Werner, “Some Open Problems in Quantum Information Theory” (Problem 9):
[https://arxiv.org/abs/quant-ph/0504166](https://arxiv.org/abs/quant-ph/0504166)

Key references mentioned on the problem page:
- M. A. Nielsen and J. Kempe, “Separable States Are More Disordered Globally than Locally”
(Phys. Rev. Lett. 86, 5184 (2001); arXiv: quant-ph/0011117)
- A. Peres, “Separability Criterion for Density Matrices”
(Phys. Rev. Lett. 77, 1413 (1996); arXiv: quant-ph/9604005)
- M. Horodecki, P. Horodecki, and R. Horodecki,
“Mixed-State Entanglement and Distillation: Is there a ‘Bound’ Entanglement in Nature?”
(Phys. Rev. Lett. 80, 5239 (1998); arXiv: quant-ph/9801069)
- M. Horodecki and P. Horodecki,
“Reduction criterion of separability and limits for a class of distillation protocols”
(Phys. Rev. A 59, 4206 (1999); arXiv: quant-ph/9708015)
- K. G. H. Vollbrecht and M. M. Wolf,
“Conditional entropies and their relation to entanglement criteria”
(arXiv: quant-ph/0202058) — partial progress via conditional Rényi entropies
- **Solution reference:**
T. Hiroshima, “Majorization criterion for distillability of a bipartite quantum state”
(Phys. Rev. Lett. 91, 057902 (2003); arXiv: quant-ph/0303057)

### Prerequisites needed
- Finite-dimensional quantum mechanics: density matrices, tensor products, partial trace
- Linear algebra / matrix analysis: Hermitian/PSD operators, eigenvalues, operator inequalities
- Majorization theory: sorted partial sums, (sub-)stochastic matrices, equivalent characterizations
- Basic entanglement/separability criteria: separability, PPT, reduction criterion, (optionally) distillability

### [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, tests, or entry points. Start by reading Hiroshima's solution reference and the stated definitions of the reduction and majorization criteria, then inspect the repository for related formalizations. Done means adding a Lean statement and proof of both majorization conclusions from the reduction criterion, including the stated padding convention.

Written by the indexing model from the issue text.