Six Hadamard matrices with five-by-five modulus constraints

Open

RybinAI2026.P16.six_hadamards_five_by_five_constraints

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

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

This is an open existence assertion for the dimension-six MUB problem, with redundant modulus equations removed.

There exist six complex square matrices $H_0,\ldots,H_5$ of order six such that

\begin{aligned} H_r^\dagger H_r&=6I_6 &&(0\leq r<6),\\ |(H_r)_{ij}|^2&=1 &&(0\leq r<6,\ 0\leq i,j<5),\\ |(H_r^\dagger H_s)_{ij}|^2&=6 &&(0\leq r<s<6,\ 0\leq i,j<5). \end{aligned}

All conditions concern the same family of matrices. The Gram identities are full matrix equalities. Only the entry-modulus and cross-Gram-modulus equations are restricted to the leading five-by-five blocks. Entries are arbitrary complex numbers, with no phase, root-of-unity, Fourier, tensor-product, or dephasing restriction.

This assertion is equivalent to the mission's existing six-Hadamard frontier: scaled unitarity forces the omitted row and column modulus equations. It keeps 525 explicit real modulus-squared equations in place of 756, while preserving all six Gram identities. Its truth remains unresolved; the cited sources do not establish this existence assertion.

Formalization Note. Row and column indices for the restricted equations are in Fin 5, embedded into Fin 6 by castSucc, so the omitted index is exactly 5. This is a reduced encoding of the source's open dimension-six problem, with equivalence justified by the accompanying formal reduction, rather than a new existence result.

Preamble

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

Formal statement

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

Source

CUHK-Shenzhen AI Math Problem 16, Known results, https://rybindmitry.github.io/problems/16.html; Durt, Englert, Bengtsson and Zyczkowski, On mutually unbiased bases, arXiv:1004.3348v2, Sections 5.1-5.2, equations (5.5), (5.16), https://arxiv.org/html/1004.3348#S5.SS2. The five-by-five restriction is an equivalent reduced encoding derived using row and column normalization, equations (1.1)-(1.2), and proved sufficient in the accompanying formal reduction. The existence assertion remains open.

View graph