Order 18 = 2 · 3²
2 / 5 paper-excluded 0 / 5 Lean-excluded even candidate
Why a candidate
Order 18 = 2 · 3² is a candidate because it divides the following Theorem 7 maxima: 54.
From the paper (Macaj–Siran 2010)
Theorem 2 (Makhnev–Paduchikh) restricts any
even-order G to G = ⟨Y, t⟩ × X with
|Y| ∈ {1, 3, 5, 7, 19, 21, 57}. Combined with Lemma 17
(3-group fixes Petersen or singleton), the two groups of order 18
whose only allowed decomposition would need |Y| = 9
(i.e. all of the 3²-subgroup inverted by t) are
paper-excluded: D₉ and the generalized-dihedral
(ℤ₃)² ⋊ ℤ₂.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(18, 1) | D₉ | Dihedral of order 18; ℤ₉ inverted by t. | excluded (Thm 2: |Y|=9) | open |
(18, 2) | ℤ₁₈ | Cyclic; decomposes as ⟨t⟩ × ℤ₉ with |Y|=1, |X|=9. | allowed | open |
(18, 3) | (ℤ₃)² ⋊ ℤ₂ | Generalized dihedral; t inverts the whole (ℤ₃)². | excluded (Thm 2: |Y|=9) | open |
(18, 4) | S₃ × ℤ₃ | Direct product; decomposes as ⟨ℤ₃, t⟩ × ℤ₃ with |Y|=3, |X|=3. | allowed | open |
(18, 5) | ℤ₆ × ℤ₃ ≅ ℤ₂ × (ℤ₃)² | Abelian; decomposes as ⟨t⟩ × (ℤ₃)² with |Y|=1, |X|=9. | allowed | open |
SmallGroup IDs are illustrative — exact GAP IDs may differ; the paper-status is determined by isomorphism class.
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.