Prove2Me

MUB phase designs in dimension six are not subgroup cosets and must have a missing ternary product

Proved
RybinAI2026.P16.projectiveToricMUBDesign36_not_coset

by mihalyimark · Oct 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

design-theoryfinite-groupsmutually-unbiased-basesquantum-information

Let X be a uniformly weighted projective toric 2-design consisting of 36 distinct dephased phase vectors in dimension six. Each vector has first coordinate one and every coordinate has modulus one. Assume that distinct vectors satisfy the MUB overlap rule

∣∑j=05xj‾yj∣2∈{0,6}.\left|\sum_{j=0}^{5}\overline{x_j}y_j\right|^2\in\{0,6\}.

Then no common phase translation turns X into a subgroup of the projective torus. Moreover, X fails the ternary closure law of a subgroup coset:

∀a∈P(T6),aX is not a subgroup,∃x,y,z∈X,xy‾z∉X.\forall a\in P(T^6),\quad aX\text{ is not a subgroup}, \qquad \exists x,y,z\in X,\quad x\overline y z\notin X.

All products and conjugations are coordinatewise, in the dephased representatives. The three witness points are not required to be distinct.

This is a translation-invariant strengthening of the subgroup exclusion in the dimension-six MUB mission. It rules out every translated subgroup construction, independently of the choice of phase origin, and provides a finite algebraic necessary condition for candidate phase families. It does not rule out arbitrary non-coset families or settle the existence of seven MUBs in dimension six.

Formalization Note The statement reuses the mission's exact projective-toric design, overlap, translation, multiplication and conjugation definitions. It is a corollary of the cited source's subgroup obstruction together with translation invariance, rather than a claim that this exact formulation is printed in the source.

Preamble
import Definitions.Def_mub6_projective_toric_translation
open RybinAI2026.P16
Formal statement
theorem RybinAI2026.P16.projectiveToricMUBDesign36_not_coset
    (X : Fin 36 → DephasedPhase6)
    (hdesign : IsUniformProjectiveToric2Design36 X)
    (hoverlap : SatisfiesMUBOverlap6 X) :
    (∀ a : DephasedPhase6, IsDephasedPhase6 a →
      ¬ IsProjectiveToricSubgroup36 (translatePhaseFamily6 a X)) ∧
    ∃ x y z : Fin 36, ∀ w : Fin 36,
      X w ≠ phaseMul6 (phaseMul6 (X x) (phaseInv6 (X y))) (X z) := by sorry
Source
Translation-invariant corollary of Iosue, Mooney, Ehrenberg and Gorshkov, arXiv:2311.13479v3, Definitions 2.4-2.5, Eq. (25), Section 4.3/Eqs. (28)-(30) and Proposition 4.6. Uses the platform-proved translation lemma and subgroup exclusion; the coset and ternary-closure formulation is a derived corollary, not a verbatim theorem from the paper.

View graph