Order 45 = 3² · 5
0 / 2 paper-excluded 0 / 2 Lean-excluded odd candidate
Why a candidate
Order 45 = 3² · 5 is a candidate because it divides the following Theorem 6 maxima: 135.
From the paper (Macaj–Siran 2010)
Combines a 3²-Sylow (Lemma 17: Fix ∈ {singleton, Petersen},
|X| ∣ 81 or 27) and a 5-Sylow (Lemma 18 /
Lem 3(1/4/6): Fix(ℤ₅) ∈ {empty, pentagon, HS}).
Proposition 6 (p = 3, q = 5) constrains the
3 · 5 structure. Neither of the two order-45 groups is
individually excluded — both paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(45, 1) | ℤ₄₅ | Cyclic; 3-Sylow ℤ₉. | allowed | open |
(45, 2) | (ℤ₃)² × ℤ₅ | Abelian, rank 2; 3-Sylow ℤ₃². | allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.