A dimension-six subgroup MUB design would force six to be a prime power

Proved

RybinAI2026.P16.subgroupProjectiveToricMUBDesign36_implies_primePower

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

design-theoryfinite-geometryfinite-groupsmutually-unbiased-bases

If a 36-point subgroup of $P(T^6)$ is a uniformly weighted projective toric $2$ -design and satisfies Equation (25), then $6$ must be a prime power.

The proof restricts the six coordinate characters to the subgroup, obtains a Sidon set, constructs a relative $(6,6,6,1)$ -difference set and hence a projective plane of order six with an abelian collineation group of order $36$ . The theorem of Blokhuis, Jungnickel, and Schmidt then forces the plane order to be a prime power.

Preamble

import Definitions.Def_mub6_projective_toric_design
import Mathlib.Algebra.IsPrimePow

Formal statement

namespace RybinAI2026.P16

theorem subgroupProjectiveToricMUBDesign36_implies_primePower
    (X : Fin 36 → DephasedPhase6)
    (hdesign : IsUniformProjectiveToric2Design36 X)
    (hoverlap : SatisfiesMUBOverlap6 X)
    (hgroup : IsProjectiveToricSubgroup36 X) :
    IsPrimePow 6 := by sorry

end RybinAI2026.P16

Source

A Translation Observation for Three Conjectures on Projective Toric Designs, Theorem “Subgroup obstruction”; Blokhuis--Jungnickel--Schmidt, Proc. AMS 130 (2002), Theorem 1.1, DOI 10.1090/S0002-9939-01-06388-2.

View graph