Order 38 = 2 · 19

From the paper (Macaj–Siran 2010)

Theorem 7 lists 38 = 2 · 19 as a surviving even candidate. Available partial constraints:

• Lemma 2 (Higman / Cameron): an involution fixes a 56-vertex star, so a₀(τ) = 56 and a₁(τ) = 112.
• Lemma 12 row p = 19, a₀ = 1: a₁(σ) ∈ {57, 342, ...}.
• Lemma 15 has no entry for pq = 38.

However, Theorem 2 (Makhnev–Paduchikh) requires G = ⟨Y, t⟩ × X with |Y| ∈ {1, 3, 5, 7, 19, 21, 57}; if X ≠ 1, then Fix(X) ∈ {star, pentagon, Petersen, HS}. For ℤ₃₈ = ℤ₂ × ℤ₁₉, the only decomposition has Y = 1, X = ℤ₁₉ — but Fix(ℤ₁₉) = singleton (Lemma 4(2)), which is NOT in Theorem 2(b)'s list. So ℤ₃₈ is paper-excluded. The remaining case D₁₉ (with Y = ℤ₁₉ inverted, |Y| = 19 ∣ 57 ✓) is the genuine paper-survivor, and is closed only by the Lean proof of this project.

Natural-language proof (this project)

The two group types are handled separately:

• D₁₉ case (dihedral): Lean-aware writeup at proofs/moore57_d19_lean_aware_proof.md (Japanese), with companion notes proofs/moore57_d19_contradiction.md. Strategy: Higman trace + E₇ idempotent + D₁₉ character decomposition + rotation character constancy versus the compact adjacent-moved residual.
• C₃₈ case (cyclic): a generator g of order 38 gives ρ = g² (order 19) and τ = g¹⁹ (involution) that commute. The Tier-2 lemma aut_involution_fixedVertexCount_candidates gives |Fix(τ)| ∈ {0, 2, 6, 10, 16, 26, 36, 46, 50, 56}; combined with order19_aut_fixedVertexCount_eq_one for ρ the parity / mod-19 obstruction closes the case.

Lean formalization (this project)

theorem no_D19_acts_on_Moore57_unconditional
    {V} [Fintype V] [DecidableEq V]
    {Γ : SimpleGraph V} [DecidableRel Γ.Adj] :
    ¬ Nonempty (D19ActsOnMoore57 V Γ)

theorem no_C38_acts_on_Moore57_unconditional
    {V} [Fintype V] [DecidableEq V]
    {Γ : SimpleGraph V} [DecidableRel Γ.Adj] :
    ¬ Nonempty (C38ActsOnMoore57 V Γ)

theorem Moore57_no_order38_structure
    {V} [Fintype V] [DecidableEq V]
    {Γ : SimpleGraph V} [DecidableRel Γ.Adj] :
    (¬ Nonempty (D19ActsOnMoore57 V Γ))
    ∧ (¬ Nonempty (C38ActsOnMoore57 V Γ))

Files: Moore57/D19OnMoore57/NoGo.lean (D₁₉ + assembly), Moore57/C38OnMoore57/NoGo.lean (C₃₈).

By the classification of order-38 groups, the conjunction Moore57_no_order38_structure excludes every group of order 38 acting as a subgroup of Aut(Γ).

Group classification

The two cases are handled by separate Lean theorems: D₁₉ is the central case of the project (the original target), and C₃₈ reduces to commutativity of ρ = g² and τ = g¹⁹ with aut_involution_fixedVertexCount_candidates.

Lean proof structure (D₁₉ phases)

The Lean formalisation of the D₁₉ branch is split into 7 phases (Moore57/Phases/Phase{1..7}.lean) plus the Moore57/D19OnMoore57/ directory:

1. Phase 1: rotation a₀ ≤ 19, reflection a₀ = 56 / a₁ = 112 from raw action.
2. Phase 2: SRG identity, E₇ idempotent, Higman trace, Tr(E₇) = 1729.
3. Phase 3: reflection character χ₇(t) = 33.
4. Phase 4: D₁₉ characters 1, ε, ρ; linear character formulas; π_V = 114·1 + 58·ε + 171·ρ.
5. Phases 5–7: rotation character constancy versus the compact adjacent-moved residual gives the contradiction.