Open Quantum Problem 13: Mutually unbiased bases

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$, $|\langle e_i^{(r)}, e_j^{(s)} \rangle| = 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^\dagger V$, contains all cross-basis overlaps as its entries. Since Lean works more smoothly with squared norms, we formalize mutual unbiasedness by requiring $\| (relativeUnitary\ U\ V)_{ij} \|^2 = 1 / d$ for all $i, j$, which is equivalent to $|\langle e_i^{(r)}, e_j^{(s)} \rangle| = 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.

@[reducible, inline]

abbrev OpenQuantumProblem13.UMat (d : ℕ) : Type

A unitary matrix representing an orthonormal basis of $\mathbb{C}^d$ via its columns.

Equations

• OpenQuantumProblem13.UMat d = ↥(Matrix.unitaryGroup (Fin d) ℂ)

def OpenQuantumProblem13.relativeUnitary {d : ℕ} (U V : UMat d) : Matrix (Fin d) (Fin d) ℂ

The relative unitary between two bases.

Equations

• OpenQuantumProblem13.relativeUnitary U V = star ↑U * ↑V

def OpenQuantumProblem13.IsUnbiased {d : ℕ} (U V : UMat d) : Prop

Two unitary matrices represent mutually unbiased bases if every entry of the relative unitary has squared norm $1 / d$.

Equations

• OpenQuantumProblem13.IsUnbiased U V = ∀ (i j : Fin d), ‖OpenQuantumProblem13.relativeUnitary U V i j‖ ^ 2 = (↑d)⁻¹

theorem OpenQuantumProblem13.IsUnbiased.symm {d : ℕ} {U V : UMat d} (hUV : IsUnbiased U V) : IsUnbiased V U

Mutual unbiasedness is symmetric.

def OpenQuantumProblem13.IsMUBFamily {d k : ℕ} (B : Fin k → UMat d) : Prop

A family of unitary matrices is a family of mutually unbiased bases if every two distinct members are unbiased.

Equations

• OpenQuantumProblem13.IsMUBFamily B = Pairwise fun (m n : Fin k) => OpenQuantumProblem13.IsUnbiased (B m) (B n)

def OpenQuantumProblem13.HasMUBs (d k : ℕ) : Prop

There exist $k$ mutually unbiased bases in $\mathbb{C}^d$.

Equations

• OpenQuantumProblem13.HasMUBs d k = ∃ (B : Fin k → OpenQuantumProblem13.UMat d), OpenQuantumProblem13.IsMUBFamily B

def OpenQuantumProblem13.HasCompleteMUBs (d : ℕ) : Prop

There exists a complete set of $d + 1$ mutually unbiased bases in $\mathbb{C}^d$.

Equations

• OpenQuantumProblem13.HasCompleteMUBs d = OpenQuantumProblem13.HasMUBs d (d + 1)

def OpenQuantumProblem13.IsMaxMUBCount (d k : ℕ) : Prop

$k$ is the maximal size of a family of mutually unbiased bases in dimension $d$.

Equations

• OpenQuantumProblem13.IsMaxMUBCount d k = (OpenQuantumProblem13.HasMUBs d k ∧ ∀ (m : ℕ), OpenQuantumProblem13.HasMUBs d m → m ≤ k)

theorem OpenQuantumProblem13.hasMUBs_zero (d : ℕ) : HasMUBs d 0

Every dimension admits the empty family of mutually unbiased bases.

theorem OpenQuantumProblem13.hasMUBs_one (d : ℕ) : HasMUBs d 1

Every dimension admits a family of one mutually unbiased basis.

def OpenQuantumProblem13.Qubit.ω : ℂ

A convenient phase with squared norm $1/2$. Using $\omega = (1+i)/2$ avoids square roots.

Equations

• OpenQuantumProblem13.Qubit.ω = (1 + Complex.I) / 2

def OpenQuantumProblem13.Qubit.phaseMatrix (ζ : ℂ) : Matrix (Fin 2) (Fin 2) ℂ

The raw phase-parametrized Hadamard matrix. The cases $\zeta = 1$ and $\zeta = i$ give the $X$ and $Y$ bases.

Equations

• OpenQuantumProblem13.Qubit.phaseMatrix ζ = !![1, 1; ζ, -ζ]

theorem OpenQuantumProblem13.Qubit.omega_norm_sq : ‖ω‖ ^ 2 = 2⁻¹

The squared norm of ω is $1/2$.

theorem OpenQuantumProblem13.Qubit.conj_omega_mul_omega : star ω * ω = (↑2)⁻¹

The product $\overline{\omega}\,\omega$ is $1/2$.

theorem OpenQuantumProblem13.Qubit.star_smul_mul_smul (a : ℂ) (A B : Matrix (Fin 2) (Fin 2) ℂ) : star (a • A) * a • B = (star a * a) • (star A * B)

Taking the star of a scalar multiple on the left and multiplying by another scalar multiple collects the scalar factor as $\overline{a} a$.

theorem OpenQuantumProblem13.Qubit.star_phaseMatrix_mul_phaseMatrix (ζ η : ℂ) : star (phaseMatrix ζ) * phaseMatrix η = !![1 + star ζ * η, 1 - star ζ * η; 1 - star ζ * η, 1 + star ζ * η]

The relative product of two phase matrices has the expected $2 \times 2$ form.

theorem OpenQuantumProblem13.Qubit.star_phaseMatrix_mul_self_of_unit_phase {ζ : ℂ} (hζ : star ζ * ζ = 1) : star (phaseMatrix ζ) * phaseMatrix ζ = 2 • 1

If $\zeta$ has unit modulus, then the phase matrix is orthogonal up to the scalar factor $2$.

theorem OpenQuantumProblem13.Qubit.scaled_phaseMatrix_mem_unitary {ζ : ℂ} (hζ : star ζ * ζ = 1) : ω • phaseMatrix ζ ∈ Matrix.unitaryGroup (Fin 2) ℂ

Scaling a phase matrix by $\omega$ produces a unitary matrix whenever the phase has unit modulus.

theorem OpenQuantumProblem13.Qubit.star_phaseBasis_mul_phaseBasis (ζ η : ℂ) : star (ω • phaseMatrix ζ) * ω • phaseMatrix η = (star ω * ω) • !![1 + star ζ * η, 1 - star ζ * η; 1 - star ζ * η, 1 + star ζ * η]

The relative product of two scaled phase matrices is obtained by scaling the corresponding relative product of phase matrices.

def OpenQuantumProblem13.Qubit.phaseU (ζ : ℂ) (hζ : star ζ * ζ = 1) : UMat 2

The bundled qubit basis associated to a unit-modulus phase $\zeta$.

Equations

• OpenQuantumProblem13.Qubit.phaseU ζ hζ = ⟨OpenQuantumProblem13.Qubit.ω • OpenQuantumProblem13.Qubit.phaseMatrix ζ, ⋯⟩

theorem OpenQuantumProblem13.Qubit.phase_norm_sq_eq_one {ζ : ℂ} (hζ : star ζ * ζ = 1) : ‖ζ‖ ^ 2 = 1

A complex number with $\overline{\zeta}\,\zeta = 1$ has squared norm $1$.

theorem OpenQuantumProblem13.Qubit.omega_mul_phase_norm_sq {ζ : ℂ} (hζ : star ζ * ζ = 1) : ‖ω * ζ‖ ^ 2 = 2⁻¹

Multiplying $\omega$ by a unit-modulus phase preserves the squared norm $1/2$.

def OpenQuantumProblem13.Qubit.ZU : UMat 2

The standard qubit basis.

Equations

• OpenQuantumProblem13.Qubit.ZU = 1

def OpenQuantumProblem13.Qubit.XU : UMat 2

The qubit $X$ basis as a bundled unitary matrix.

Equations

• OpenQuantumProblem13.Qubit.XU = OpenQuantumProblem13.Qubit.phaseU 1 OpenQuantumProblem13.Qubit.XU._proof_1

def OpenQuantumProblem13.Qubit.YU : UMat 2

The qubit $Y$ basis as a bundled unitary matrix.

Equations

• OpenQuantumProblem13.Qubit.YU = OpenQuantumProblem13.Qubit.phaseU Complex.I OpenQuantumProblem13.Qubit.YU._proof_1

theorem OpenQuantumProblem13.Qubit.isUnbiased_Z_phaseU (ζ : ℂ) (hζ : star ζ * ζ = 1) : IsUnbiased ZU (phaseU ζ hζ)

The standard basis is mutually unbiased with any phase basis of unit-modulus phase.

theorem OpenQuantumProblem13.Qubit.relative_phaseU_phaseU_of_mul_eq_I {ζ η : ℂ} (hζ : star ζ * ζ = 1) (hη : star η * η = 1) (hζη : star ζ * η = Complex.I) : relativeUnitary (phaseU ζ hζ) (phaseU η hη) = !![ω, star ω; star ω, ω]

If $\overline{\zeta}\,\eta = i$, then the relative unitary between the corresponding phase bases is the qubit mutually unbiased overlap matrix.

theorem OpenQuantumProblem13.Qubit.isUnbiased_phaseU_phaseU_of_mul_eq_I {ζ η : ℂ} (hζ : star ζ * ζ = 1) (hη : star η * η = 1) (hζη : star ζ * η = Complex.I) : IsUnbiased (phaseU ζ hζ) (phaseU η hη)

If $\overline{\zeta}\,\eta = i$, then the corresponding phase bases are mutually unbiased.

def OpenQuantumProblem13.Qubit.qubitFamily : Fin 3 → UMat 2

The three standard qubit mutually unbiased bases: $Z$, $X$, and $Y$.

Equations

• OpenQuantumProblem13.Qubit.qubitFamily = ![OpenQuantumProblem13.Qubit.ZU, OpenQuantumProblem13.Qubit.XU, OpenQuantumProblem13.Qubit.YU]

theorem OpenQuantumProblem13.Qubit.qubitFamily_isMUB : IsMUBFamily qubitFamily

The standard qubit family is a family of mutually unbiased bases.

theorem OpenQuantumProblem13.Qubit.qubit_hasThreeMUBs : HasMUBs 2 3

There exist three mutually unbiased bases in dimension $2$.

def OpenQuantumProblem13.Qubit.u0 (U : UMat 2) : ℂ

The first entry of the first column of a qubit unitary basis matrix.

Equations

• OpenQuantumProblem13.Qubit.u0 U = ↑U 0 0

def OpenQuantumProblem13.Qubit.u1 (U : UMat 2) : ℂ

The second entry of the first column of a qubit unitary basis matrix.

Equations

• OpenQuantumProblem13.Qubit.u1 U = ↑U 1 0

@[reducible, inline]

abbrev OpenQuantumProblem13.Qubit.BlochVec : Type

The real Bloch-vector space for qubits.

Equations

• OpenQuantumProblem13.Qubit.BlochVec = EuclideanSpace ℝ (Fin 3)

def OpenQuantumProblem13.Qubit.bloch (U : UMat 2) : BlochVec

The Bloch vector associated to the first column of a qubit basis matrix.

Equations

• One or more equations did not get rendered due to their size.

theorem OpenQuantumProblem13.Qubit.relativeUnitary_apply_zero_zero (U V : UMat 2) : relativeUnitary U V 0 0 = star (u0 U) * u0 V + star (u1 U) * u1 V

The $(0,0)$ entry of the relative unitary is the overlap of the first columns.

theorem OpenQuantumProblem13.Qubit.firstCol_normSq (U : UMat 2) : Complex.normSq (u0 U) + Complex.normSq (u1 U) = 1

The first column of a unitary matrix has squared norm $1$.

theorem OpenQuantumProblem13.Qubit.re_mul_conj (z w : ℂ) : (z * star w).re = z.re * w.re + z.im * w.im

The real part of $z \overline{w}$ is the Euclidean dot product of the coordinate pairs of z and w.

theorem OpenQuantumProblem13.Qubit.bloch_inner_eq_two_normSq_sub_one (U V : UMat 2) : inner ℝ (bloch U) (bloch V) = 2 * Complex.normSq (relativeUnitary U V 0 0) - 1

The Bloch inner product is determined by the $(0,0)$ entry of the relative unitary.

theorem OpenQuantumProblem13.Qubit.relativeUnitary_self (U : UMat 2) : relativeUnitary U U = 1

The relative unitary of a basis with itself is the identity matrix.

theorem OpenQuantumProblem13.Qubit.bloch_inner_self (U : UMat 2) : inner ℝ (bloch U) (bloch U) = 1

Every qubit Bloch vector has squared Euclidean norm $1$.

theorem OpenQuantumProblem13.Qubit.bloch_ne_zero (U : UMat 2) : bloch U ≠ 0

A qubit Bloch vector is never the zero vector.

theorem OpenQuantumProblem13.Qubit.bloch_inner_eq_zero_of_isUnbiased {U V : UMat 2} (hUV : IsUnbiased U V) : inner ℝ (bloch U) (bloch V) = 0

Mutually unbiased qubit bases have orthogonal Bloch vectors.

theorem OpenQuantumProblem13.Qubit.qubit_upper_bound (m : ℕ) : HasMUBs 2 m → m ≤ 3

No family of mutually unbiased bases in dimension $2$ has size greater than $3$.

theorem OpenQuantumProblem13.Qubit.qubit_maximal : IsMaxMUBCount 2 3

The maximum number of mutually unbiased bases in dimension $2$ is $3$.

theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim2 : IsMaxMUBCount 2 3

In dimension $2$, the maximum number of mutually unbiased orthonormal bases is $3$.

theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim6_bounds : HasMUBs 6 3 ∧ ∀ (m : ℕ), HasMUBs 6 m → m ≤ 7

Known general bounds in dimension $6$: the maximal number of mutually unbiased bases satisfies $3 \le \mu(6) \le 7$.

theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim6 : IsMaxMUBCount 6 sorry

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

theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim10 : IsMaxMUBCount 10 sorry

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

theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim12 : IsMaxMUBCount 12 sorry

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

theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim14 : IsMaxMUBCount 14 sorry

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

theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim15 : IsMaxMUBCount 15 sorry

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

theorem OpenQuantumProblem13.mutuallyUnbiasedBases (d : ℕ) (hd : 2 ≤ d) : IsMaxMUBCount d (sorry d)

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