Six compatible Hadamard matrices yield seven dimension-six MUBs

Proved

RybinAI2026.P16.hadamards_to_completeMUB6

by jtiosue · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complex-hadamard-matricesmutually-unbiased-bases

Let $H_0,\ldots,H_5$ be six complex Hadamard matrices of order six: each satisfies $H_r^\dagger H_r=6I$ , every entry has squared modulus one, and every cross-Gram entry between distinct matrices has squared modulus six. Then adjoining the computational basis and scaling each $H_r$ by $1/\sqrt6$ produces seven pairwise mutually unbiased orthonormal bases in $\mathbb C^6$ .

Preamble

import Definitions.Def_rybin2026_p16_mutually_unbiased_bases

open Matrix
open scoped ComplexConjugate Matrix

Formal statement

namespace RybinAI2026.P16

theorem hadamards_to_completeMUB6
    (H : Fin 6 → Matrix (Fin 6) (Fin 6) ℂ)
    (hunit : ∀ r, (H r)ᴴ * H r = (6 : ℂ) • (1 : Matrix (Fin 6) (Fin 6) ℂ))
    (hflat : ∀ r i j, Complex.normSq (H r i j) = 1)
    (hoverlap : ∀ r s, r < s → ∀ i j,
      Complex.normSq (((H r)ᴴ * H s) i j) = 6) :
    ∃ B : Fin 7 → Matrix (Fin 6) (Fin 6) ℂ, IsCompleteMUB6 B := by sorry

end RybinAI2026.P16

Source

Standard Hadamard-coordinate construction for mutually unbiased bases; Durt et al., arXiv:1004.3348, Sections 5.1--5.2, Eqs. (5.5) and (5.16); used in arXiv:2311.13479v3, Theorem 4.4.

View graph