Any dimension-six complete MUB yields a non-group toric design

Proved

RybinAI2026.P16.completeMUB6_implies_nonGroup_projectiveToricDesign36

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

design-theoryfinite-groupsmutually-unbiased-basesquantum-information

If a complete family of seven mutually unbiased bases exists in complex dimension six, then there is an associated uniformly weighted 36-point projective toric $2$ -design satisfying the MUB overlap condition which is not a subgroup of $P(T^6)$ .

This is Proposition 4.6 of the source. It is strictly conditional: it neither proves nor disproves the existence of seven mutually unbiased bases in dimension six. Its proof separates into Theorem 4.4's equivalence and the exact exclusion of all 36-point subgroup candidates.

Preamble

import Definitions.Def_mub6_projective_toric_design

Formal statement

namespace RybinAI2026.P16

theorem completeMUB6_implies_nonGroup_projectiveToricDesign36 :
    (∃ B : Fin 7 → Matrix (Fin 6) (Fin 6) ℂ, IsCompleteMUB6 B) →
      ∃ X : Fin 36 → DephasedPhase6,
        IsUniformProjectiveToric2Design36 X ∧
          SatisfiesMUBOverlap6 X ∧ ¬ IsProjectiveToricSubgroup36 X := by sorry

end RybinAI2026.P16

Source

Iosue--Mooney--Ehrenberg--Gorshkov, arXiv:2311.13479v3, Section 4.3, Proposition 4.6, using Theorem 4.4 and Eqs. (28)--(30).

View graph