Read-back: exists_const_pow_le_growthFunction_of_le_sub_and_of_le_mul

Setting and the quantities involved

Fix a type $\Gamma$ (in an arbitrary universe) carrying a group structure, and a finite subset $S \subseteq \Gamma$. The type $\Gamma$ and its group structure are supplied implicitly; the finite set $S$ is the one explicit datum the statement takes. Nothing else is assumed about $S$: it is not assumed to generate $\Gamma$, not assumed nonempty, and not assumed symmetric (closed under inversion). $\Gamma$ need not be finitely generated, finite, or infinite.

For a natural number $m$, let

$$B_S(m) \;=\; \bigl\{\, g \in \Gamma \;:\; g = x_1 x_2 \cdots x_k \text{ for some } k \le m \text{ and some } x_1,\dots,x_k \in \Gamma \text{ with } x_i \in S \text{ or } x_i^{-1} \in S \text{ for each } i \,\bigr\}.$$

That is, $B_S(m)$ is the closed ball of radius $m$: the set of elements expressible as an ordered product of at most $m$ factors, each factor drawn from $S \cup S^{-1}$. The sequence of factors is a finite list, the product is taken in the listed order, and the case $k = 0$ (the empty product) is permitted, so the identity element $1$ lies in $B_S(m)$ for every $m$, including $m = 0$; indeed $B_S(0) = \{1\}$.

Let

$$\beta_S(m) \;=\; \lvert B_S(m) \rvert \in \mathbb{N}$$

be the number of elements of that ball. Because $S$ is finite, $B_S(m)$ is a finite set for every $m$, so $\beta_S(m)$ is a genuine cardinality (the underlying cardinality operator would return the junk value $0$ on an infinite set, but that case cannot arise here). In particular $\beta_S(m) \ge 1$ for every $m$, and $\beta_S(0) = 1$.

Throughout, $\beta_S(m)$ is compared against real numbers by regarding the natural number $\beta_S(m)$ as a real number.

What is asserted

For every such $\Gamma$ and every finite $S \subseteq \Gamma$, the assertion is the conjunction of the following two independent statements (A) and (B). They share no variables: the $q$ and $c$ of (A) are quantified separately from the $q$ and $c$ of (B).

(A)

For all natural numbers $r$ and $q$, and all real numbers $c$ with $c > 0$:

if

$$c \cdot (m - r)^{\,q} \;\le\; \beta_S(m) \qquad \text{for every natural number } m \ge 1,$$

then there exists a real number $c' > 0$ such that

$$c' \cdot m^{\,q} \;\le\; \beta_S(m) \qquad \text{for every natural number } m \ge 1.$$

Here $m - r$ is subtraction of real numbers — the naturals $m$ and $r$ are each converted to real numbers first and the difference is then a real number, possibly negative. It is not truncated subtraction of naturals. The exponent $q$ is a natural number, so $(m-r)^q$ means the $q$-fold product of $m - r$ with itself, with the convention $x^0 = 1$ for every real $x$ (including $x = 0$ and $x < 0$).

(B)

For all natural numbers $l$ and $q$, and all real numbers $c$, with $l > 0$ and $c > 0$:

if

$$c \cdot (l m)^{\,q} \;\le\; \beta_S(l m) \qquad \text{for every natural number } m \ge 1,$$

then there exists a real number $c'' > 0$ such that

$$c'' \cdot m^{\,q} \;\le\; \beta_S(m) \qquad \text{for every natural number } m \ge 1.$$

In (B)'s hypothesis, both the polynomial and the ball radius are evaluated at the same product $l m$: the hypothesis is a lower bound $c \cdot (lm)^q \le \beta_S(lm)$ at the points $l, 2l, 3l, \dots$ only, and says nothing at the radii that are not positive multiples of $l$. The product $lm$ is formed in the natural numbers and then converted to a real number as the base of the power.

The two conclusions of (A) and (B) are word-for-word the same statement; only the name given to the witnessing constant differs.

Precision, scope of the quantifiers, and degenerate cases

• All inequalities are non-strict ($\le$) where written $\le$, and strict ($<$) only in the positivity conditions $0 < c$, $0 < c'$, $0 < c''$, $0 < l$. The positivity of the constants is over the reals; $0 < l$ is over the naturals, i.e. $l \ge 1$.

• Radius $m = 0$ is excluded from all four families of inequalities, since each is guarded by $1 \le m$ (over the naturals). So neither hypothesis nor conclusion says anything at $m = 0$.

• The existential constants are merely asserted to exist, not to be unique, computable, or related to $c$ in any stated way. In (A), $c'$ may depend on $\Gamma$, $S$, $r$, $q$, $c$ and on the hypothesis itself; in (B), $c''$ may likewise depend on $\Gamma$, $S$, $l$, $q$, $c$. No bound on $c'$ or $c''$ in terms of $c$ is claimed.

• Order of quantifiers. In both parts, $S$ is fixed before everything else; then the numerical parameters are fixed; then the hypothesis is assumed; and only then is the constant produced. So a single constant is not claimed to work for all $q$ or all $c$.

• The case $q = 0$. Since $x^0 = 1$ for every real $x$, (A)'s hypothesis degenerates to "$c \le \beta_S(m)$ for all $m \ge 1$" and its conclusion to "$c' \le \beta_S(m)$ for all $m \ge 1$"; the shift $r$ drops out entirely. The same degeneration happens in (B), where the multiplier $l$ then only restricts which radii the hypothesis speaks about.

• The case $r = 0$ in (A), and $l = 1$ in (B). In each, the hypothesis and the conclusion become literally the same inequality, so the implication is immediate with $c' = c$ (respectively $c'' = c$).

• Small radii in (A). For $q \ge 1$ and $m < r$ the quantity $(m-r)^q$ is negative when $q$ is odd and positive when $q$ is even; at $m = r$ it is $0$, so the hypothesis reads $0 \le \beta_S(r)$ there and is automatic. Thus for odd $q$ the hypothesis carries no content at radii below $r$, whereas for even $q$ it does.

• The hypotheses may be impossible to satisfy, making the implications vacuous. For example, if $S = \emptyset$ then $B_S(m) = \{1\}$ and $\beta_S(m) = 1$ for every $m$; then for any $q \ge 1$ and any $c > 0$ neither hypothesis can hold (the left side grows without bound). More generally, whenever $\beta_S$ is a bounded sequence — for instance when the subgroup generated by $S$ is finite — both implications are vacuously satisfied for every $q \ge 1$. The statement therefore has content only for those $S$ whose ball-counting function does admit such a lower bound.

• What is compared. Every inequality compares a real number on the left with the natural number $\beta_S(\cdot)$ viewed as a real number on the right; the constant always multiplies the power, and the power's base is the radius (shifted by $r$ in (A)'s hypothesis, scaled by $l$ in (B)'s), never the constant.

• No claim about $\beta_S$ itself — no monotonicity, no submultiplicativity, no upper bound, and no relation between the balls at different radii — is asserted anywhere; such properties appear neither as hypotheses nor as conclusions.