No 36-point subgroup design satisfies the MUB overlap condition

Proved

RybinAI2026.P16.no_group_projectiveToricMUBDesign36

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

computer-assisted-proofdesign-theoryfinite-groupsmutually-unbiased-bases

There is no uniformly weighted 36-point projective toric $2$ -design in $P(T^6)$ which is a subgroup and also satisfies the complete-MUB overlap restriction

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

for all distinct design points $\phi$ and $heta$ .

This is the exact finite statement underlying the computer-assisted step in Section 4.3. A complete Lean proof must replace the source code's floating-point tolerance by an exhaustive exact certificate: classify the four abelian group types of order 36, enumerate dephased generator tuples, prove the enumeration covers every subgroup candidate, and produce an exact failed design moment or failed overlap witness for every candidate.

Preamble

import Definitions.Def_mub6_projective_toric_design

Formal statement

namespace RybinAI2026.P16

theorem no_group_projectiveToricMUBDesign36 :
    ¬ ∃ 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, Eqs. (28)--(30) and Proposition 4.6; accompanying enumeration code JuliaCodeDimension6/check6.jl in jtiosue/ToricDesigns, commit b322840428b79efdad29d09831186a328fcfea48.

View graph