Open Quantum Problem 13: Mutually unbiased bases

The question

mutuallyUnbiasedBases_dim6. Special case in dimension $6$: determine the maximal number of mutually unbiased orthonormal bases in ${\mathbb{C}}^6$.

mutuallyUnbiasedBases_dim10. Special case in dimension $10$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in ${\mathbb{C}}^{10}$.

mutuallyUnbiasedBases_dim12. Special case in dimension $12$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in ${\mathbb{C}}^{12}$.

mutuallyUnbiasedBases_dim14. Special case in dimension $14$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in ${\mathbb{C}}^{14}$.

mutuallyUnbiasedBases_dim15. Special case in dimension $15$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in ${\mathbb{C}}^{15}$.

mutuallyUnbiasedBases. Open Quantum Problem 13: determine the maximal number of mutually unbiased orthonormal bases in ${\mathbb{C}}^d$ for $d\ge 2$.

Mathematical problem

For each integer $d\ge 2$, determine the maximum number $k$ for which there exist orthonormal bases ${\mathcal{B}}_1,\dots ,{\mathcal{B}}_k$ of the complex Hilbert space ${\mathbb{C}}^d$ such that any two distinct bases are mutually unbiased.

Concretely, if ${\mathcal{B}}_r=\{e_0^{(r)},\dots ,e_{d-1}^{(r)}\}$ and ${\mathcal{B}}_s=\{e_0^{(s)},\dots ,e_{d-1}^{(s)}\}$, then ${\mathcal{B}}_r$ and ${\mathcal{B}}_s$ are mutually unbiased if for all $i,j$ and all $r\ne s$, $|⟨e_i^{(r)},e_j^{(s)}⟩|=d^{-1/2}$.

The problem is therefore to determine the maximal value $\mu(d) := \max \{ k : \text{there exist } k \text{ pairwise mutually unbiased orthonormal bases in } \mathbb{C}^d \}$.

In this file, an orthonormal basis is represented by a unitary matrix whose columns are the basis vectors. For two such bases U and V, the matrix relativeUnitary U V, which is $U^{†}V$, contains all cross-basis overlaps as its entries. Since Lean works more smoothly with squared norms, we formalize mutual unbiasedness by requiring $\Vert (relativeUnitaryUV{)}_{ij}{\Vert }^2=1/d$ for all $i,j$, which is equivalent to $|⟨e_i^{(r)},e_j^{(s)}⟩|=d^{-1/2}$.

Background

Mutually unbiased bases are a basic structure in finite-dimensional quantum theory. They arise in quantum state determination, quantum tomography, quantum cryptography, finite geometry, and combinatorics.

A general upper bound is $\mu (d)\le d+1$. Equality is known when $d$ is a prime power, via constructions over finite fields. For composite dimensions that are not prime powers, the exact value of $\mu (d)$ is in general open.

The smallest and most famous unresolved case is $d=6$. The IQOQI OQP page emphasizes this dimension in particular: although many equivalent reformulations are known, no construction yielding more than three mutually unbiased bases in dimension six is known.

What this file formalizes

This file is organized around the quantity IsMaxMUBCount d k, which expresses that $k$ is the maximum number of mutually unbiased orthonormal bases in dimension $d$.

• the open theorem mutuallyUnbiasedBases expresses the full problem for all $d\ge 2$;
• the open theorem mutuallyUnbiasedBases_dim6 expresses the especially important case $d=6$;
• the solved theorem mutuallyUnbiasedBases_dim2 proves the qubit case $\mu (2)=3$.

References

Primary source list entry:

• IQOQI Vienna Open Quantum Problems, problem 13: https://oqp.iqoqi.oeaw.ac.at/mutually-unbiased-bases
• Master list of open quantum problems: https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems

Foundational papers

• I. D. Ivanović, Geometrical description of quantal state determination, J. Phys. A 14, 3241-3245 (1981).
• W. K. Wootters and B. D. Fields, Optimal state-determination by mutually unbiased measurements, Ann. Phys. 191, 363-381 (1989).

General constructions and surveys

• A. Klappenecker and M. Rötteler, Constructions of mutually unbiased bases, in Finite Fields and Applications, LNCS 2948 (2004).

Dimension six and the maximal-number problem

• M. Grassl, On SIC-POVMs and MUBs in Dimension 6, arXiv:quant-ph/0406175 (2004).
• P. Butterley and W. Hall, Numerical evidence for the maximum number of mutually unbiased bases in dimension six, Phys. Lett. A 369, 5-8 (2007), arXiv:quant-ph/0701122.
• S. Brierley and S. Weigert, Maximal Sets of Mutually Unbiased Quantum States in Dimension Six, Phys. Rev. A 78, 042312 (2008), arXiv:0808.1614.
• P. Raynal, X. Lü, and B.-G. Englert, Mutually unbiased bases in dimension six: The four most distant bases, Phys. Rev. A 83, 062303 (2011), arXiv:1103.1025.

Remark on the status of $d=6$

The dimension-six case is not known to be solved. At present, the best-known general picture is:

• $3\le \mu (6)\le 7$,
• complete sets of $7$ MUBs are not known,
• and several analytic and numerical works give strong evidence that one cannot go beyond $3$.

This is why the theorem mutuallyUnbiasedBases_dim6 is marked as an open research statement.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OpenQuantumProblems.«13» (6 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem mutuallyUnbiasedBases_dim6 :
    IsMaxMUBCount 6 (answer(sorry))

theorem mutuallyUnbiasedBases_dim10 :
    IsMaxMUBCount 10 (answer(sorry))

theorem mutuallyUnbiasedBases_dim12 :
    IsMaxMUBCount 12 (answer(sorry))

theorem mutuallyUnbiasedBases_dim14 :
    IsMaxMUBCount 14 (answer(sorry))

theorem mutuallyUnbiasedBases_dim15 :
    IsMaxMUBCount 15 (answer(sorry))

theorem mutuallyUnbiasedBases (d : ℕ) (hd : 2 ≤ d) :
    IsMaxMUBCount d ((answer(sorry) : ℕ → ℕ) d)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Source and licence

Imported from Formal Conjectures (Open quantum problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.