Order 6 = 2 · 3
0 / 2 paper-excluded 0 / 2 Lean-excluded even candidate
Why a candidate
Order 6 = 2 · 3 is a candidate because it divides the following Theorem 7 maxima: 54.
From the paper (Macaj–Siran 2010)
Lemma 15 row pq = 6 (a₀ = 2, a₀(x_p) = 10,
a₀(x_q) = 56) constrains order-6 elements; no starred row.
Theorem 2 (Makhnev–Paduchikh) reads the two
order-6 groups via G = ⟨Y, t⟩ × X with
|Y| ∈ {1, 3, 5, 7, 19, 21, 57} and (if
X ≠ 1) Fix(X) ∈ {star, pentagon, Petersen, HS}:
S₃ = D₃:Y = ℤ₃inverted byt,X = 1;|Y| = 3 ✓, condition (b) vacuous. Paper-allowed.ℤ₆ = ℤ₂ × ℤ₃:Y = 1, X = ℤ₃;|Y| = 1 ✓. MP 2001 Lemma 3 cases (2) / (5) forp = 3giveFix(ℤ₃) ∈ {singleton, Petersen}; condition (b) eliminates the singleton, but the Petersen branch survives. Paper-allowed.
The paper does not exclude either group of order 6.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(6, 1) |
S₃ |
Symmetric on 3 letters / D₃; ℤ₃ inverted by t, |Y|=3, |X|=1. |
allowed | open |
(6, 2) |
ℤ₆ |
Cyclic; decomposes as ⟨t⟩ × ℤ₃ with |Y|=1, |X|=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.