Order 19 = 19
0 / 1 paper-excluded 0 / 1 Lean-excluded odd candidate
Why a candidate
Order 19 = 19 is a candidate because it divides the following Theorem 6 maxima: 171.
From the paper (Macaj–Siran 2010)
MP 2001 Lemma 3 case (2) for p = 19 forces
|Fix(ℤ₁₉)| = 1 (a singleton) — = Lemma 4 case 2 /
Lemma 16 case 2. Lemma 19 case (2) further forces the 19-Sylow to
be cyclic: X ≅ ℤ₁₉, no ℤ₁₉². This is the
same restriction the project uses for the order-38 case (formalized
as order19_aut_fixedVertexCount_eq_one). No direct
exclusion at order 19 — the single group ℤ₁₉ is
paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(19, 1) |
ℤ₁₉ |
Cyclic; |Fix(ℤ₁₉)| = 1 (Lem 3(2)); 19-Sylow forced cyclic (Lem 19(2)). |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.