Read-back

The file contains a single theorem. What follows is a rendering of exactly what it asserts.

Setting

Let $\Gamma$ be a type (in an arbitrary universe; it is an implicit argument, so it is universally quantified and inferred from the rest of the data), equipped with a group structure. The group structure is a further universally quantified argument: the statement is about the pair "type together with a chosen group structure on it", not about a type alone. No finiteness, countability, commutativity or decidability assumption is placed on $\Gamma$.

Throughout, $1$ denotes the identity of $\Gamma$, and for a subgroup $H$ the symbol $\{1\}$ denotes the trivial subgroup.

Hypotheses

There are four hypotheses. Two are quantified data ($\Gamma$'s group structure, and the set $S$ below), and all four must hold.

1. $\Gamma$ is solvable

This is assumed as a structural property of $\Gamma$. Unfolded, it says: there exists a natural number $n$ such that the $n$-th term of the derived series of $\Gamma$ is the trivial subgroup, where the derived series is defined by

$$D^0(\Gamma) = \Gamma, \qquad D^{k+1}(\Gamma) = \big[\, D^k(\Gamma),\, D^k(\Gamma) \,\big],$$

and where, for subgroups $H_1, H_2 \le \Gamma$, the subgroup $[H_1, H_2]$ is the subgroup generated by (not merely the set of) all elements $g_1 g_2 g_1^{-1} g_2^{-1}$ with $g_1 \in H_1$ and $g_2 \in H_2$.

Note that $n = 0$ is permitted, in which case the condition reads $\Gamma = \{1\}$.

2. $\Gamma$ is not polycyclic

This is the negation of an existential statement, which is spelled out here in full because the notion is defined in the accompanying files rather than taken from the library.

$\Gamma$ would be polycyclic if there existed a natural number $t$ and a family of subgroups

$$A_0,\ A_1,\ \dots,\ A_t \ \le\ \Gamma$$

— exactly $t+1$ subgroups, indexed by $0, 1, \dots, t$ — such that all of the following hold:

• $A_0 = \Gamma$ (the whole group, as a subgroup of itself);
• $A_t = \{1\}$;
• for every index $i$ with $0 \le i < t$:

  • $A_{i+1} \subseteq A_i$ (the chain is descending, and this is required explicitly rather than being a consequence of the other conditions);

  • $A_{i+1}$, viewed as a subgroup of the group $A_i$, is normal in $A_i$ — normality is required only relative to $A_i$, not relative to $\Gamma$;

  • the quotient group $A_i / A_{i+1}$ — formed as the set of left cosets of $A_{i+1}$ inside $A_i$, with the group structure supplied by the normality just required — is cyclic, meaning: there exists an element $g$ of that quotient such that the map $k \mapsto g^k$ from $\mathbb{Z}$ to the quotient is surjective.

    "Cyclic" in this sense includes the trivial group ($g = 1$) and infinite cyclic groups; it does not require the quotient to be finite.

The hypothesis is that no such $t$ and no such family of subgroups exist.

Degenerate case worth noting: $t = 0$ is allowed in the definition of polycyclic, and it forces $A_0$ to be simultaneously $\Gamma$ and $\{1\}$. Hence the trivial group is polycyclic, and so this hypothesis in particular rules out $\Gamma$ being trivial. Repetitions are allowed in the chain (consecutive terms may be equal, giving a trivial quotient), so the length $t$ is not required to be minimal or the chain strictly decreasing.

3. A finite subset $S$

$S$ is a finite subset of $\Gamma$, given as explicit data (a finite set of elements, not a subtype). It is universally quantified: the conclusion is asserted for every such $S$ satisfying the next hypothesis. $S$ is not required to be nonempty, nor closed under inversion, nor to avoid the identity.

4. $S$ generates $\Gamma$

The smallest subgroup of $\Gamma$ containing $S$ (equivalently, the intersection of all subgroups of $\Gamma$ containing $S$) is all of $\Gamma$.

Together, hypotheses 3 and 4 say that $\Gamma$ is finitely generated, with $S$ as a chosen finite generating set.

Conclusion

Before stating it, here is the quantity that appears in it, expanded.

The ball of radius $m$. For a natural number $m$, let

$$B_S(m) \ = \ \Big\{\, g \in \Gamma \ \Big|\ \exists\, k \le m \text{ and } x_1, \dots, x_k \in \Gamma \text{ with } \big(x_j \in S \text{ or } x_j^{-1} \in S\big) \text{ for each } j, \text{ and } g = x_1 x_2 \cdots x_k \,\Big\}.$$

Three points of precision about this set:

• The list $x_1, \dots, x_k$ is an ordered list and may repeat entries; the product is taken in the listed order, $x_1$ leftmost. (Because $\Gamma$ is a group, the bracketing is immaterial; the order is not.)
• The length condition is $k \le m$, not $k = m$. In particular $k = 0$ is always allowed, the empty product being $1$, so $1 \in B_S(m)$ for every $m$, and $B_S(0) = \{1\}$.
• Each letter is required to lie in $S$ or to have its inverse in $S$; so $B_S(m)$ is the set of elements expressible as a product of at most $m$ elements of $S \cup S^{-1}$.

Its cardinality. The quantity in the conclusion is the number of elements of $B_S(m)$, taken as a natural number by a total "cardinality" operation that returns $0$ when the set is infinite. Since $S$ is finite, $B_S(m)$ is finite for every $m$ and this junk value never arises here; the number is the honest cardinality. This natural number is then converted to a real number.

The assertion. The theorem asserts:

There exists a real number $c$ such that $c > 1$ and, for every natural number $m$ with $m \ge 1$,

$$c^{\,m} \ \le \ \#\, B_S(m).$$

Points of logical precision:

• The quantifier order is $\exists c\, \forall m$: a single $c$ works for all $m \ge 1$. The number $c$ is allowed to depend on $\Gamma$, on its group structure, and on $S$; the existential is inside the scope of all four hypotheses.
• Since $S$ itself is universally quantified, the assertion is made for every finite generating set of $\Gamma$, with a $c$ chosen after $S$ is given.
• The inequality is non-strict ($\le$), and the strict inequality $1 < c$ on the base is strict.
• It is $\exists$, not $\exists!$; nothing is claimed about uniqueness, maximality, or the supremum of admissible $c$.
• The exponent $m$ is a natural number and $c^m$ is the $m$-fold product of $c$ with itself.
• The case $m = 0$ is excluded from the conclusion by the hypothesis $m \ge 1$. (For $m = 0$ the inequality would read $1 \le \# B_S(0) = 1$.)
• The statement gives a lower bound only. It says nothing about any matching upper bound, about a limit or growth rate existing, or about the behaviour of $\# B_S(m)$ being eventually monotone or submultiplicative.

Satisfiability of the hypotheses

The hypotheses are not vacuous: they ask for a finitely generated solvable group admitting no finite subnormal chain from the whole group to the trivial subgroup with cyclic successive quotients, and such groups exist. Note, however, that hypothesis 2 does the work of excluding the degenerate configurations under which the conclusion could not hold — for instance $S = \varnothing$, which by hypothesis 4 would force $\Gamma$ to be trivial and hence $\# B_S(m) = 1$ for all $m$, contradicting $c^m \le 1$ with $c > 1$; the trivial group is polycyclic, so hypothesis 2 already excludes it.