Central low return in a generated group
Abstract
A central low return word forces a group generated by the marked pair to be commutative.
Theorem 1.1 (Central low return implies commutativity).
Lean statement: D5/S3/Geometry/Hyperideal/NoncommutativeCentralReturn.commutative_of_central_low_return
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/NoncommutativeCentralReturn.commutative_of_central_low_return (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let u and v generate G. If every element of the generated subgroup commutes with the low return word v inverse times u squared, then u commutes with that word. The identity v = u squared times the inverse low return word then gives Commute(u,v). Since the two marked generators commute pairwise, their generated subgroup is commutative; the generation hypothesis makes every pair in G commute.
The conclusion applies to arbitrary groups and does not assume finiteness, faithfulness of an action, or a geometric realization. In a noncommutative group generated by u and v, the low return word therefore cannot be central.