Formalize Open Quantum Problem #42: Reversible dynamics on composite systems

### What is the conjecture

This is problem [#42](https://oqp.iqoqi.oeaw.ac.at/reversible-dynamics-on-composite-systems) in the [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems). According to the OQP master list, it was added in 2017 by B. Dakić and M. Müller.

> **Problem (Open Quantum Problem #42: “Reversible dynamics on composite systems”).**
> Consider two state spaces `Ω_A, Ω_B` such that the reversible transformations `G_A` and `G_B` are transitive on the pure states.
> Given any (locally-tomographic) composite state space `Ω_AB` as just described, suppose that there exists any reversible transformation `T_AB` which is not of the form `T_A ⊗ T_B` (that is, a transformation that reversibly creates correlations).
> Prove, or disprove by counterexample, that this state space must then be embeddable into standard quantum theory.

`*` Here “transitive on the pure states” means that every pure state can be mapped to every other by a suitable reversible transformation.

A standard formalization is in the language of **finite-dimensional generalized probabilistic theories (GPTs)**:

* A system `A` is a compact convex set of normalized states `Ω_A` affinely spanning a finite-dimensional real vector space `V_A`.
* The **pure states** of `A` are the extreme points of `Ω_A`.
* A **reversible transformation** of `A` is an affine automorphism of `Ω_A`; after fixing an affine embedding, this is a linear map `T : V_A → V_A` with `T(Ω_A)=Ω_A`. The reversible transformations form a group `G_A`.
* The hypothesis that `G_A` is **transitive on pure states** means: for any pure `α, α' ∈ Ω_A`, there exists `T ∈ G_A` with `T(α)=α'`.
* A **locally-tomographic composite** of systems `A` and `B` is a composite GPT `AB` whose normalized state space `Ω_AB` lives in `V_A ⊗ V_B`, contains product states `α ⊗ β`, product measurements, and product reversible transformations `T_A ⊗ T_B`, and whose global states are completely determined by local/product measurement statistics.
* A reversible transformation `T_AB ∈ G_AB` is **non-product** / **genuinely global** iff it is not of the form `T_A ⊗ T_B`. These are the reversible dynamics beyond independent local evolution; typical examples can create correlations or entanglement from product inputs.

With this setup, the problem can be read as:

* **Main question / open classification problem:** classify the locally-tomographic GPT composites with pure-state-transitive local reversible groups that admit at least one genuinely global reversible transformation.
* **Conjectural answer:** every such example is **embeddable into ordinary finite-dimensional complex quantum theory**; equivalently, there should be no non-quantum counterexample satisfying the stated assumptions.

A natural formal meaning of “**embeddable into standard quantum theory**” is:

* there exist finite-dimensional complex Hilbert spaces `H_A, H_B` and an affine/operational embedding of the GPT into the usual quantum state spaces `D(H_A)`, `D(H_B)`, and `D(H_A ⊗ H_B)`,
* preserving convex mixtures, product structure, and reversible transformations.
(Depending on the preferred formalization target, one can ask to preserve only state spaces and reversible dynamics, or the full GPT data of states, effects, and transformations.)

The word **“embeddable”** is essential: the conjecture is not that the theory must literally *equal* full quantum theory. Classical probability theory already has pure-state-transitive reversible dynamics and non-product reversible gates such as classical CNOT, while still being representable inside complex quantum theory.

Natural sub-problems / special cases highlighted in the existing literature are:

* Prove the conjecture under extra assumptions such as **continuity** or **connectedness** of the reversible transformation group.
* Solve the problem for important model local state spaces, especially **Bloch-ball / g-bit** systems.
* Determine whether every interacting example is either standard complex quantum theory itself or a subtheory already embeddable in it.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #42)](https://oqp.iqoqi.oeaw.ac.at/reversible-dynamics-on-composite-systems)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)
* Closely related precursor / strong special case:
G. de la Torre, L. Masanes, A. J. Short, and M. P. Müller, “Deriving Quantum Theory from Its Local Structure and Reversibility” (Phys. Rev. Lett. 109, 090403 (2012); arXiv:1110.5482):
[https://arxiv.org/abs/1110.5482](https://arxiv.org/abs/1110.5482)

Key related references (as listed on the OQP page, plus one updated later citation):

* J. Barrett, “Information processing in generalized probabilistic theories” (Phys. Rev. A 75, 032304 (2007))
(standard GPT formalism)
* L. Hardy, “Quantum Theory From Five Reasonable Axioms” (arXiv: quant-ph/0101012)
(standard source for tomographic locality in reconstruction-style axiomatizations)
* D. Gross, M. Müller, R. Colbeck, and O. C. O. Dahlsten, “All reversible dynamics in maximally non-local theories are trivial” (Phys. Rev. Lett. 104, 080402 (2010))
(boxworld / maximally nonlocal theories admit only trivial reversible dynamics)
* S. W. Al-Safi and A. J. Short, “Reversible Dynamics in Strongly Non-Local Boxworld Systems” (J. Phys. A 47, 325303 (2014))
(stronger no-go results for reversible dynamics in boxworld-type theories)
* S. W. Al-Safi and J. Richens, “Reversibility and the structure of the local state space” (New J. Phys. 17, 123001 (2015))
(constraints on which local state spaces can support nontrivial reversible dynamics)
* J. G. Richens, J. H. Selby, and S. W. Al-Safi, “Entanglement is an inevitable feature of any non-classical theory” (arXiv: 1610.00682; journal version: *Entanglement Is Necessary for Emergent Classicality in All Physical Theories*, Phys. Rev. Lett. 119, 080503 (2017))
(shows that natural reversible-interaction assumptions force entanglement in broad GPT settings)
* Ll. Masanes, M. P. Müller, D. Pérez-García, and R. Augusiak, “Entanglement and the three-dimensionality of the Bloch ball” (J. Math. Phys. 55, 122203 (2014))
(for two Bloch-ball systems, only the quantum `d=3` case admits a locally-tomographic interacting composite)
* M. Krumm and M. P. Müller, “Quantum computation is the unique reversible circuit model for which bits are balls” (npj Quantum Inf. 5, 7 (2019))
(updates the OQP page’s older “in preparation” citation and extends the Bloch-ball no-go to arbitrary numbers of gbits)
* L. Hardy and W. K. Wootters, “Limited Holism and Real-Vector-Space Quantum Theory” (Found. Phys. 42(3), 454–473 (2012))
(important non-locally tomographic example)
* H. Barnum, M. A. Graydon, and A. Wilce, “Some Nearly Quantum Theories” (EPTCS 195, 59–70 (2015))
(Jordan-algebraic / nearly quantum examples)
* H. Barnum, M. A. Graydon, and A. Wilce, “Composites and Categories of Euclidean Jordan Algebras” (Quantum 4, 359 (2020); arXiv: 1606.09331)
(further structured families of nearly-quantum composite theories)

### Prerequisites needed

* Finite-dimensional convex geometry: compact convex sets, extreme points, affine maps, convex hulls
* Linear algebra over real vector spaces, tensor products, and duality/effect spaces
* Group actions / basic Lie groups: automorphism groups, transitivity on pure states
* Generalized probabilistic theories: states, effects, reversible transformations, composites, local tomography
* Basic quantum information / quantum foundations: density matrices, unitary dynamics, entangling gates, classical vs quantum reversible computation
* (Optional) Order-unit spaces / cones, Euclidean Jordan algebras, and stabilizer-like subtheories

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-81 (Quantum theory)
* ams-52 (Convex and discrete geometry)
* ams-20 (Group theory and generalizations)
* ams-15 (Linear and multilinear algebra; matrix 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 the Open Quantum Problems entry for Problem #42 and the cited precursor literature to determine a precise formal statement. Then inspect existing formalized conjectures in the repository and its Lean project structure; done means adding a reviewed formal conjecture that matches the repository’s conventions and captures the intended GPT claim.

Written by the indexing model from the issue text.