Order 135 = 3³ · 5
0 / 5 paper-excluded 0 / 5 Lean-excluded odd candidate
From the paper (Macaj–Siran 2010)
Theorem 6 lists 135 as a surviving odd-order maximum. Theorem 4
bounds |3-part of G| ≤ 27; Theorem 5 restricts the
Sylow-5 piece (a single ℤ₅ here). Per-prime: Lem 17 /
Lem 3(2/5) gives Fix(ℤ₃) ∈ {singleton, Petersen};
Lem 18 / Lem 3(1/4/6) gives Fix(ℤ₅) ∈ {empty, pentagon, HS}.
The paper does not exclude group order 135 — none of the 5 isomorphism types is individually ruled out.
Natural-language proof (this project)
not yet written
Strategy: the 5-Sylow subgroup is normal
(n₅ ∣ 27, n₅ ≡ 1 mod 5), and the action of
the 3-part on Aut(ℤ₅) ≅ ℤ₄ is trivial. Thus every group
of order 135 is ℤ₅ × P for one of the five groups
P of order 27; remains to close all five products. See
Contribute.
Lean formalization (this project)
open
Group classification
There are 5 groups of order 135
(SmallGroup(135, 1) … SmallGroup(135, 5)).
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(135, 1) | ℤ₂₇ × ℤ₅ ≅ ℤ₁₃₅ | Cyclic, corresponding to the cyclic group of order 27 times ℤ₅. | allowed | open |
(135, 2) | ℤ₉ × ℤ₃ × ℤ₅ | Abelian, rank 2 on the 3-part. | allowed | open |
(135, 3) | Heisenberg₃ × ℤ₅ | Non-abelian 3-group of exponent 3 times ℤ₅. | allowed | open |
(135, 4) | (ℤ₉ ⋊ ℤ₃) × ℤ₅ | Non-abelian 3-group of exponent 9 times ℤ₅. | allowed | open |
(135, 5) | ℤ₃³ × ℤ₅ | Elementary abelian 3-group times ℤ₅. | allowed | open |
Exact GAP indices may differ; the family names are the invariant data.