Order 9 = 3²
0 / 2 paper-excluded 0 / 2 Lean-excluded odd candidate
Why a candidate
Order 9 = 3² is a candidate because it divides the following Theorem 6 maxima: 135, 171.
From the paper (Macaj–Siran 2010)
Lemma 17 (3-group classification): a 3-group X has
Fix(X) either the Petersen graph (|X| ∣ 27)
or a singleton (|X| ∣ 81). Both branches allow
|X| = 9, so the paper does not single out either
order-9 group as excluded. Lemma 13 provides further trace
constraints for order-9 elements. Both groups
paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(9, 1) |
ℤ₉ |
Cyclic; 3-group, Lem 17 allows |X|=9 in either Fix branch. |
allowed | open |
(9, 2) |
ℤ₃ × ℤ₃ |
Elementary abelian; 3-group, Lem 17 allows. | allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.