Orders of Large Alternating Groups
Abstract
Alternating groups of degree at least five have order divisible by sixty and cannot be 2-groups.
Lemma 1.1 (Sixty divides the alternating order).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/AlternatingBounds.sixty_dvd_card_alternating (✓ std3). ∎
Source. Repository-derived.
Commentary.
Alt(k) denotes the alternating group on Fin(k). Twice its order equals k factorial. For k at least five, divisibility by 5 factorial gives divisibility of the order by sixty.
Lemma 1.2 (Large alternating groups have even order).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/AlternatingBounds.two_dvd_card_alternating (✓ std3). ∎
Source. Repository-derived.
Commentary.
This is the even-order consequence of divisibility by sixty, used when applying the Sylow 2-subgroup obstruction.
Lemma 1.3 (Large alternating groups are not 2-groups).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/AlternatingBounds.alternating_not_twoGroup (✓ std3). ∎
Source. Repository-derived.
Commentary.
A finite 2-group has order a power of two. Three divides sixty and hence the order of Alt(k) for k at least five, contradicting that power-of-two order.