Finite Group Obstruction for Orders Nine, Three and Two
Abstract
A finite group of order dividing seventy-two cannot be generated by elements of exact orders nine and three whose product has exact order two.
Theorem 1.1 (The universal finite-group obstruction).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CycleNineThreeObstruction.result (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. trureturing contributors (2026). No normal torsionfree index-72 orientation quotient for the degree-(8,9) Coxeter sector. URL: https://github.com/the-omega-institute/trureturing/pull/12077.
Acknowledgement. Mathlib contributors (2026). Sylow theory and automorphisms of finite cyclic groups in Mathlib. URL: https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/GroupTheory/Sylow.lean.
Commentary.
The universe u is arbitrary, Typeu denotes its types, and Group(H) denotes a chosen group structure on H. Finite(H) says the underlying type is finite. The function card gives its cardinality, ord gives exact element order, closure is the subgroup generated by the displayed set, and False is falsity. Thus for every finite group H and every r and s in H, the five hypotheses of generation, cardinality dividing seventy-two, and exact orders nine, three and two imply a contradiction. No normality hypothesis is imposed.
Lagrange’s theorem makes nine and two divide the order of H. Since that order divides seventy-two, it is eighteen, thirty-six or seventy-two. The cyclic subgroup P generated by r has order nine and index two, four or eight, so it is a Sylow three-subgroup. The Sylow count divides this index and is one modulo three, leaving exactly one or four Sylow three-subgroups. If there is only one, the subgroup generated by s lies in P. Hence rs lies in a group of order nine, which contradicts its exact order two.
In the four-subgroup case, conjugation defines a homomorphism alpha from H to the permutations of those four Sylow subgroups. Its image I acts transitively by Sylow conjugacy, so orbit-stabilizer makes four divide the order of I. The order of alpha(r) divides both nine and twenty-four and therefore divides three; the order of alpha(s) divides three as well. If both images were the identity, generation by r and s would make I trivial, contradicting transitivity on four points. A nonidentity image has exact order three. Thus the order of I is twelve or twenty-four.
Let K be the kernel of alpha and let z be r cubed. Kernel normality is automatic, and alpha(r) cubed being the identity puts z in K. The exact order of z is three. The kernel-image cardinality identity now forces K to have order three or six. Inside K, Z generated by z has order three and index one or two, so Sylow counting makes it the unique Sylow three-subgroup. Consequently Z is characteristic in K and normal in H. Both kernel normality and normality of Z are derived.
Conjugation on the normal cyclic subgroup Z maps H to its automorphism group, whose order is the totient of three, namely two. The automorphism induced by s has cube equal to the identity because s has order three. Its order therefore divides two and three, so it is trivial. Hence s commutes with z. The element r already commutes with its own cube; generation by r and s makes z central.
For the final word argument set u equal to rs, v equal to r times u times the inverse of r, and w equal to r squared times u times the inverse of r squared. These are three involutions. Multiplying in the order w, v, u gives r cubed times s cubed, which is z. Since w squares to the identity, vu equals wz. Commutation of w and z gives the identity that the square of vu is the square of z.
Conjugate that identity by u, which is its own inverse and commutes with z. The square of uv is also the square of z. Because u and v are involutions, uv is the inverse of vu. Multiplying their squared identities therefore makes the fourth power of z the identity. Its third power is also the identity because r has order nine. Thus z itself is the identity, contradicting the exact order nine of r.
The ordinary CFMP index-seventy-two project argument supplies the provenance of this obstruction. The cited Mathlib sources supply the Sylow conjugacy and counting statements, characteristic-subgroup normality and the cyclic automorphism cardinality used in the proof. The contradiction above uses the three conjugate involutions directly.
A Coxeter application still requires a finite quotient and the exact orders of the images of bc, cd and their product, as well as generation and the cardinality divisor condition. This theorem does not establish finite-parabolic faithfulness or those quotient hypotheses. The normal-cover interpretation of the project argument therefore remains conditional on that separate bridge; arbitrary pairings of twenty-four tetrahedra lie outside this conclusion.
References
- Truth anchor:
D5/S3/FiniteGroups/CycleNineThreeObstruction.result