Exclude the $\mathbb Z_3^2\times\mathbb Z_4$ subgroup case

Proved

RybinAI2026.P16.no_groupType334_projectiveToricMUBDesign36

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

computer-assisted-prooffinite-groupsmutually-unbiased-bases

No uniformly weighted 36-point projective toric $2$ -design satisfying Equation (25) has a faithful ZMod 3 × ZMod 3 × ZMod 4 generator presentation. This is one exact finite case of the exhaustive dimension-six subgroup exclusion. A proof should enumerate dephased generators using exact roots of unity and return a checkable collision, failed design moment, or failed overlap certificate for every tuple.

Preamble

import Definitions.Def_mub6_group36_presentations

Formal statement

namespace RybinAI2026.P16

theorem no_groupType334_projectiveToricMUBDesign36 :
    ¬ ∃ X : Fin 36 → DephasedPhase6,
      IsUniformProjectiveToric2Design36 X ∧
        SatisfiesMUBOverlap6 X ∧ HasGroupType334 X := by sorry

end RybinAI2026.P16

Source

arXiv:2311.13479v3, Section 4.3, group type 334 in Eq. (30); jtiosue/ToricDesigns JuliaCodeDimension6/check6.jl, commit b322840428b79efdad29d09831186a328fcfea48.

View graph

Exclude the Z32×Z4\mathbb Z_3^2\times\mathbb Z_4Z32​×Z4​ subgroup case

Exclude the $\mathbb Z_3^2\times\mathbb Z_4$ subgroup case