Order 375 = 3 · 5³

From the paper (Macaj–Siran 2010)

Theorem 6 lists 375 as a surviving odd-order maximum — the largest overall (Corollary 3: |G| ≤ 375). Theorem 5 restricts the Sylow-5 of order 125 to two abelian types (ℤ₁₂₅ or ℤ₂₅ × ℤ₅) once SmallGroup(625, 12) is ruled out (Proposition 4). Per-prime: Lem 17 / Lem 3(2/5) gives Fix(ℤ₃) ∈ {singleton, Petersen}; Lem 18 / Theorem 5 constrain the 5³-Sylow. The paper notes that even after Lemma 5's equitable-partition check, hundreds of candidate adjacency matrices for groups of order 375 with 10 orbits survive.

The paper does not exclude order 375 as a whole (it is the Corollary 3 maximum). Theorem 5 / Proposition 4 do, however, rule out the three groups whose Sylow-5 is non-abelian or ℤ₅³, leaving four paper-allowed families.

Natural-language proof (this project)

The cyclic case C₃₇₅ is closed in proofs/no_cyclic_aut_groups_moore57.md (§4.7) via subgroup containment: if σ has order 375 then σ⁵ has order 75, contradicting the cyclic C₇₅ exclusion (order 75). The three non-cyclic SmallGroup families are not yet covered; the harder remaining Tier of paper-faithful results (GAP-aided Prop 4 / Prop 5) attacks them.

Lean formalization (this project)

theorem aut_no_cyclic_order_three_hundred_seventy_five_unconditional
    (hΓ : IsMoore57 Γ) (σ : Equiv.Perm V)
    (smul_adj : ∀ a b : V, Γ.Adj a b ↔ Γ.Adj (σ a) (σ b))
    (hpow : σ ^ 375 = 1) (hne_125 : σ ^ 125 ≠ 1) (hne_75 : σ ^ 75 ≠ 1) :
    False

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

Group classification

There are 7 groups of order 375 (SmallGroup(375, 1) … SmallGroup(375, 7); 375 is the smallest order with exactly 7 groups, OEIS A046057). Theorem 5 / Proposition 4 restrict the Sylow-5 subgroup P of size 125 to one of two abelian types (ℤ₁₂₅ or ℤ₂₅ × ℤ₅) once SmallGroup(625, 12) is excluded — paper-excluding the 3 groups whose Sylow-5 is ℤ₅³ or non-abelian. The remaining 4 paper-allowed families:

SmallGroup IDs SmallGroup(375, k) enumerate the precise extensions; we list them by family here.