Four generator presentations for order-36 projective-torus subgroups

Definition

mub6_group36_presentations

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

design-theoryfinite-groupsmutually-unbiased-bases

This module gives exact generator presentations for each isomorphism type of finite abelian group of order $36$ :

\mathbb Z_4 imes\mathbb Z_9,\quad \mathbb Z_3 imes\mathbb Z_3 imes\mathbb Z_4,\quad \mathbb Z_2 imes\mathbb Z_2 imes\mathbb Z_9,\quad \mathbb Z_2 imes\mathbb Z_2 imes\mathbb Z_3 imes\mathbb Z_3.

For each type, generators are dephased phase vectors, their required powers are the identity, and evaluation on the product of cyclic index types must be injective and cover all 36 represented points. These predicates isolate the four exact finite enumeration cases used in Section 4.3 of the source.

Definition code

import Definitions.Def_mub6_projective_toric_design

namespace RybinAI2026.P16

/-- Pointwise natural-number powers of a dephased phase vector. -/
def phasePow6 (z : DephasedPhase6) (n : ℕ) : DephasedPhase6 :=
  fun j => z j ^ n

structure Group334Index where
  a : ZMod 3
  b : ZMod 3
  c : ZMod 4

structure Group229Index where
  a : ZMod 2
  b : ZMod 2
  c : ZMod 9

structure Group2233Index where
  a : ZMod 2
  b : ZMod 2
  c : ZMod 3
  d : ZMod 3

/-- Evaluation of generators for the group type `ZMod 4 × ZMod 9`. -/
def evalGroup49 (g4 g9 : DephasedPhase6) (p : ZMod 4 × ZMod 9) : DephasedPhase6 :=
  phaseMul6 (phasePow6 g4 p.1.val) (phasePow6 g9 p.2.val)

/-- Evaluation of generators for the group type `ZMod 3 × ZMod 3 × ZMod 4`. -/
def evalGroup334
    (g₁ g₂ g₃ : DephasedPhase6) (p : Group334Index) : DephasedPhase6 :=
  phaseMul6 (phaseMul6 (phasePow6 g₁ p.a.val) (phasePow6 g₂ p.b.val))
    (phasePow6 g₃ p.c.val)

/-- Evaluation of generators for the group type `ZMod 2 × ZMod 2 × ZMod 9`. -/
def evalGroup229
    (g₁ g₂ g₃ : DephasedPhase6) (p : Group229Index) : DephasedPhase6 :=
  phaseMul6 (phaseMul6 (phasePow6 g₁ p.a.val) (phasePow6 g₂ p.b.val))
    (phasePow6 g₃ p.c.val)

/-- Evaluation of generators for the group type `ZMod 2 × ZMod 2 × ZMod 3 × ZMod 3`. -/
def evalGroup2233
    (g₁ g₂ g₃ g₄ : DephasedPhase6) (p : Group2233Index) : DephasedPhase6 :=
  phaseMul6
    (phaseMul6 (phasePow6 g₁ p.a.val) (phasePow6 g₂ p.b.val))
    (phaseMul6 (phasePow6 g₃ p.c.val) (phasePow6 g₄ p.d.val))

/-- The points have a faithful `ZMod 4 × ZMod 9` generator presentation. -/
def HasGroupType49 (X : Fin 36 → DephasedPhase6) : Prop :=
  ∃ g4 g9,
    phasePow6 g4 4 = (fun _ => 1) ∧
      phasePow6 g9 9 = (fun _ => 1) ∧
      Function.Injective (evalGroup49 g4 g9) ∧
      ∀ x, ∃ p, X x = evalGroup49 g4 g9 p

/-- The points have a faithful `ZMod 3 × ZMod 3 × ZMod 4` generator presentation. -/
def HasGroupType334 (X : Fin 36 → DephasedPhase6) : Prop :=
  ∃ g₁ g₂ g₃,
    phasePow6 g₁ 3 = (fun _ => 1) ∧
      phasePow6 g₂ 3 = (fun _ => 1) ∧
      phasePow6 g₃ 4 = (fun _ => 1) ∧
      Function.Injective (evalGroup334 g₁ g₂ g₃) ∧
      ∀ x, ∃ p, X x = evalGroup334 g₁ g₂ g₃ p

/-- The points have a faithful `ZMod 2 × ZMod 2 × ZMod 9` generator presentation. -/
def HasGroupType229 (X : Fin 36 → DephasedPhase6) : Prop :=
  ∃ g₁ g₂ g₃,
    phasePow6 g₁ 2 = (fun _ => 1) ∧
      phasePow6 g₂ 2 = (fun _ => 1) ∧
      phasePow6 g₃ 9 = (fun _ => 1) ∧
      Function.Injective (evalGroup229 g₁ g₂ g₃) ∧
      ∀ x, ∃ p, X x = evalGroup229 g₁ g₂ g₃ p

/-- The points have a faithful `ZMod 2 × ZMod 2 × ZMod 3 × ZMod 3` generator presentation. -/
def HasGroupType2233 (X : Fin 36 → DephasedPhase6) : Prop :=
  ∃ g₁ g₂ g₃ g₄,
    phasePow6 g₁ 2 = (fun _ => 1) ∧
      phasePow6 g₂ 2 = (fun _ => 1) ∧
      phasePow6 g₃ 3 = (fun _ => 1) ∧
      phasePow6 g₄ 3 = (fun _ => 1) ∧
      Function.Injective (evalGroup2233 g₁ g₂ g₃ g₄) ∧
      ∀ x, ∃ p, X x = evalGroup2233 g₁ g₂ g₃ g₄ p

end RybinAI2026.P16

Source

Iosue--Mooney--Ehrenberg--Gorshkov, arXiv:2311.13479v3, Section 4.3, Eqs. (28) and (30a)--(30d).

View graph