Six mutually unbiased partial Hadamard matrices with five columns

Open

RybinAI2026.P16.six_unbiased_partial_hadamards

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

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

This is an open existence assertion for the dimension-six complete MUB problem in rectangular, unnormalized coordinates.

There exist six complex matrices $A_0,\ldots,A_5$ , each with six rows and five columns, satisfying

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

All conditions concern the same family. Each Gram identity is the full five-by-five identity, so each matrix has five mutually orthogonal columns of squared length six. Entry-modulus equations are explicitly imposed on the first five rows; cross-Gram modulus equations cover all five-by-five entries. There is no sixth column among the unknowns. Entries are arbitrary complex numbers, with no phase, root-of-unity, Fourier, tensor-product, or dephasing restriction.

After division by $\sqrt6$ , the columns represent partial orthonormal bases. This formulation follows the source's partial-basis, or MU-constellation, viewpoint. Completing the missing column of each partial basis gives a witness for the preceding square-matrix frontier; restricting square matrices to their first five columns gives the converse. The required completions and their preservation properties are proved in the accompanying formal reduction.

The formulation uses 180 complex entries instead of 216, retains 525 explicit modulus-squared equations, and replaces six Gram identities of order six by six Gram identities of order five. Its truth remains unresolved. The cited paper's completion argument does not prove that this simultaneous family exists.

Formalization Note. The row restriction in the entry-modulus equations uses Fin.castSucc from Fin 5 to Fin 6. The reduced entry constraints are inherited from the mission's preceding border-completion reduction; they are an equivalent encoding of the full entry-modulus conditions, not a phase restriction.

Preamble

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

Formal statement

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

Source

Brierley and Weigert, Maximal Sets of Mutually Unbiased Quantum States in Dimension Six, arXiv:0808.1614v1, Section 2.1, equation (3) and the surrounding completion argument, https://arxiv.org/html/0808.1614#S2.SS1; published as Phys. Rev. A 78, 042312 (2008), Section II.A, https://doi.org/10.1103/PhysRevA.78.042312. The open case is the constellation of seven partial bases with five vectors each, with the computational basis fixed and the six remaining partial bases rescaled by sqrt(6). The restriction of individual entry-modulus equations to the first five rows is an equivalent reduced encoding inherited from the prior formal border-completion step, not a verbatim source convention. Original problem: https://rybindmitry.github.io/problems/16.html, Known results.

View graph