Extract a 36-point toric design from a complete dimension-six MUB

Proved

RybinAI2026.P16.completeMUB6_to_projectiveToricDesign36

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

design-theorymutually-unbiased-bases

If seven mutually unbiased orthonormal bases exist in $\mathbb C^6$ , then after a common unitary change of coordinates sends one basis to the computational basis, the remaining 36 vectors determine a uniformly weighted projective toric $2$ -design satisfying Equation (25). This is the “only if” direction of Theorem 4.4, specialized to dimension six.

Preamble

import Definitions.Def_mub6_projective_toric_design

Formal statement

namespace RybinAI2026.P16

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

end RybinAI2026.P16

Source

arXiv:2311.13479v3, Section 4.2, Theorem 4.4, “only if” direction; Appendix F, Lemma F.2 of Iosue--Sharma--Gullans--Albert, arXiv:2211.05127.

View graph