Formalize Open Quantum Problem #37: Stronger submultiplicativity for the diamond norm

### What is the conjecture

This is problem [#37](https://oqp.iqoqi.oeaw.ac.at/stronger-submultiplicativity-for-the-diamond-norm) in the [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

> **Problem (Open Quantum Problem #37: “Stronger submultiplicativity for the diamond norm”).**
> Does there exist an absolute constant `α < 1` such that the submultiplicativity statement
> `||Θ ∘ (id - T)||_⋄ ≤ α ||Θ||_⋄ ||id - T||_⋄`
> holds for all quantum channels `T` over any finite-dimensional Hilbert space?
> Here `Θ` denotes the transposition map, so `||Θ||_⋄` equals the Hilbert space dimension.

A standard formalization is as follows:

* Fix a finite-dimensional complex Hilbert space `H ≅ C^d`.
* Let `L(H)` denote the space of linear operators on `H`.
* A quantum channel is a linear map `T : L(H) → L(H)` that is completely positive and trace preserving (CPTP).
* `id = id_H : L(H) → L(H)` is the identity superoperator.
* Fix an orthonormal basis of `H`, and let `Θ = Θ_H : L(H) → L(H)` be the associated transposition map, `Θ(X) = X^T`.
* For a linear map `Φ : L(H) → L(H)`, its **diamond norm** is
`||Φ||_⋄ := sup_n sup_{X : ||X||_1 ≤ 1} ||(Φ ⊗ id_n)(X)||_1`,
and in finite dimensions one may take `n = d`.

Ordinary submultiplicativity of the diamond norm always gives
`||Θ ∘ (id - T)||_⋄ ≤ ||Θ||_⋄ ||id - T||_⋄`,
so the problem asks whether one gets a **uniform strict improvement** on the special family of maps of the form `id - T`, where `T` is a quantum channel.

Equivalently, since `||Θ||_⋄ = d`, the question is:

* **Main question:** does there exist a universal constant `α < 1` such that for every `d` and every channel
`T : L(C^d) → L(C^d)`,
one has
`||Θ_d ∘ (id_d - T)||_⋄ ≤ α d ||id_d - T||_⋄` ?

A natural formalization target is to define the optimal dimension-`d` constant
`α(d) := sup_T ||Θ_d ∘ (id_d - T)||_⋄ / (||Θ_d||_⋄ ||id_d - T||_⋄)`,
where the supremum runs over all quantum channels `T` on `L(C^d)`.
Then the open problem becomes:

* **Dimension-independent version:** is
`α_* := sup_{d ≥ 1} α(d)`
strictly less than `1`?

This matters because the OQP page explains that Holevo–Werner’s upper bound on `ε`-quantum capacity,
`Q_ε(C) ≤ log ||Θ ∘ C||_⋄` for `ε < 1/2`,
uses only the ordinary submultiplicativity case `α = 1`.
If some universal `α < 1` existed, the same argument would extend to a larger error regime
`ε ∈ [0, 1/(2α))`.
The original hope was `α = 1/2`, which would have yielded a strong converse rate via that route.

Known partial results / subproblems highlighted on the OQP page:

* For each fixed dimension `d`, some constant `α(d) < 1` exists by continuity/compactness arguments.
* For qubit-qubit channels (`d = 2`), one has
`||id - T||_⋄ = ||Θ ∘ (id - T)||_⋄`,
so the exact best constant is `α(2) = 1/2`.
* For channels symmetric with respect to the orthogonal group `O(d)` or with `SU(2)` symmetry at input and output, the inequality holds with `α = 1/2`.
* Random testing in dimensions at least `3` found examples requiring `α > 1/2`.
* For unitarily implemented channels `T(ρ) = U ρ U^*`, analytic lower bounds imply that asymptotically one needs `α > 0.63`.
* A natural sharpened goal is therefore to determine the exact universal optimum `α_*`.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #37)](https://oqp.iqoqi.oeaw.ac.at/stronger-submultiplicativity-for-the-diamond-norm)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)

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

* A. S. Holevo and R. F. Werner, “Evaluating capacities of bosonic Gaussian channels” (Phys. Rev. A 63, 032312 (2001); arXiv: quant-ph/9912067)
* https://arxiv.org/abs/quant-ph/9912067
* J. Watrous, “Simpler semidefinite programs for completely bounded norms” (Chicago Journal of Theoretical Computer Science 2013, 08, 1–19; arXiv: 1207.5726)
* https://arxiv.org/abs/1207.5726
* D. Fischer, “Quantum capacity bounds via semidefinite programming” (Bachelor’s Thesis, Leibniz University of Hannover, 2016)
* A. Müller-Hermes, D. Reeb, and M. M. Wolf, “Positivity of linear maps under tensor powers” (J. Math. Phys. 57, 015202 (2016); arXiv: 1502.05630)
* https://arxiv.org/abs/1502.05630

Important recent progress / possible resolution:

* H. Cha, “A dimension-independent strict submultiplicativity for the transposition map in diamond norm” (arXiv: 2602.17748, 2026)
* https://arxiv.org/abs/2602.17748
(claims a full affirmative solution with explicit `α = 1/√2`; if correct, this resolves the problem, not peer-reviewed yet)

### Prerequisites needed

* Finite-dimensional quantum information theory: quantum channels (CPTP maps), superoperators, composition
* Trace norm `||·||_1` and the diamond norm / completely bounded trace norm
* Linear algebra / matrix analysis: transposition, adjoints, unitary conjugation
* Basic operator theory / functional analysis of normed spaces of linear maps
* (Optional) Semidefinite-programming formulations of the diamond norm
* (Optional) Quantum channel capacity notions, for the motivation from the Holevo–Werner bound

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

* ams-81 (Quantum theory)
* ams-46 (Functional analysis)
* 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 files, tests, or Lean entry points are named. Start by reviewing the Open Quantum Problems page and the cited references, then inspect existing formalized conjectures in this repository for conventions. Done would require adding a Lean statement and supporting formalization for the stated diamond-norm conjecture, but the mathematical problem remains open.

Written by the indexing model from the issue text.