Order 171 = 3² · 19

From the paper (Macaj–Siran 2010)

Theorem 6 lists 171 as a surviving odd-order maximum — the only odd-order candidate involving the prime 19. Lemma 12 row p = 19, a₀ = 1: a₁(σ) ∈ {57, 342, ...}. Per-prime: Lem 19(2) forces |Fix(ℤ₁₉)| = 1 and the 19-Sylow cyclic; Lem 17 / Lem 3(2/5) gives Fix(ℤ₃) ∈ {singleton, Petersen}.

The paper does not exclude group order 171 — none of the 5 isomorphism types is individually ruled out.

Natural-language proof (this project)

The cyclic case C₁₇₁ is closed in proofs/no_cyclic_aut_groups_moore57.md (§4.5) via subgroup containment: if σ has order 171 then σ³ has order 57, contradicting the cyclic C₅₇ exclusion (order 57). The four non-cyclic groups (ℤ₁₉ ⋊ ℤ₉, ℤ₁₉ × ℤ₃², (ℤ₁₉ ⋊ ℤ₃) × ℤ₃, ℤ₁₉ ⋊ ℤ₃²) are not yet covered.

Lean formalization (this project)

theorem aut_no_cyclic_order_one_hundred_seventy_one_unconditional
    (hΓ : IsMoore57 Γ) (σ : Equiv.Perm V)
    (smul_adj : ∀ a b : V, Γ.Adj a b ↔ Γ.Adj (σ a) (σ b))
    (hpow : σ ^ 171 = 1) (hne_9 : σ ^ 9 ≠ 1) (hne_57 : σ ^ 57 ≠ 1) :
    False

File: Moore57/Moore57Graph/Aut/CyclicGroupExclusions.lean (reduces to aut_no_cyclic_order_fifty_seven_unconditional on σ³). Axiom dependencies: propext, Classical.choice, Quot.sound only.

Group classification (SmallGroup(171, k))

There are 5 groups of order 171.

Exact GAP indices may differ; family names are the invariant data.