Order 275 = 5² · 11

From the paper (Macaj–Siran 2010)

Theorem 6 lists 275 as a surviving odd-order maximum. Proposition 8 (p = 5, q = 11) constrains the Sylow structure: P₁₁ is normal and |P₅| divides 25. Lemma 12 row p = 11, a₀ = 5: a₁(σ) ∈ {55, 220, 385}. Per-prime: Lem 19(3) forces Fix(ℤ₁₁) = pentagon and the 11-Sylow cyclic; Lem 18 allows the 5²-Sylow as ℤ₂₅ or ℤ₅² (unlike p = 7 at order 49, no cyclic exclusion at p = 5).

The paper does not exclude group order 275 — none of the 4 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.6). Powers σ²⁵ (order 11) and σ⁵⁵ (order 5) give |Fix(σ²⁵)| = 5 (pentagon, Lem 19(3)) and |Fix(σ⁵⁵)| ∈ {0, 5, 50}; combined with the total-divisor sum Σ_{d ∣ 275} y_d = 3250 and the divisibility m ∣ y_m, the value y₂₇₅ is forced into a non-multiple-of-275 — contradiction.

Two newer proof notes propose a route for three of the four order-275 groups: proofs/no_aut_order_275_three_cases_moore57.md and the corrected centralizer note proofs/no_aut_order_275_centralizer_fix_empty_case_ja.md. The correction is important: from |σ| = 11, |τ| = 5, and στ = τσ one should use the weaker dichotomy |Fix(τ)| ∈ {0, 5}, not the false blanket claim Fix(τ) = Fix(σ). The useful consequence is that a nontrivial commuting order-5 element cannot setwise stabilize a length-11 σ-orbit outside Fix(σ).

Lean formalization (this project)

theorem aut_no_cyclic_order_two_hundred_seventy_five_unconditional
    (hΓ : IsMoore57 Γ) (σ : Equiv.Perm V)
    (smul_adj : ∀ a b : V, Γ.Adj a b ↔ Γ.Adj (σ a) (σ b))
    (hpow : σ ^ 275 = 1) (hne_25 : σ ^ 25 ≠ 1) (hne_55 : σ ^ 55 ≠ 1) :
    False

Cyclic case file: Moore57/Moore57Graph/Aut/CyclicGroupExclusions.lean.

The centralizer/orbit ingredients for the non-cyclic order-275 route are now formalized separately:

theorem aut_order_five_fixedVertexCount_zero_or_five_of_commuting_order_eleven
    ... : fixedVertexCount τ = 0 ∨ fixedVertexCount τ = 5

theorem aut_order_five_not_sameCycle_image_of_commuting_order_eleven
    ... {z : V} (hz : σ z ≠ z) :
    ¬ σ.SameCycle z (τ z)

theorem aut_no_order25_conj_preserving_order11_cycleFactors
    ... : False

File: Moore57/Moore57Graph/Aut/Order275ThreeCases.lean. These theorems pass AxiomsCheck.lean with only the standard allowlisted axioms propext, Classical.choice, Quot.sound.

Status note: the last theorem assumes conjugation preserves the actual oriented σ.cycleFactorsFinset. A full Lean closure of ℤ₁₁ ⋊ ℤ₂₅ still needs the weaker orbit-support action induced by normalizing ⟨σ⟩. The abelian ℤ₁₁ × (ℤ₅ × ℤ₅) route likewise still needs subgroup-level packaging, so the public exclusion count remains 1 / 4.

Group classification

There are 4 groups of order 275 (SmallGroup(275, 1) … SmallGroup(275, 4)).

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