Order 2 = 2
0 / 1 paper-excluded 0 / 1 Lean-excluded even candidate
Why a candidate
Order 2 = 2 is a candidate because it divides the following Theorem 7 maxima: 14, 22, 38, 50, 54, 110.
From the paper (Macaj–Siran 2010)
Lemma 2 (Higman / Cameron): every involution t fixes a
56-vertex star (a₀(t) = 56, a₁(t) = 112), and
4 ∤ |Aut(Γ)| — so the involution is isolated in its
Sylow 2-subgroup.
Theorem 2 (Makhnev–Paduchikh) reads the order-2
group via the trivial decomposition G = ⟨1, t⟩ × 1
with |Y| = 1 ∈ {1, 3, 5, 7, 19, 21, 57} ✓ and
X = 1 (condition (b) on Fix(X) vacuous).
The single group ℤ₂ is paper-allowed;
closing it requires the deeper star / involution-action analysis.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(2, 1) |
ℤ₂ |
Cyclic; single involution t, |Y|=1, |X|=1. |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.