Order 110 = 2 · 5 · 11

From the paper (Macaj–Siran 2010)

Theorem 7 lists 110 = 2 · 5 · 11 as a surviving even candidate; Corollary 3 records it as the maximum even |G|. Lemma 15 row pq = 22 with a₀ = 1, a₀(x_5) = 5, a₀(x_{11}) = 56 gives a₁ = 222 etc. and the remark

"from Lemma 15 it follows that there is no automorphism of order 110."

This excludes only an element of order 110 — i.e. ℤ₁₁₀ (cyclic). But Theorem 2 (Makhnev–Paduchikh) further constrains the structure: G = ⟨Y, t⟩ × X with |Y| ∈ {1, 3, 5, 7, 19, 21, 57}. This excludes three more groups at order 110:

• D₅₅ needs |Y| = 55 (or 11) — both disallowed.
• ℤ₅ × D₁₁ needs |Y| = 11 — disallowed.
• The Frobenius F₁₁₀ = ℤ₁₁ ⋊ ℤ₁₀ has no allowed decomposition (the involution in ℤ₁₀ inverts ℤ₁₁, forcing |Y| = 11).

So the paper already excludes 4 of the 6 groups. The remaining two (D₅ × ℤ₁₁ and ℤ₂ × (ℤ₁₁ ⋊ ℤ₅)) are paper-allowed and are closed only by this project via the order-22 Sylow + Cauchy reduction.

Natural-language proof (this project)

Short subgroup-reduction argument:

1. Sylow's third theorem: n₁₁ ∣ 10 and n₁₁ ≡ 1 (mod 11), so n₁₁ = 1; the unique Sylow-11 subgroup P₁₁ ≅ ℤ₁₁ is normal.
2. Cauchy's theorem applied to |G| = 110: there exists an involution τ ∈ G.
3. H := ⟨P₁₁, τ⟩ has order 22 and is a subgroup of G ≤ Aut(Γ).
4. The Order-22 result (see order 22 page + writeup proofs/no_aut_order_22_moore57.md) excludes such H. Contradiction.

The novel content is the order-22 step; everything else is classical Sylow theory.

Lean formalization (this project)

theorem no_Order110_group_acts_on_Moore57 :
    ¬ Nonempty (OrderN_GroupActsOnMoore57 110 V Γ)

File: Moore57/Order22OnMoore57/GroupAction.lean. The proof body is the Sylow-reduction chain above, applying no_Order22_group_acts_on_Moore57 at the end.

Group classification (SmallGroup(110, k))

All 6 groups of order 110 (Sylow analysis: n₁₁ = 1; n₅ ∈ {1, 11}) are Lean-excluded uniformly via the order-22 Sylow + Cauchy reduction.