Order 3 = 3
0 / 1 paper-excluded 0 / 1 Lean-excluded odd candidate
Why a candidate
Order 3 = 3 is a candidate because it divides the following Theorem 6 maxima: 39, 135, 147, 171, 375.
From the paper (Macaj–Siran 2010)
MP 2001 Lemma 3 cases (2) / (5) for p = 3 give
Fix(ℤ₃) ∈ {singleton, Petersen}; Lemma 12 row
p = 3, a₀(x) = 1 is starred and excluded, so the
Petersen-Fix branch is the live one (Lemma 4 case 5 / Lemma 16
case 2). Lemma 17 then bounds any 3-group: |X| ∣ 27
(Petersen-Fix) or |X| ∣ 81 (singleton-Fix). No
direct exclusion at order 3 — the single group ℤ₃
is paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(3, 1) |
ℤ₃ |
Cyclic; Fix(ℤ₃) = Petersen (Lem 3(5)) — singleton ruled out by Lemma 12 starred row. |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.