Formalize Open Quantum Problem #6: Nice error bases

### What is the conjecture

This is problem [#6](https://oqp.iqoqi.oeaw.ac.at/nice-error-bases) 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 (negative answer / counterexample by Klappenecker–Rötteler).

> **Problem (Open Quantum Problem #6: “Nice error bases”).**
> There are two special constructions to obtain orthogonal bases of unitaries (unitary error bases).
> Decide whether every **nice error basis** is of **shift-and-multiply type**.

Concretely, fix a dimension `d ≥ 1` and let `H = ℂ^d`. A **unitary error basis** is a family of `d^2` unitary operators
`{U_i}_{i=1,…,d^2} ⊂ U(d)`
such that they are orthogonal with respect to the Hilbert–Schmidt inner product:
`tr(U_i^* U_j) = d · δ_{ij}`.

There are two commonly used extra structures:

1. **Nice error bases (Knill).**
One requires closure under multiplication *up to phase*: for any basis elements `U_i, U_j`, their product is proportional to another basis element:
`U_i U_j = phase · U_k`.
The induced label-composition `(i,j) ↦ k` defines a finite **index group** (equivalently: a nice error basis is a faithful irreducible **projective representation** of a group of order `d^2`, with suitable normalization conventions).

2. **Shift-and-multiply type (Werner).**
One requires that in some choice of computational basis, the basis unitaries are generated by:

* `d` **permutation** operators (“shifts”), and
* `d` **diagonal** “multiplication” operators,
so that the whole error basis consists of their products. Equivalently, these bases are **monomial**: each unitary matrix has exactly one nonzero entry in each row and each column.

The question posed on the OQP page is:

* **Open question (now solved):** Is every **nice error basis** (up to the standard notion of equivalence, e.g. change of basis by a fixed unitary and relabeling/phases) of **shift-and-multiply type**?

**Solved statement to formalize (Klappenecker–Rötteler, 2003):** the answer is **no** — there exists a **nice error basis** that is **not** of shift-and-multiply type (equivalently: there exists a nice error basis that is **not monomial**).

---

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site (Problem #6)](https://oqp.iqoqi.oeaw.ac.at/nice-error-bases)
* [Solved Quantum Problems list (marks #6 as solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
* [Werner / Krüger–Werner arXiv list (2005)](https://arxiv.org/abs/quant-ph/0504166) (see “Problem 6”)

Key references (as cited on the OQP page):

* A. Klappenecker and M. Rötteler, “Beyond Stabilizer Codes I: Nice Error Bases” (2000), arXiv: [quant-ph/0010082](https://arxiv.org/abs/quant-ph/0010082)
* E. Knill, “Group Representations, Error Bases and Quantum Codes” (1996), arXiv: [quant-ph/9608049](https://arxiv.org/abs/quant-ph/9608049)
* R. F. Werner, “All Teleportation and Dense Coding Schemes” (2000), arXiv: [quant-ph/0003070](https://arxiv.org/abs/quant-ph/0003070)
* **Solution / negative answer:**
A. Klappenecker and M. Rötteler, “On the Monomiality of Nice Error Bases” (2003), arXiv: [quant-ph/0301078](https://arxiv.org/abs/quant-ph/0301078)

---

### Prerequisites needed

* Linear algebra over `ℂ`: unitary matrices, adjoint, trace, matrix entries
* Operator inner products: Hilbert–Schmidt inner product and orthonormal operator bases
* Basic quantum information motivation: teleportation / dense coding / error bases as operator bases
* Finite group theory and representations:

* projective representations and 2-cocycles (for “nice” error bases),
* monomial representations / monomial matrices (for shift-and-multiply)
* (Optional, for the shift-and-multiply construction details) combinatorics:

* Latin squares (“squares”),
* complex Hadamard matrices

---

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

* ams-81 (Quantum theory)
* ams-20 (Group theory and generalizations)
* 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

---

Start by reading the Klappenecker–Rötteler paper “On the Monomiality of Nice Error Bases” and the cited definitions of nice and shift-and-multiply error bases. Formalize the negative statement that a nice error basis exists which is not monomial, with the repository’s existing quantum and group-theory conventions. Done means the theorem is stated and accepted by the Lean project.

Written by the indexing model from the issue text.