Partition a 36-point toric MUB design into six Hadamard bases

Proved

RybinAI2026.P16.projectiveToricDesign36_to_six_hadamards

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

complex-hadamard-matricesdesign-theorymutually-unbiased-bases

A uniformly weighted 36-point projective toric $2$ -design satisfying Equation (25) can be partitioned into six groups of six phase vectors. Arranging each group as the columns of a matrix gives six complex Hadamard matrices: columns within one matrix are orthogonal, entries are flat, and cross-Gram entries between distinct matrices have squared modulus six.

This is the combinatorial partition step in the reverse direction of Theorem 4.4.

Preamble

import Definitions.Def_mub6_projective_toric_design

open Matrix
open scoped ComplexConjugate Matrix

Formal statement

namespace RybinAI2026.P16

theorem projectiveToricDesign36_to_six_hadamards :
    (∃ X : Fin 36 → DephasedPhase6,
      IsUniformProjectiveToric2Design36 X ∧ SatisfiesMUBOverlap6 X) →
      ∃ 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

end RybinAI2026.P16

Source

Iosue--Mooney--Ehrenberg--Gorshkov, arXiv:2311.13479v3, Section 4.2, Theorem 4.4; Iosue--Sharma--Gullans--Albert, arXiv:2211.05127, Appendix F.

View graph