Read-back of the single declaration in the artifact

The file contains exactly one declaration: a theorem whose proof is omitted. What follows renders its statement in full. Everything the statement depends on is expanded here, so nothing below needs the source files.

---

1. The ambient data and the standing hypotheses

The statement begins by fixing:

• a type $\Gamma$, living in an arbitrary universe (the universe is an implicit parameter and is otherwise unconstrained);
• a group structure on $\Gamma$ (multiplication, identity $1$, inversion, with the group axioms). $\Gamma$ is not assumed abelian, nor finite, nor nonempty-by-fiat beyond containing $1$.

and then three hypotheses, all supplied as typeclass (instance) assumptions rather than named hypotheses, so they are available throughout but are never referred to by name in the conclusion:

(H1) $\Gamma$ is a group. As above.

(H2) $\Gamma$ is finitely generated. Literally: the improper subgroup $\Gamma \le \Gamma$ is finitely generated, which unfolds to: there is a finite subset $S \subseteq \Gamma$ whose generated subgroup is all of $\Gamma$. Here the generated subgroup of a subset $k$ is the intersection of all subgroups of $\Gamma$ containing $k$ — the smallest subgroup containing $k$.

(H3) $\Gamma$ is solvable. Literally: there exists $n \in \mathbb{N}$ with $D^n(\Gamma) = \{1\}$, where the derived series is

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

and for subgroups $H_1, H_2$ the bracket $[H_1, H_2]$ denotes the subgroup generated by the set of commutators $\{\, g_1 g_2 g_1^{-1} g_2^{-1} \;:\; g_1 \in H_1,\ g_2 \in H_2 \,\}$ (not that set itself). The commutator convention is $[g_1, g_2] = g_1 g_2 g_1^{-1} g_2^{-1}$.

Note that (H3) is solvable, not polycyclic and not nilpotent; and $n$ is not bounded.

---

2. Word balls and the counting convention

All the growth notions below are stated in terms of the following object. For a group $G$, an arbitrary subset $S \subseteq G$ and an $n \in \mathbb{N}$, the word ball

$$B_S(n) \;=\; \bigl\{\, g \in G \;:\; \text{there is a finite list } (x_1, \dots, x_l) \text{ of elements of } G \text{ with } l \le n,\ \ (\forall i)\ \bigl(x_i \in S \ \text{or}\ x_i^{-1} \in S\bigr),\ \text{and } x_1 x_2 \cdots x_l = g \,\bigr\}.$$

Four points about this, all of which are consequences of how it is literally written:

• The list is a list, not a set: repetitions are allowed and the order is fixed. The product is taken in list order — it is defined by folding multiplication from the right against the identity, i.e. $x_1\bigl(x_2(\cdots(x_l \cdot 1))\bigr)$, which by associativity is the ordinary ordered product $x_1 x_2 \cdots x_l$.
• The length bound is $l \le n$, not $l = n$. The empty list ($l = 0$) is permitted and its product is $1$, so $1 \in B_S(n)$ for every $n$, and in particular $B_S(0) = \{1\}$. Also $B_S(m) \subseteq B_S(n)$ whenever $m \le n$.
• The letters $x_i$ range over all of $G$, constrained only by $x_i \in S$ or $x_i^{-1} \in S$. So $S$ is implicitly symmetrized: the ball is built from $S \cup S^{-1}$, and $S$ itself is not required to be symmetric or to contain $1$.
• $S$ is an arbitrary subset here; in the growth definitions it will be the underlying set of a finite subset.

Counting convention. Where a cardinality of $B_S(n)$ appears, it is the number of elements of $B_S(n)$ as a natural number, with the convention that an infinite set is assigned the value $0$. Write $\#B_S(n)$ for this natural number. This convention matters below and is flagged where it does.

---

3. The two growth notions, expanded

Exponential growth. A group $G$ has exponential growth means, literally:

there exists a finite subset $S \subseteq G$ whose generated subgroup is all of $G$, and there exists a real number $c$ with $1 < c$ (strict), such that for every $n \in \mathbb{N}$,

$$c^{\,n} \;\le\; \#B_S(n)$$

(non-strict inequality; the right-hand side is the natural number $\#B_S(n)$ regarded as a real).

Two things this does and does not say. The generating set is quantified existentially: the inequality is required to hold for some finite generating set, not for all of them. And the inequality is required for all $n$ including $n = 0$, where it reads $1 \le \#\{1\} = 1$. Because of the counting convention, if some ball $B_S(n)$ with $n \ge 1$ were infinite its count would be $0$ and the inequality $c^n \le 0$ would fail; so this condition can only be met by a generating set all of whose balls are finite.

Polynomial growth of degree at most $E$, for a natural number $E$. A group $G$ has polynomial growth of degree $\le E$ means, literally:

there exists a finite subset $S \subseteq G$ whose generated subgroup is all of $G$, and there exists a real number $c$ with $0 < c$ (strict), such that for every $m \in \mathbb{N}$ with $1 \le m$,

$$\#B_S(m) \;\le\; c \cdot m^{E}.$$

Again the generating set is existential. The bound is imposed only for $m \ge 1$; the case $m = 0$ is excluded, so nothing is asserted about $\#B_S(0)$. The exponent $E$ is a natural number, so $E = 0$ is permitted and then the assertion is that $\#B_S(m) \le c$ for all $m \ge 1$, i.e. the balls are uniformly bounded. Here the counting convention cuts the other way: an infinite ball would be counted as $0$, and $0 \le c\, m^E$ holds automatically, so an infinite ball would satisfy rather than violate this inequality.

The quantity counted in this definition is written via an intermediate name (a "growth function"), but that name is defined to be exactly $\#B_S(m)$ for the same word ball as above, so the two definitions count the same thing.

---

4. Polycyclic, expanded

A group $G$ is polycyclic means, literally: there exist a natural number $t$ and a family of subgroups $A_0, A_1, \dots, A_t$ of $G$ (indexed by $\{0, 1, \dots, t\}$) such that

1. $A_0 = G$ (the improper subgroup);
2. $A_t = \{1\}$ (the trivial subgroup);
3. for every $i \in \{0, 1, \dots, t-1\}$, both of the following hold:
   • $A_{i+1} \le A_i$, and
   • writing $A_{i+1}\!\restriction_{A_i}$ for the subgroup of $A_i$ obtained by pulling $A_{i+1}$ back along the inclusion $A_i \hookrightarrow G$ — that is, $A_{i+1} \cap A_i$ regarded as a subgroup of the group $A_i$, which in the presence of the containment just stated is $A_{i+1}$ itself — the subgroup $A_{i+1}\!\restriction_{A_i}$ is normal in $A_i$ and the quotient group

$$A_i \big/ A_{i+1}\!\restriction_{A_i}$$

 is **cyclic**, meaning: there is an element $g$ of that quotient such that every element of the
 quotient is $g^{\,k}$ for some $k \in \mathbb{Z}$.

Points worth making explicit. The normality and the cyclicity are packaged together (the normality witness is what makes the quotient a group at all, and it is a proposition, so requiring its existence is the same as requiring normality); the net content of the third clause is "each consecutive quotient is a normal subgroup with cyclic quotient". "Cyclic" here includes the trivial group and both the finite and the infinite cyclic groups. The subgroups $A_i$ are required to be normal only in $A_i$, not in $G$. The chain is descending from $G$ to $\{1\}$, of some finite length $t$ that is existentially quantified and otherwise unconstrained. The degenerate case $t = 0$ is allowed: then the family is the single subgroup $A_0$, clause 3 is vacuous, and clauses 1 and 2 read $A_0 = G$ and $A_0 = \{1\}$ together — so $t = 0$ is satisfiable exactly when $G$ is trivial.

---

5. The numerical exponent, expanded

The polynomial-growth degree appearing in the theorem is a specific natural number attached to a group $H$. It is built in four layers.

(a) Lower central series, in the indexing the definition actually uses. For a group $H$ set

$$\Gamma_0(H) = H, \qquad \Gamma_{k+1}(H) = [\,\Gamma_k(H),\, H\,],$$

the bracket again being the subgroup generated by the relevant commutators. Note the indexing starts at $\Gamma_0 = H$ (so $\Gamma_1 = [H,H]$); in the more common $1$-based convention this $\Gamma_k$ is the $(k+1)$-st term.

(b) Nilpotency class, with its junk value. The upper central series of $H$ is

$$Z_0 = \{1\}, \qquad Z_{n+1} = \{\, x \in H \;:\; [x,y] \in Z_n \text{ for all } y \in H \,\},$$

and $H$ is nilpotent iff $Z_n = H$ for some $n$. The nilpotency class $c(H)$ is the least such $n$ when $H$ is nilpotent, and is defined to be $0$ when $H$ is not nilpotent. So the value $0$ is ambiguous between "trivial group" and "not nilpotent at all".

(c) The $k$-th factor and its rank. For $k \in \mathbb{N}$, take the abelianization of $\Gamma_k(H)$ — that is, $\Gamma_k(H)\big/[\Gamma_k(H), \Gamma_k(H)]$ — and quotient it further by the image, under the abelianization map, of the subgroup $\Gamma_{k+1}(H) \cap \Gamma_k(H)$ viewed inside $\Gamma_k(H)$. Call the resulting abelian group $F_k(H)$. (Every subgroup of an abelian group is normal, so this second quotient is formed without an extra hypothesis.)

Regard $F_k(H)$ additively, as a module over $\mathbb{Z}$, with $n \cdot x$ the $n$-th power of $x$ in $F_k(H)$. Then

$$r_k(H) \;=\; \text{the } \mathbb{Z}\text{-rank of } F_k(H),$$

where "rank" is: take the supremum, as a cardinal, of the cardinalities of the $\mathbb{Z}$-linearly independent subsets of $F_k(H)$, and convert that cardinal to a natural number with the convention that an infinite cardinal is sent to $0$. Consequences of this convention that the reader should not miss: a finite $F_k(H)$, or more generally a torsion one, gives $r_k(H) = 0$; and an $F_k(H)$ of infinite rank also gives $r_k(H) = 0$. So $r_k(H)$ records only a finite free rank, and $0$ is again ambiguous.

(d) The exponent. Finally

$$E_2(H) \;=\; \sum_{k=0}^{c(H)-1} 2^{\,k} \cdot r_k(H),$$

the sum being over $k \in \{0, 1, \dots, c(H)-1\}$ — the weights are powers of $2$, not the weights $k+1$ of the other exponent defined alongside it in the same source, which this statement does not use. If $c(H) = 0$ the index set is empty and $E_2(H) = 0$.

---

6. The statement itself

With $\Gamma$ a finitely generated solvable group as in §1, the theorem asserts the conjunction of the following two claims.

Claim (a). For every subgroup $\Delta$ of $\Gamma$, if

• $\Delta$, regarded as a group in its own right (the type of elements of $\Gamma$ lying in $\Delta$, with the inherited multiplication), is nilpotent in the sense of §5(b); and
• $\Delta$ has finite index in $\Gamma$, which unfolds to: the number of cosets in the quotient $\Gamma/\Delta$, counted as a natural number under the same "infinite $\mapsto 0$" convention, is $\ne 0$ — i.e. that quotient is finite,

then both

• $\Gamma$ is polycyclic in the sense of §4, and
• $\Gamma$ has polynomial growth of degree at most $E_2(\Delta)$ in the sense of §3, where the exponent is computed from $\Delta$'s own lower central series and nilpotency class as in §5, not from $\Gamma$'s.

Claim (b). If there is no subgroup $\Delta$ of $\Gamma$ that is simultaneously nilpotent and of finite index — i.e. the negation of "$\exists \Delta \le \Gamma$ with $\Delta$ nilpotent and $\Delta$ of finite index" — then $\Gamma$ has exponential growth in the sense of §3.

---

7. Quantifier structure, degenerate cases, and what the shape forces

• The two claims have complementary antecedents: (a)'s hypothesis is that a given $\Delta$ is nilpotent of finite index, and (b)'s hypothesis is that no such $\Delta$ exists. Exactly one of "some nilpotent finite-index subgroup exists" and "none does" holds of any $\Gamma$, so in each case one of the two claims is vacuously true and the other carries the content.

• In claim (a) the quantifier over $\Delta$ is universal, and the conclusion's first half, "$\Gamma$ is polycyclic", does not mention $\Delta$. So (a) says: if at least one nilpotent finite-index subgroup exists then $\Gamma$ is polycyclic; and the polynomial bound is asserted with the exponent $E_2(\Delta)$ for every qualifying $\Delta$, which is the strongest such statement (equivalently, with the smallest exponent arising this way). It does not merely assert the bound for one convenient $\Delta$.

• $\Delta = \{1\}$ always satisfies the nilpotence requirement (the trivial group is nilpotent, of class $0$). It satisfies the finite-index requirement exactly when $\Gamma$ is finite. When $\Gamma$ is finite, then, (a) applies with this $\Delta$, and since $c(\{1\}) = 0$ we get $E_2(\{1\}) = 0$: so for finite $\Gamma$ the claim includes "$\Gamma$ is polycyclic" and "$\#B_S(m) \le c$ for all $m \ge 1$, for some finite generating set $S$ and some $c > 0$".

• $\Delta = \Gamma$ satisfies the finite-index requirement always (the quotient has one element), and the nilpotence requirement exactly when $\Gamma$ itself is nilpotent; in that case (a) applies with exponent $E_2(\Gamma)$.

• No hypothesis beyond nilpotence and finite index is placed on $\Delta$ — in particular $\Delta$ is not assumed normal in $\Gamma$, and the coset space $\Gamma/\Delta$ in the index is a space of cosets, not necessarily a group.

• Both growth conditions are existential in the generating set, so neither claim asserts anything about an arbitrary finite generating set of $\Gamma$; nothing in the statement asserts that the growth type or the bound is independent of the choice of generators.

• The exponent $E_2(\Delta)$ is asserted only as an upper bound on the degree ($\le$, and the bound is $c \cdot m^{E_2(\Delta)}$ with $c$ existentially quantified). Nothing asserts that this degree is attained, sharp, or minimal, and nothing asserts a matching lower bound.

• The two exponents built in the imported source differ in their weights ($2^k$ versus $k+1$); this statement uses the $2^k$ one only.

• Claim (b) concludes exponential growth with some base $c > 1$; no particular base, and no relation between $c$ and any invariant of $\Gamma$, is asserted.

• The proof of the theorem is not part of what is being read back here.