Formalize Open Quantum Problem #41: All rank inequalities for reduced states of quadripartite quantum states

### What is the conjecture

This is problem [#41](https://oqp.iqoqi.oeaw.ac.at/all-rank-inequalities-for-reduced-states-of-quadripartite-quantum-states) in the [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

> **Problem (Open Quantum Problem #41: “All rank inequalities for reduced states of quadripartite quantum states”).**
> Given any tripartite density matrix `ρ_{ABC}`, let
> `r_{AB} = rank(Tr_C(ρ_{ABC}))`
> denote the rank of the corresponding marginal. Prove or find a counterexample to the following hypothesis:
> `r_{AB} ≤ r_{AC} r_{BC}`.

A standard formalization is as follows:

* Fix finite-dimensional complex Hilbert spaces `H_A`, `H_B`, `H_C`.
* A tripartite mixed state is a density operator `ρ_{ABC}` on `H_A ⊗ H_B ⊗ H_C` (positive semidefinite, trace `1`).
* For each subsystem `X ⊆ {A,B,C}`, write `ρ_X` for the reduced state obtained by partial trace over the complementary parties, and define
`r_X := rank(ρ_X)`.
* The singled-out conjectured inequality is
`r_{AB} ≤ r_{AC} r_{BC}`.
* Since the 0-Rényi entropy is `S_0(ρ) = log rank(ρ)`, the same conjecture can be written additively as
`S_0(AB) ≤ S_0(AC) + S_0(BC)`.

The problem is often viewed through **purifications** to four-party pure states:

* every tripartite mixed state `ρ_{ABC}` admits a purification `|ψ⟩_{ABCD}`,
* for pure four-party states, complementary subsystem ranks agree (`r_X = r_{X^c}`),
* and the conjecture is equivalently expressible (up to relabeling/complements) in the form highlighted by Cadney–Huber–Linden–Winter:
`r_{BC} ≤ r_{AB} r_{AC}` for every pure state `|ψ⟩_{ABCD}`.

This is why the OQP title is about **reduced states of quadripartite quantum states**, even though the explicit hypothesis is stated for a tripartite mixed state.

The broader classification problem is:

* **Main question / rank-inequality classification problem:** determine all universal multiplicative inequalities among the ranks of reduced states of four-party quantum states, equivalently all universal **linear** inequalities among the 0-Rényi entropies `S_0(X)=log r_X`.

Cadney–Huber–Linden–Winter showed that several families of four-party linear `S_0`-inequalities are always valid, including

* `S_0(A) ≥ 0`,
* `S_0(A) + S_0(B) ≥ S_0(AB)`,
* `S_0(AB) + S_0(AC) ≥ S_0(A)`,
* `S_0(AB) + S_0(AC) + S_0(BC) ≥ 2 S_0(A)`,

together with all versions obtained by permuting parties (and, more generally, substituting pairwise disjoint subsets of parties). They further showed that completeness of the four-party linear rank-inequality picture would follow from the conjectured inequality above.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #41)](https://oqp.iqoqi.oeaw.ac.at/all-rank-inequalities-for-reduced-states-of-quadripartite-quantum-states)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)
* J. Cadney, M. Huber, N. Linden, and A. Winter, “Inequalities for the Ranks of Quantum States”
(introduces the conjectured missing four-party rank inequality / 0-entropy inequality):
* [https://arxiv.org/abs/1308.0539](https://arxiv.org/abs/1308.0539)

Important later update / likely resolution:

* Z. Song, L. Chen, Y. Sun, and M. Hu, “A complete picture of the four-party linear inequalities in terms of the 0-entropy”
(claims to prove the conjectured inequality and complete the classification):
* [https://arxiv.org/abs/2105.07679](https://arxiv.org/abs/2105.07679)

Key related references (as listed on the OQP page):

* E. H. Lieb and M.-B. Ruskai, “Proof of the strong subadditivity of quantum-mechanical entropy” (J. Math. Phys. 14:1938–1941 (1973))
* N. Linden, M. Mosonyi, and A. Winter, “The structure of Renyi entropic inequalities” (Proc. R. Soc. A 469(2158):20120737 (2013); arXiv: 1212.0248)
* N. Pippenger, “The inequalities of quantum information theory” (IEEE Trans. Inf. Theory 49(4):773–789 (2003))
* R. W. Yeung and Z. Zhang, “On Characterization of Entropy Function via Information Inequalities” (IEEE Trans. Inf. Theory 44(4):1440–1452 (1998))
* N. Linden and A. Winter, “A New Inequality for the von Neumann Entropy” (Commun. Math. Phys. 259:129–138 (2005); arXiv: quant-ph/0406162)

### Prerequisites needed

* Finite-dimensional quantum mechanics: density matrices, tensor products, partial trace, purification
* Reduced states and their ranks; Schmidt rank across bipartitions of pure states
* Rényi-0 entropy (`S_0 = log rank`) and the entropy-vector viewpoint
* Linear algebra / matrix analysis: rank inequalities, tensor/Kronecker products, support subspaces
* (Optional) Convex-cone / extremal-ray language for entropy or log-rank vectors

### [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-47 (Operator 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

---

No repository file, test, or Lean entry point is named in the issue. Start by reading the Open Quantum Problems statement and the Cadney–Huber–Linden–Winter and Song et al. references, then identify the repository's conventions for formalized conjectures; done means the stated rank inequality is formally added with the required proof or appropriately documented result.

Written by the indexing model from the issue text.