Read-back

The single declaration in the file

Setting fixed by the binders

Let $n$ be a natural number (so $n = 0$ is allowed). Throughout, the ambient group is

$$\Gamma_n \;=\; \mathbb{Z}^n \;=\; \{\,x : \{0,1,\dots,n-1\} \to \mathbb{Z}\,\},$$

the set of all functions from an $n$-element index set to $\mathbb{Z}$, carrying the group structure obtained from componentwise addition but written multiplicatively: the product $x \cdot y$ is the function $i \mapsto x(i) + y(i)$, the identity element $1$ is the zero function $i \mapsto 0$, and the inverse $x^{-1}$ is the function $i \mapsto -x(i)$. This is the free abelian group of rank $n$; it is abelian, and for $n = 0$ it is the trivial group with exactly one element. No additional structure and no typeclass hypotheses are assumed: the group structure above is the only one in play, and it is determined by $n$.

The statement also fixes:

• a finite subset $T \subseteq \Gamma_n$ (a finite set of elements, listed without repetition);
• a hypothesis $\mathrm{(H1)}$: the smallest subgroup of $\Gamma_n$ containing $T$ is all of $\Gamma_n$ — that is, $T$ generates $\Gamma_n$;
• a hypothesis $\mathrm{(H2)}$: the number of elements of $T$ is exactly $n$, i.e. $\#T = n$.

Both hypotheses are simultaneously satisfiable for every $n$: for $n \ge 1$ the standard basis $\{e_1,\dots,e_n\}$ is a generating set with exactly $n$ elements, and for $n = 0$, $\mathrm{(H2)}$ forces $T = \emptyset$, which does generate the trivial group. So neither hypothesis is vacuous.

The growth function being used

For a finite subset $S$ of a group $G$ and a natural number $m$, the quantity written below as $g_S(m)$ is defined as the number of elements of the set

$$B_S(m) \;=\; \Bigl\{\, g \in G \;\Bigm|\; \exists\, k \le m \text{ and } x_1,\dots,x_k \in G \text{ with } (\forall\, j)\ \bigl(x_j \in S \text{ or } x_j^{-1} \in S\bigr),\ \ g = x_1 x_2 \cdots x_k \,\Bigr\}.$$

Spelled out precisely: $g$ belongs to $B_S(m)$ exactly when there is a finite list of elements of $G$, of length at most $m$ (not exactly $m$), each entry of which either lies in $S$ or has its inverse in $S$, whose product — formed by multiplying from the right, i.e. $x_1\cdot(x_2\cdot(\cdots(x_k\cdot 1)))$, though the group here is abelian so the order and bracketing are immaterial — equals $g$. Entries may repeat, and the empty list (length $0$) is allowed, so the identity element $1$ always lies in $B_S(m)$ for every $m$, including $m = 0$. Thus $B_S(m)$ is the ball of radius $m$ about the identity in the word metric determined by $S \cup S^{-1}$.

The count $g_S(m)$ is the cardinality of $B_S(m)$ taken as a natural number, with the convention that an infinite set is assigned the value $0$. (The statement does not separately assert that these balls are finite; that is left implicit in whatever the two claims below say about the numbers.)

What the declaration asserts

Under the hypotheses above, the declaration asserts the conjunction of the following two claims.

First claim — an exact count for the given generating set $T$. For every natural number $m$ (including $m = 0$),

$$g_T(m) \;=\; \sum_{l=0}^{n} 2^{l}\,\binom{n}{l}\binom{m}{l},$$

an equality of natural numbers. The sum runs over the integers $l$ with $0 \le l \le n$, i.e. over $n+1$ terms, and each term is the product $\bigl(2^{l} \cdot \binom{n}{l}\bigr) \cdot \binom{m}{l}$ computed in the natural numbers. Both binomial coefficients use the natural-number convention $\binom{a}{b} = 0$ whenever $b > a$; consequently every term with $l > m$ vanishes, and the sum is effectively over $0 \le l \le \min(n,m)$. In the degenerate case $m = 0$ only the $l = 0$ term survives and the right-hand side is $1$; in the degenerate case $n = 0$ the sum has the single term $l = 0$ and is again $1$ for every $m$.

Second claim — two-sided polynomial bounds for every generating set. For every finite subset $S \subseteq \Gamma_n$ such that the smallest subgroup containing $S$ is all of $\Gamma_n$ (i.e. $S$ generates; no condition whatsoever is placed on the number of elements of $S$), there exist real numbers $c_1, c_2$ such that

$$0 < c_1, \qquad c_1 \le c_2, \qquad \text{and} \qquad \forall\, m \in \mathbb{N} \text{ with } m \ge 1:\quad c_1\, m^{n} \;\le\; g_S(m) \;\le\; c_2\, m^{n}.$$

Here $m^n$ means the real number $m$ (the natural number $m$ viewed as a real) raised to the natural-number power $n$, and $c_i\,m^n$ is the product $c_i \cdot (m^n)$; the counts $g_S(m)$ are natural numbers viewed as reals. The constants $c_1, c_2$ are chosen after $S$ is given, so they may depend on $S$ (and on $n$); they are not claimed to be uniform over generating sets. Both inequalities are non-strict ($\le$, not $<$), and the quantifier over $m$ ranges only over $m \ge 1$, so the case $m = 0$ is excluded from the bounds. The positivity requirement is stated for $c_1$ only; that $c_2 > 0$ follows from $0 < c_1 \le c_2$.

Degenerate cases silently included: when $n = 0$ the exponent is $0$, so $m^n = 1$ for all $m \ge 1$ and the claim reads $c_1 \le g_S(m) \le c_2$; and $S = \emptyset$ is permitted as a generating set precisely when $\Gamma_n$ is trivial, i.e. when $n = 0$.

The second claim mentions $T$ nowhere; $T$ enters it only through the number $n$, which the hypotheses tie to $\#T$. The whole conclusion is a conjunction, so both claims are asserted together for the same fixed $n$, $T$.