Complete MUBs and 36-point projective toric designs

Proved

RybinAI2026.P16.completeMUB6_iff_projectiveToricDesign36

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

design-theorymutually-unbiased-basesquantum-information

A complete family of seven mutually unbiased orthonormal bases in $\mathbb C^6$ exists if and only if there is a uniformly weighted 36-point projective toric $2$ -design $X\subset P(T^6)$ such that every two distinct points satisfy

\left|\sum_{j=0}^{5} e^{i(\phi_j- heta_j)} ight|^2\in\{0,6\}.

This is Theorem 4.4 of the source specialized to dimension six. The forward implication extracts the 36 non-computational-basis vectors after a unitary gauge choice; the reverse implication adjoins the six computational-basis vectors. The assertion is an equivalence of two existence statements and does not itself establish either side.

Preamble

import Definitions.Def_mub6_projective_toric_design

Formal statement

namespace RybinAI2026.P16

theorem completeMUB6_iff_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

Iosue--Mooney--Ehrenberg--Gorshkov, arXiv:2311.13479v3, Section 4.2, Theorem 4.4 and Eqs. (25)--(26); adapted from Appendix F of Iosue--Sharma--Gullans--Albert, arXiv:2211.05127.

View graph