Order 39 = 3 · 13

From the paper (Macaj–Siran 2010)

Theorem 6 lists 39 as a surviving odd-order maximum — the only candidate involving the prime 13. Lemma 12 row p = 13 gives a₀(x) = 0 and a₁(x) ∈ {65, 260, 455}. Lemma 15 has no entry for pq = 39.

Per-prime: Lem 19(1) forces Fix(ℤ₁₃) = ∅ and the 13-Sylow cyclic; Lem 17 / Lem 3(2/5) gives Fix(ℤ₃) ∈ {singleton, Petersen}. Neither of the two order-39 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.2) via the cyclic orbit-count lemma: |Fix(σ³)| = ∑_{d ∣ 13} y_d and |Fix(σ¹³)| = ∑_{d ∣ 3} y_d mixed with Lemma 12 dichotomy and the order-13 / order-3 fixed-vertex counts. The non-cyclic ℤ₁₃ ⋊ ℤ₃ case is not yet covered.

Lean formalization (this project)

theorem aut_no_cyclic_order_thirty_nine_unconditional
    (hΓ : IsMoore57 Γ) (σ : Equiv.Perm V)
    (smul_adj : ∀ a b : V, Γ.Adj a b ↔ Γ.Adj (σ a) (σ b))
    (hpow : σ ^ 39 = 1) (hne_3 : σ ^ 3 ≠ 1) (hne_13 : σ ^ 13 ≠ 1) :
    False

File: Moore57/Moore57Graph/Aut/CyclicGroupExclusions.lean. Foundations layer: Foundations/GroupAction/CyclicOrbitCount.lean (cyclic orbit-count and m ∣ y_m divisibility). Axiom dependencies: propext, Classical.choice, Quot.sound only.

Group classification