Order 7 = 7
0 / 1 paper-excluded 0 / 1 Lean-excluded odd candidate
Why a candidate
Order 7 = 7 is a candidate because it divides the following Theorem 6 maxima: 35, 147.
From the paper (Macaj–Siran 2010)
MP 2001 Lemma 3 case (3) for p = 7 forces
Fix(ℤ₇) to be a star on 2 + 7l vertices
(= Lemma 4 case 3 / Lemma 16 case 3). Lemma 19 then bounds the
7-Sylow: either |X| = 7 (star Fix) or
|X| = 49 only as ℤ₇ × ℤ₇ with edge Fix
(the cyclic ℤ₄₉ is excluded). No direct exclusion at
order 7 — the single group ℤ₇ is
paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(7, 1) |
ℤ₇ |
Cyclic; Fix(ℤ₇) = star on 2 + 7l vertices (Lem 3(3)). |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.