Order 10 = 2 · 5
0 / 2 paper-excluded 0 / 2 Lean-excluded even candidate
Why a candidate
Order 10 = 2 · 5 is a candidate because it divides the following Theorem 7 maxima: 50, 110.
From the paper (Macaj–Siran 2010)
Lemma 15 rows pq = 10 (a₀ ∈ {1, 6})
constrain order-10 elements. Theorem 7 proof remark:
"G cannot contain ℤ₁₀ and
ℤ₃₅ with a common ℤ₅".
Theorem 2 (Makhnev–Paduchikh) reads the two
order-10 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}:
D₅:Y = ℤ₅inverted byt,X = 1;|Y| = 5 ✓, condition (b) vacuous. Paper-allowed.ℤ₁₀ = ℤ₂ × ℤ₅:Y = 1, X = ℤ₅;|Y| = 1 ✓. MP 2001 Lemma 3 cases (1), (4), (6) forp = 5giveFix(ℤ₅) ∈ {empty, pentagon, HS}; condition (b) rules out the empty case, leavingFix(ℤ₅) ∈ {pentagon, HS}. Paper-allowed.
The paper does not exclude either group of order 10.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(10, 1) |
D₅ |
Dihedral; ℤ₅ inverted by t, |Y|=5, |X|=1. |
allowed | open |
(10, 2) |
ℤ₁₀ |
Cyclic; decomposes as ⟨t⟩ × ℤ₅ with |Y|=1, |X|=5. |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.