Order 75 = 3 · 5²

0 / 3 paper-excluded 1 / 3 Lean-excluded odd candidate · cyclic C₇₅ closed

Why a candidate

Order 75 = 3 · 5² is a candidate because it divides the following Theorem 6 maxima: 375.

From the paper (Macaj–Siran 2010)

Combines order-3 (Lem 17 / Lem 3(2/5)) and order-25 / 5² Sylow (Lem 18) constraints. Proposition 6 (3 · 5²) restricts the 75-order group structure. None of the three order-75 groups is individually excluded — all 3 paper-allowed.

Natural-language proof (this project)

The cyclic case C₇₅ is closed in proofs/no_cyclic_aut_groups_moore57.md (§4.4). The key tools are |Fix(σ²⁵)| ∈ {1, 10} (order-3) and |Fix(σ¹⁵)| ∈ {0, 5, 50} (order-5): expanding via the orbit-count |Fix(σᵏ)| = Σ_{m ∣ gcd(k, 75)} y_m and using the divisibility m ∣ y_m gives 3 ∣ (y₃ + y₁₅), but the same sum must equal 40 (mod 3) ≡ 1 — contradiction. The two non-cyclic cases (ℤ₅²) ⋊ ℤ₃ and ℤ₁₅ × ℤ₅ are not yet covered.

Lean formalization (this project)

theorem aut_no_cyclic_order_seventy_five_unconditional
    (hΓ : IsMoore57 Γ) (σ : Equiv.Perm V)
    (smul_adj : ∀ a b : V, Γ.Adj a b ↔ Γ.Adj (σ a) (σ b))
    (hpow : σ ^ 75 = 1) (hne_25 : σ ^ 25 ≠ 1) (hne_15 : σ ^ 15 ≠ 1) :
    False

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

Group classification

SmallGroupGroupDescriptionPaperLean
(75, 1)(ℤ₅ × ℤ₅) ⋊ ℤ₃Non-abelian (3 acts on ℤ₅²).allowedopen
(75, 2)ℤ₇₅Cyclic; 5-Sylow ℤ₂₅.allowedexcluded (original)
(75, 3)ℤ₁₅ × ℤ₅Abelian, rank 2; 5-Sylow ℤ₅².allowedopen