Order 22 = 2 · 11

From the paper (Macaj–Siran 2010)

Theorem 7 lists 2p with p ∈ {7, 11, 19} as a surviving even candidate. The paper provides:

• Lemma 12 row p = 11, a₀ = 5: a₁(σ) ∈ {55, 220, 385}.
• Lemma 15 row pq = 22, a₀ = 1, a₀(x_p) = 5, a₀(x_q) = 56: a partial entry with a₁(x) = 222 etc. — but not a contradiction.

However, Theorem 2 (Makhnev–Paduchikh) further requires the structural decomposition G = ⟨Y, t⟩ × X with |Y| ∈ {1, 3, 5, 7, 19, 21, 57}. For D₁₁ = ℤ₁₁ ⋊ ℤ₂, the only inverted subgroup is ℤ₁₁ itself (|Y| = 11 ∉ allowed set), and no other decomposition works — so D₁₁ is paper-excluded. The remaining case ℤ₂₂ is paper-allowed (|Y| = 1, X = ℤ₁₁, Fix(X) = pentagon) and is the genuine paper-survivor.

Natural-language proof (this project)

Writeup: proofs/no_aut_order_22_moore57.md.

From a generator σ of order 11 and an involution τ with τστ = σ−1:

1. Hoffman–Singleton local bound + k = 5 regular case forces Fix(σ) ≅ C₅;
2. Higman trace identity Tk = 11 n (k = 1..10);
3. F₁₁ permutation module / orbit kernel: 10 n ≡ 6 (mod 11);
4. Phase 3 four-cycle bound: n ∈ {5, 20, 35, 50};
5. Combined: n = 5;
6. Even-trace parity (dihedral case) contradicts n = 5.

The Hoffman–Singleton SRG classification (k ∈ {1, 3, 7, 57}) used in step 1 is also new in this project (formalised from Hoffman–Singleton 1960 + Bannai–Ito 1973).

Lean formalization (this project)

theorem no_Order22_group_acts_on_Moore57 :
    ¬ Nonempty (OrderN_GroupActsOnMoore57 22 V Γ)

File: Moore57/Order22OnMoore57/GroupAction.lean. The raw-action form Moore57.no_Order22_acts_on_Moore57 lives in Moore57/Order22OnMoore57/NoGo.lean.

Axiom dependencies (checked by AxiomsCheck.lean): propext, Classical.choice, Quot.sound, plus one native_decide axiom (a Fin 5 dihedral enumeration).

Group classification

Both cases are captured by the same Lean theorem: a group of order 22 must contain an involution τ and an element σ of order 11 (Cauchy), and the relation τστ = σ±1 is determined by the conjugation action. Both possibilities are handled inside Order22ActsOnMoore57.