Order 57 = 3 · 19

Why a candidate

Order 57 = 3 · 19 is a candidate because it divides the following Theorem 6 maxima: 171.

From the paper (Macaj–Siran 2010)

Lemma 15 covers an element of order 57 = 3 · 19. Proposition 7 (q = 19) handles the 3 · 19 structure.

Per-prime: Lem 17 / Lem 3(2/5) gives Fix(ℤ₃) ∈ {singleton, Petersen}; Lem 19(2) forces |Fix(ℤ₁₉)| = 1 and the 19-Sylow cyclic. Neither of the two order-57 groups is excluded individually — both paper-allowed.

Natural-language proof (this project)

The cyclic case C₅₇ is closed in proofs/no_cyclic_aut_groups_moore57.md (§4.3). From σ³ (order 19) and σ¹⁹ (order 3): |Fix(σ³)| = 1 by Lem 19(2), so (y₁, y₃) = (1, 0); combined with |Fix(σ¹⁹)| ∈ {1, 10} and y₁ = 1, this forces y₁₉ = 0 or 9. The orbit-size bound (y_m = 0 or m ≤ y_m) excludes y₁₉ = 9, leaving y₁₉ = 0 — but then |Fix(σ¹⁹)| = 1, contradicting lem12 p=3, a₀=1. The Frobenius ℤ₁₉ ⋊ ℤ₃ case is not yet covered.

Lean formalization (this project)

theorem aut_no_cyclic_order_fifty_seven_unconditional
    (hΓ : IsMoore57 Γ) (σ : Equiv.Perm V)
    (smul_adj : ∀ a b : V, Γ.Adj a b ↔ Γ.Adj (σ a) (σ b))
    (hpow : σ ^ 57 = 1) (hne_3 : σ ^ 3 ≠ 1) (hne_19 : σ ^ 19 ≠ 1) :
    False

File: Moore57/Moore57Graph/Aut/CyclicGroupExclusions.lean. Axiom dependencies: propext, Classical.choice, Quot.sound only.

Group classification