Exclude the $\mathbb Z_4\times\mathbb Z_9$ subgroup case

Proved

RybinAI2026.P16.no_groupType49_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 4 × ZMod 9 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_groupType49_projectiveToricMUBDesign36 :
    ¬ ∃ X : Fin 36 → DephasedPhase6,
      IsUniformProjectiveToric2Design36 X ∧
        SatisfiesMUBOverlap6 X ∧ HasGroupType49 X := by sorry

end RybinAI2026.P16

Source

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

View graph

Exclude the Z4×Z9\mathbb Z_4\times\mathbb Z_9Z4​×Z9​ subgroup case

Exclude the $\mathbb Z_4\times\mathbb Z_9$ subgroup case