Order 21 = 3 · 7

Why a candidate

Order 21 = 3 · 7 is a candidate because it divides the following Theorem 6 maxima: 147.

From the paper (Macaj–Siran 2010)

Lemma 15 has no entry for pq = 21 directly; Proposition 7 handles the p = 3, q = 7 case in the p^a q^b structural analysis. Per-prime: Lem 17 / Lem 3(2/5) gives Fix(ℤ₃) ∈ {singleton, Petersen}; Lem 19(4) gives Fix(ℤ₇) = star. Neither of the two order-21 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.1) via the Petersen-centralizer argument: write C₂₁ = ⟨a⟩ × ⟨b⟩ with |a| = 3, |b| = 7. Then Fix(a) = Petersen graph (Lem 17), and by commutativity b acts on Fix(a). Since Aut(Petersen) ≅ S₅ has no element of order 7, the b-action is trivial, so Petersen ⊆ Fix(b). But Fix(b) is a star (Lem 19(4)), which cannot contain Petersen as an induced subgraph — contradiction. The Frobenius case ℤ₇ ⋊ ℤ₃ is not yet covered.

Lean formalization (this project)

theorem aut_no_cyclic_order_twenty_one_unconditional
    {V : Type} [Fintype V] [DecidableEq V] {Γ : SimpleGraph V}
    [DecidableRel Γ.Adj]
    (hΓ : IsMoore57 Γ) (σ : Equiv.Perm V)
    (smul_adj : ∀ v w, Γ.Adj v w ↔ Γ.Adj (σ v) (σ w))
    (hpow : σ ^ 21 = 1) (hne_7 : σ ^ 7 ≠ 1) (hne_3 : σ ^ 3 ≠ 1) :
    False

File: Moore57/Moore57Graph/Aut/CyclicGroupExclusions.lean. The proof dispatches via aut_order_three_SingletonOrPetersenSRG_unconditional on σ⁷ (order 3): singleton case excluded by lem12_no_p3_a0_one; Petersen-SRG case extracts PetersenFixedData Γ (σ⁷) via petersenUniqueness, then a star-vs-Petersen degree argument contradicts. The chain Aut(Kneser(5,2)) ≅ S₅ → Aut(Petersen) ≅ S₅ → no element of order 7 is in Moore57/Foundations/GraphTheory/ (Kneser52, Kneser52Aut, Kneser52MaxIndep, PetersenAutS5 — A'.4 track). Universe restricted to V : Type (universe 0) by petersenUniqueness's downstream constraint. Axiom dependencies: propext, Classical.choice, Quot.sound, plus the compiler-generated native_decide axioms used by the Petersen/S₅ finite checks; all are accepted by AxiomsCheck.lean's allowlist.

Group classification