Order 35 = 5 · 7

From the paper (Macaj–Siran 2010)

Theorem 6 lists 35 as a surviving odd-order maximum. Lemma 15 row pq = 35, a₀(x) = 1, a₀(x_5) = 51 is one of two starred (impossible) rows — so the strongest orbit-shape for an order-35 element is already excluded by the paper, but the group-order exclusion is still open.

Per-prime: Lem 18 / Lem 3(1/4/6) gives Fix(ℤ₅) ∈ {empty, pentagon, HS}; Lem 19(4) gives Fix(ℤ₇) = star. The single group ℤ₃₅ is not individually excluded — paper-allowed. (Note: Theorem 7 proof remark "G cannot contain ℤ₁₀ and ℤ₃₅ with a common ℤ₅" is a joint constraint that does not apply here in isolation.)

Natural-language proof (this project)

not yet written

Strategy: combine Lemma 12 / 14 / 15 (the latter with its single surviving row for pq = 35) into a complete statement. See Contribute.

Lean formalization (this project)

open

Group classification