Six mutually unbiased complex Hadamard matrices of order six

Open

RybinAI2026.P16.six_mutually_unbiased_hadamards

by puno · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complex-hadamard-matricesmutually-unbiased-basesquantum-information-theory

This is the open dimension-six existence problem in unnormalized Hadamard coordinates, not an established existence theorem.

There exist six complex matrices of order six, indexed by $r=0,\ldots,5$ , satisfying

H_r^\dagger H_r=6I_6,\qquad |(H_r)_{ij}|^2=1

for every matrix and every entry, and satisfying

\left|(H_r^\dagger H_s)_{ij}\right|^2=6 \qquad(0\le r<s\le5)

for every pair of column indices. All three conditions concern the same six matrices. Entries are arbitrary complex numbers; no restriction to roots of unity, Fourier families, tensor products, or separately dephased representatives is imposed.

This formulation removes the computational basis and clears the normalization denominators from the remaining equations. The overlaps are required for the fifteen unordered pairs; conjugate-transpose symmetry recovers the reverse orders. The assertion retains the unresolved existence content of the seven-basis problem.

Formalization Note. The column Gram convention is used, matching the mission. For square matrices this is equivalent to the row Gram convention in equation (5.5) of the source. The cross-Gram condition is the entrywise modulus part of equation (5.16); its orthogonality follows from the individual Hadamard identities.

Preamble

import Mathlib.LinearAlgebra.Matrix.ConjTranspose
import Mathlib.Data.Complex.Basic
open Matrix
open scoped ComplexConjugate Matrix

Formal statement

theorem RybinAI2026.P16.six_mutually_unbiased_hadamards :
    ∃ H : Fin 6 → Matrix (Fin 6) (Fin 6) ℂ,
      (∀ r, (H r)ᴴ * H r = (6 : ℂ) • (1 : Matrix (Fin 6) (Fin 6) ℂ)) ∧
      (∀ r i j, Complex.normSq (H r i j) = 1) ∧
      (∀ r s, r < s → ∀ i j,
        Complex.normSq (((H r)ᴴ * H s) i j) = 6) := by sorry

Source

CUHK-Shenzhen AI Math Problem 16, Known results, https://rybindmitry.github.io/problems/16.html (open dimension-six case); Durt, Englert, Bengtsson and Zyczkowski, On mutually unbiased bases, arXiv:1004.3348v2, Sections 5.1–5.2, equations (5.5), (5.16) and the paragraph immediately after (5.16), https://arxiv.org/html/1004.3348#S5.SS2. The cited review supplies the equivalence, not a proof of dimension-six existence.

View graph