Theorem 4.7: a finitely generated solvable group with no free subsemigroup of rank two is polycyclic

Let $\Gamma$ be a finitely generated solvable group which contains no free subsemigroup of rank two. Then $\Gamma$ is polycyclic.

The hypotheses. "Finitely generated" is the existence of a finite subset whose generated subgroup is all of $\Gamma$; the empty set is allowed, so the trivial group qualifies. "Solvable" is taken in Mathlib's form — the derived series $\Gamma^{(0)} = \Gamma$, $\Gamma^{(k+1)} = [\Gamma^{(k)}, \Gamma^{(k)}]$ reaches the trivial subgroup after finitely many steps. Both are typeclass hypotheses; they are assumptions, not conclusions.

No free subsemigroup of rank two, spelled out, is the negation of: there exist $a, b \in \Gamma$ such that distinct positive words in the two letters take distinct values when the letters are read as $a$ and $b$, the factors multiplied left to right in the order the letters occur and the empty word sent to $1$. So the hypothesis says that for every ordered pair $(a,b)$ of elements of $\Gamma$ — degenerate pairs such as $a = b$ or $a = 1$ included, where it is automatic — there are two distinct positive words with the same value.

Two points about this condition, both of which matter for how strong the theorem is. No letter stands for an inverse and no cancellation is performed, so this is a statement about a free subsemigroup, strictly weaker than asserting that $\Gamma$ has no free subgroup of rank two; and the quantifier is over all pairs, so the force of the hypothesis lies in the pairs of distinct elements of infinite order.

The conclusion. Polycyclic is taken in the published sense of Wolf's Proposition 4.1 (1): there are a natural number $t$ and subgroups $A_0, A_1, \dots, A_t$ of $\Gamma$ with $A_0 = \Gamma$, $A_t = \{1\}$, and for each $i < t$ both $A_{i+1} \subseteq A_i$ and — regarding $A_{i+1}$ as a subgroup of the group $A_i$ — $A_{i+1}$ normal in $A_i$ with $A_i/A_{i+1}$ cyclic.

Three things this conclusion does not say. Normality is asserted only relative to the immediately preceding term, so the chain is a subnormal series and no $A_i$ is claimed normal in $\Gamma$. "Cyclic" means generated by a single element as a group, which includes the trivial group and every finite cyclic group, so the quotients need not be infinite. And the chain is not required to descend strictly: repetitions $A_{i+1} = A_i$ are allowed, with trivial quotient. The length $t$ is existentially quantified and is tied neither to the number of generators nor to the length of the derived series.

The hypotheses are jointly satisfiable — the trivial group meets all three — so the implication is not vacuous.