Order 147 = 3 · 7²

From the paper (Macaj–Siran 2010)

Theorem 6 lists 147 as a surviving odd-order maximum. Lemma 19 case (5) forces the Sylow-7 (order 49) to be ℤ₇ × ℤ₇, not ℤ₄₉. The two groups of order 147 whose 7-Sylow is ℤ₄₉ are therefore paper-excluded: ℤ₁₄₇ (cyclic) and ℤ₄₉ ⋊ ℤ₃.

The remaining 4 groups (with 7-Sylow ℤ₇ × ℤ₇) are constrained but not excluded by the paper: Lemma 12 row p = 7 gives several (a₀, a₁, χ₁) shapes, and Lemma 13 / 14 add further trace constraints. This project now excludes two of those four by reducing visible C₂₁ subgroups to the Lean-certified cyclic C₂₁ obstruction.

Natural-language proof (this project)

Strategy for the four ℤ₇²-Sylow groups: combine the order-7 / order-49 element constraints (Lemma 12 / 13) with the orbit structure. Six SmallGroup cases total. See Contribute.

The cyclic case ℤ₁₄₇ is paper-excluded (Lemma 19, ℤ₄₉ Sylow forbidden). This project also supplies an independent NL proof via subgroup containment: σ of order 147 yields σ⁷ of order 21, contradicting the cyclic C₂₁ exclusion (proofs/no_cyclic_aut_groups_moore57.md §4.1). The same subgroup-containment path removes (147, 5) ℤ₇ × (ℤ₇ ⋊ ℤ₃) and (147, 6) ℤ₃ × ℤ₇ × ℤ₇, since each contains commuting elements of orders 3 and 7. It does not by itself remove the fixed-line-free ℤ₇² ⋊ ℤ₃ cases (147, 3) and (147, 4).

Lean formalization (this project)

2 / 6 excluded — the two C₂₁-visible ℤ₇²-Sylow cases have Lean wrappers: aut_no_order_147_case5_c7_times_frobenius21_via_c21 and aut_no_order_147_case6_c3_times_c7_times_c7_via_c21. Both use the common faithful-action obstruction no_faithful_aut_action_of_commuting_order_three_order_seven. The cyclic ℤ₁₄₇ case remains Lean-reducible to C₂₁ (aut_no_cyclic_order_twenty_one_unconditional) via σ ↦ σ⁷ (order 21), but the wrapper theorem is not yet in the codebase.

Group classification (SmallGroup(147, k))

There are 6 groups of order 147 in total.

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