Theorem 4.3 (2): a polycyclic group with no nilpotent subgroup of finite index grows at least exponentially

Let $\Gamma$ be a polycyclic group having no nilpotent subgroup of finite index, and let $S$ be any finite generating set of $\Gamma$. Then there is a constant $v > 1$ such that $v^m \le g_S(m)$ for every integer $m \ge 1$, where $g_S(m)$ is Wolf's growth function: the number of elements of $\Gamma$ expressible as a product of at most $m$ factors drawn from $S \cup S^{-1}$.

The constant is allowed to depend on $S$, and the conclusion is asserted for every finite generating set. It gives exponential growth in the sense of the published growth bundle: at $m = 0$ the ball is $\{1\}$ and $v^0 = 1$, so the restriction to $m \ge 1$ costs nothing, and the single generating set that definition asks for can be taken to be any one of them.

The hypothesis is not vacuous, and it is strictly stronger than it may look. Taking the trivial subgroup shows it forces $\Gamma$ to be infinite, and taking $\Gamma$ itself shows it forces $\Gamma$ to be non-nilpotent; both are intended. Groups satisfying it exist — for instance $\mathbb{Z}^2 \rtimes_A \mathbb{Z}$ for a hyperbolic $A \in SL_2(\mathbb{Z})$, which is polycyclic and has no nilpotent subgroup of finite index.

The hypothesis is spelled out rather than named, but it is exactly Mathlib's Group.IsVirtuallyNilpotent negated: that predicate is defined as the existence of a nilpotent subgroup of finite index, with the same two conjuncts in the same order, so the two are the same proposition by unfolding. It is written out here to match the form in which Wolf's Theorem 4.3 states it.