Order 14 = 2 · 7

From the paper (Macaj–Siran 2010)

Theorem 7 lists 14 as a surviving even candidate (one of 2p, p ∈ {7, 11, 19}). Available partial constraints:

• Lemma 2 (Higman / Cameron): an involution t fixes a 56-vertex star.
• Lemma 12 row p = 7 gives several shapes (a₀, a₁, χ₁).
• Lemma 15 has no entry for pq = 14.

Theorem 2 (Makhnev–Paduchikh) reads the two order-14 groups via G = ⟨Y, t⟩ × X with |Y| ∈ {1, 3, 5, 7, 19, 21, 57} and (if X ≠ 1) Fix(X) ∈ {star, pentagon, Petersen, HS}:

• D₇: Y = ℤ₇ inverted by t, X = 1; |Y| = 7 ✓, condition (b) vacuous. Paper-allowed.
• ℤ₁₄ = ℤ₂ × ℤ₇: Y = 1, X = ℤ₇; |Y| = 1 ✓. By MP 2001 Lemma 3 case (3) for p = 7, Fix(ℤ₇) is necessarily a star — which is in the Theorem 2(b) list. Paper-allowed.

The paper does not exclude group order 14.

Natural-language proof (this project)

not yet written

Strategy outline (mirrors the Order 22 route): σ of order 7, τ involution; use the F₇ permutation module + Tk = 7n Higman trace + aut_involution_fixedVertexCount_candidates. The main bottleneck is the missing F₇ good-reduction analogue of aF11_lambda_seven_eq_159. See Contribute.

Lean formalization (this project)

open — depends on the natural-language proof above.

Group classification