Existence of a Model Companion for Groups of Exponent 3
Yawara Ishida, Ryosuke Mizuno, Kota Takeuchi
math.LO
Sep 24, 2026 · v1
math.GR
TL;DR
All results of the paper, including existence of a model companion for exponent-3 groups, are fully formalized in Lean 4.
Abstract
In this article, we prove that the theory $T_3$ of groups of exponent $3$ has a model companion. Previous work established the existence of model companions for theories of groups of fixed finite exponent and nilpotency class at most $2$ (Saracino–Wood), and for theories of groups of prime exponent $p$ and nilpotency class at most $c<p$ (Maier). These results do not cover $T_3$, since groups of exponent $3$ may have nilpotency class $3$. Our theorem verifies the $n=3$ case of a conjecture proposed by the third author that, for each integer $n>1$, the theory $T_n$ of groups of exponent $n$ has a model companion if and only if every finitely generated group of exponent $n$ is finite, or equivalently, if and only if the Burnside problem has a positive solution for exponent $n$.
Problem
Whether the theory T_3 of groups of exponent 3 has a model companion. Earlier results covered exponent groups of nilpotency class at most 2, or class c<p for prime exponent p, and neither case includes exponent-3 groups of class 3.
Approach
The authors study lower central series structure and relatively free presentations of exponent-3 groups. They use the fact that normal closures consist of products of at most three conjugates. They prove uniform bounds on generators for existentially closed models (Proposition A) and use lower-central strictness to transfer amalgamation failures to finite coproducts. All results are formalized in Lean 4.
Results
T_3 has a model companion, verifying the n=3 case of a conjecture linking model companions for exponent-n groups to the Burnside problem. Examples show that lower-central strictness and existential closedness cannot be dropped from the key lemmas.
