A 36-point projective-torus subgroup has one of four abelian types

Open

RybinAI2026.P16.projectiveToricSubgroup36_has_standard_type

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

design-theoryfinite-groups

Every 36-point subgroup represented by a uniformly weighted projective toric design has a faithful generator presentation of one of the four abelian group types

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

This is the classification step that makes the dimension-six search exhaustive.

Preamble

import Definitions.Def_mub6_group36_presentations

Formal statement

namespace RybinAI2026.P16

theorem projectiveToricSubgroup36_has_standard_type
    (X : Fin 36 → DephasedPhase6)
    (hdesign : IsUniformProjectiveToric2Design36 X)
    (hgroup : IsProjectiveToricSubgroup36 X) :
    HasGroupType49 X ∨ HasGroupType334 X ∨ HasGroupType229 X ∨ HasGroupType2233 X := by sorry

end RybinAI2026.P16

Source

arXiv:2311.13479v3, Section 4.3, Eqs. (30a)--(30d), using the classification theorem for finite abelian groups.

View graph