Order 54 = 2 · 3³

From the paper (Macaj–Siran 2010)

Theorem 7 lists 54 as a surviving even-order maximum. But Theorem 2 (Makhnev–Paduchikh) restricts the structure to G = ⟨Y, t⟩ × X with |Y| ∈ {1, 3, 5, 7, 19, 21, 57}, so |Y| ∈ {1, 3} at this order (since |Y| ∣ 27 and |Y| odd):

• |Y| = 1, |X| = 27: G = ℤ₂ × X with X any of the 5 groups of order 27 (Theorem 4 caps 3-groups at order 27; Lemma 17 forces Fix(X) = Petersen, which fits Theorem 2(b)). 5 groups paper-allowed.
• |Y| = 3, |X| = 9: G = S₃ × X with X one of ℤ₉ or (ℤ₃)². 2 groups paper-allowed.
• Any group needing |Y| ∈ {9, 27} in its only decomposition (i.e. D₂₇ and the various generalized-dihedral / semidirect structures inverting all of a 9- or 27-subgroup) is paper-excluded.

Combined: 7 of the 15 groups of order 54 are paper-allowed, 8 are paper-excluded.

Natural-language proof (this project)

not yet written

Strategy: 15 specific extensions to rule out, but the Sylow-2 piece is a single involution and Theorem 4 / Corollary 2 already restrict the 3-part. The triangle-free obstruction (p = 3, a₁(x) > 0 ⇒ triangle in Γ) from Lemma 12 is the key tool. See Contribute.

Lean formalization (this project)

open

Group classification

There are 15 groups of order 54, listed as SmallGroup(54, 1) … SmallGroup(54, 15) in GAP. Representative types: