Formalize Open Quantum Problem #38: The PPT-squared conjecture

### What is the conjecture

This is problem [#38](https://oqp.iqoqi.oeaw.ac.at/the-ppt-squared-conjecture) in the community-maintained [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

> **Problem (Open Quantum Problem #38: “The PPT-squared conjecture”).**
> Let `ρ_AB` and `ρ_CD` be quantum states with positive partial transpose (i.e. they are PPT states), and let `M` be a positive operator describing a yes/no measurement on the `BC`-system. Then consider the state on `AD`, conditional on the result of `M` being “yes”,
> `σ_AD = λ Tr_{BC}((ρ_AB ⊗ ρ_CD)(1_A ⊗ M ⊗ 1_D))`,
> where `λ` is a normalization factor.
> The conjecture states that all such `σ_AD` are separable.

A standard formalization is as follows:

* Fix finite-dimensional Hilbert spaces `H_A, H_B, H_C, H_D`.
* `ρ_AB` and `ρ_CD` are **density operators** on `H_A ⊗ H_B` and `H_C ⊗ H_D`, respectively.
* A bipartite state `ω_XY` is **PPT** iff its partial transpose is positive semidefinite:
`(id_X ⊗ T_Y)(ω_XY) ≥ 0`
(with respect to a fixed local basis on `Y`).
* A bipartite state `ω_XY` is **separable** iff it can be written as a convex combination of product states:
`ω_XY = ∑_i p_i (α_i ⊗ β_i)`,
where `p_i ≥ 0`, `∑_i p_i = 1`, and `α_i, β_i` are local density operators.
* Let `M ≥ 0` be a positive operator / postselected effect on `H_B ⊗ H_C` with nonzero success probability
`p = Tr[(ρ_AB ⊗ ρ_CD)(1_A ⊗ M ⊗ 1_D)] > 0`.
Define the postselected entanglement-swapping output
`σ_AD = p^{-1} Tr_{BC}[(ρ_AB ⊗ ρ_CD)(1_A ⊗ M ⊗ 1_D)]`.

Then the conjecture is:

* **Main conjecture:** whenever `ρ_AB` and `ρ_CD` are PPT, the swapped state `σ_AD` is always separable across the bipartition `A:D`, for every positive operator `M` with nonzero success probability.

A standard equivalent reformulation is in terms of **PPT maps** and **entanglement-breaking maps** (via the Choi–Jamiołkowski correspondence):

* A completely positive map `Φ` is **PPT** iff `T ∘ Φ` (equivalently `Φ ∘ T`) is completely positive, i.e. its Choi matrix is PPT.
* A completely positive map `Φ` is **entanglement breaking** iff its Choi matrix is separable
(equivalently, in the trace-preserving case, iff `(id ⊗ Φ)(τ)` is separable for every bipartite state `τ`).

In that language, the conjecture can be written as:

* **Equivalent map formulation:** if `Φ` and `Ψ` are PPT maps, then `Ψ ∘ Φ` is entanglement breaking.

The name “PPT-squared” comes from the especially natural special case `Ψ = Φ`, but the formulation commonly studied in the literature allows two a priori different PPT maps.

Known partial results / current open regime:

* The conjecture is known in several special cases (e.g. for maps on `M_2`, for the `n = 3` / two-qutrit case, for Gaussian channels, for all Choi-type maps, and in certain random/asymptotic regimes).
* The general finite-dimensional case remains open.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #38)](https://oqp.iqoqi.oeaw.ac.at/the-ppt-squared-conjecture)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)
* M. B. Ruskai, M. Junge, D. Kribs, P. Hayden, and A. Winter (eds.), “Operator structures in quantum information theory” (BIRS workshop report 12w5084, 2012):
[https://www.birs.ca/workshops/2012/12w5084/report12w5084.pdf](https://www.birs.ca/workshops/2012/12w5084/report12w5084.pdf)

Key related references (from the OQP page and later core literature):

* K. Horodecki, M. Horodecki, P. Horodecki, and J. Oppenheim, “Secure key from bound entanglement” (Phys. Rev. Lett. 94, 160502 (2005); arXiv: quant-ph/0309110)
(motivation: PPT states can still carry secret key)
* S. Bäuml, M. Christandl, K. Horodecki, and A. Winter, “Limitations on quantum key repeaters” (Nature Communications 6, 6908 (2015); arXiv: 1402.5927)
(explains the repeater motivation behind the conjecture)
* M. Christandl and R. Ferrara, “Private states, quantum data hiding and the swapping of perfect secrecy” (Phys. Rev. Lett. 119, 220506 (2017); arXiv: 1609.04696)
(directly related entanglement-swapping / private-state background; cited on the OQP page)
* M. Kennedy, N. A. Manor, and V. I. Paulsen, “Compositions of PPT Maps” (Quantum Inf. Comput. 18, 472–480 (2018); arXiv: 1710.08475)
(records the state-vs-map formulation, proves asymptotic results, and discusses the `2×2` case)
* B. Collins, Z. Yin, and P. Zhong, “The PPT square conjecture holds generically for some classes of independent states” (J. Phys. A 51, 425301 (2018); arXiv: 1803.00143)
(random / asymptotic evidence)
* M. Christandl, A. Müller-Hermes, and M. M. Wolf, “When Do Composed Maps Become Entanglement Breaking?” (Ann. Henri Poincaré 20, 2295–2322 (2019); arXiv: 1807.01266)
(systematic treatment; proves important special cases including dimension `3` and Gaussian channels; gives equivalent conjectures)
* L. Chen, Y. Yang, and W.-S. Tang, “Positive-partial-transpose square conjecture for n = 3” (Phys. Rev. A 99, 012337 (2019); arXiv: 1807.03636)
(independent proof of the `n = 3` / two-qutrit case; states that the case `n ≥ 4` remains open)
* S. Singh and I. Nechita, “The PPT^2 conjecture holds for all Choi-type maps” (Ann. Henri Poincaré 23, 3311–3329 (2022); arXiv: 2011.03809)
(proves the conjecture for a large structured family of maps including Choi-type maps)

(If you want to include a brief “recent progress” pointer section, see also Sang-Jun Park, “`k`-Positivity and high-dimensional bound entanglement under symplectic group symmetry” (arXiv:2602.09860, 2026), which proves the conjecture for symplectic-covariant / conjugate-symplectic-covariant PPT maps. But the references above are already enough for writing the issue.)

### Prerequisites needed

* Finite-dimensional quantum mechanics: density matrices, tensor products, partial trace, postselected measurements / POVM effects
* Separability vs entanglement; convex decompositions into product states
* Partial transpose and the PPT criterion
* Quantum channels / completely positive maps and the Choi–Jamiołkowski correspondence
* Linear algebra / matrix analysis: positive semidefinite operators, transpose, tensor products, traces
* (Optional) Positive maps, decomposable maps, entanglement-breaking maps, and Schmidt number methods

### [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 entry point is named in the issue; first inspect existing formalized conjectures and the repository's contribution conventions. The work is done when the PPT-squared conjecture is added as a checked Lean formalization with the necessary supporting definitions and proofs.

Written by the indexing model from the issue text.