Order 55 = 5 · 11
0 / 2 paper-excluded 0 / 2 Lean-excluded odd candidate
Why a candidate
Order 55 = 5 · 11 is a candidate because it divides the following Theorem 6 maxima: 275.
From the paper (Macaj–Siran 2010)
Lemma 15 row pq = 55 (a₀ = 5, a₀(x_p) = 5,
a₀(x_q) = 5) has no starred row, so order-55 elements may
exist. Proposition 8 handles the 5 · 11 structure.
Per-prime: Lem 18 / Lem 3(1/4/6) gives
Fix(ℤ₅) ∈ {empty, pentagon, HS}; Lem 19(3) forces
Fix(ℤ₁₁) = pentagon and the 11-Sylow cyclic. Neither
of the two order-55 groups is excluded individually — both
paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(55, 1) | ℤ₁₁ ⋊ ℤ₅ | Non-abelian (5 ∣ 11 − 1); Frobenius group. | allowed | open |
(55, 2) | ℤ₅₅ | Cyclic. | allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.