Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Wolf's growth function, polynomial growth, polycyclic groups and the growth exponents

Definition
MilnorWolf_Growth

by dbenbenn · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-growthgroup-theorypolycyclic-groupssolvable-groups

Wolf's definitions, which Milnor's addendum also uses, on top of the published Chou.wordBall.

  • growthFunction S m: Wolf's gS(m)g_S(m)gS​(m), the number of elements expressible as words of length ≤m\le m≤m based on the finite set SSS, taken as the size of the ball of radius mmm (products of at most mmm factors from S∪S−1S \cup S^{-1}S∪S−1).
  • HasPolynomialGrowthOfDegreeLE G E: for some finite generating set SSS there is c>0c > 0c>0 with gS(m)≤c mEg_S(m) \le c\, m^EgS​(m)≤cmE for every integer m≥1m \ge 1m≥1.
  • IsPolycyclic G: there is a chain G=A0⊇A1⊇⋯⊇At=1G = A_0 \supseteq A_1 \supseteq \cdots \supseteq A_t = 1G=A0​⊇A1​⊇⋯⊇At​=1 of subgroups, each Ai+1A_{i+1}Ai+1​ normal in AiA_iAi​, with every quotient Ai/Ai+1A_i/A_{i+1}Ai​/Ai+1​ cyclic (finite or infinite).
  • lcs G k, lcsFactor G k, lcsRank G k: the lower central series Γk\Gamma_kΓk​ (Γ0=G\Gamma_0 = GΓ0​=G, Γk+1=[Γ,Γk]\Gamma_{k+1} = [\Gamma, \Gamma_k]Γk+1​=[Γ,Γk​]), the abelian group Γk/Γk+1\Gamma_k/\Gamma_{k+1}Γk​/Γk+1​ (presented as a quotient of the abelianization of Γk\Gamma_kΓk​), and its Z\mathbb ZZ-rank nkn_knk​, the rank of its free abelian part.
  • growthExponentOne G, growthExponentTwo G: Wolf's E1=∑k=0s(k+1)nkE_1 = \sum_{k=0}^{s} (k+1) n_kE1​=∑k=0s​(k+1)nk​ and E2=∑k=0s2knkE_2 = \sum_{k=0}^{s} 2^k n_kE2​=∑k=0s​2knk​, the sum running over k<s+1k < s + 1k<s+1 where s+1s + 1s+1 is the nilpotency class (so both are 000 for a group that is not nilpotent).

No theorem is stated here.

Definition code
import Definitions.Def_Chou_Growth
import Mathlib

/-!
# Growth of finitely generated groups: Wolf's definitions (J. Differential Geometry 2 (1968))

J. A. Wolf, *Growth of finitely generated solvable groups and curvature of Riemannian manifolds*,
J. Differential Geometry 2 (1968) 421–446; J. Milnor, *Growth of finitely generated solvable
groups*, ibid. 447–449, refers to Wolf for these definitions.

For a finite subset `S` of a group `Γ`, Wolf's growth function `g_S(m)` (p. 426) counts the
elements expressible as words of length `≤ m` based on `S`, a word `s₁^{a₁} ⋯ s_r^{a_r}` having
length `|a₁| + ⋯ + |a_r|`; `g_S(m)` is taken here as the size of the ball `Chou.wordBall S m` of the
published growth bundle, the set of products of at most `m` factors from `S ∪ S⁻¹`.  `Γ` has *polynomial
growth of degree `≤ E`* (p. 431) if `g_S(m) ≤ c m^E` for some finite generating set `S`, some
`c > 0` and every `m ≥ 1`; exponential growth is `Chou.HasExponentialGrowth`.  A solvable group is
*polycyclic* (Proposition 4.1 (1), p. 433) if it has a normal series with every quotient finite or
infinite cyclic; here, as in Kurosh, a normal series is a chain in which each term is normal in the
preceding one.  For a finitely generated nilpotent group with lower central series
`Γ = Γ₀ ⊇ Γ₁ ⊇ ⋯ ⊇ Γ_s ⊇ Γ_{s+1} = 1`, each `Γ_k/Γ_{k+1}` is a finitely generated abelian group
`A_k × B_k` with `A_k` finite and `B_k` free abelian of rank `n_k`, and Wolf's growth exponents
(3.3) are `E₁ = ∑ (k+1) n_k` and `E₂ = ∑ 2^k n_k`.  The rank `n_k` is taken as the `ℤ`-rank of
the abelian group `Γ_k/Γ_{k+1}`, presented as a quotient of the abelianization of `Γ_k` so that
its commutativity is available by construction; the sum runs over `k < s + 1`, Mathlib's
`Group.nilpotencyClass` (which is `0`, giving an empty sum, when the group is not nilpotent).
-/

namespace MilnorWolf

open Chou

/-- Wolf's growth function `g_S(m)` (p. 426), “the number of distinct elements of `Γ` expressible as
words of length `≤ m` based on `S`”, taken here as the size of the ball `Chou.wordBall S m`. -/
noncomputable def growthFunction {G : Type*} [Group G] (S : Finset G) (m : ℕ) : ℕ :=
  Nat.card (wordBall (S : Set G) m)

/-- Wolf, p. 431: `Γ` has polynomial growth of degree `≤ E` if for some finite generating set `S`
there is a constant `c > 0` with `g_S(m) ≤ c m^E` for every integer `m ≥ 1`. -/
def HasPolynomialGrowthOfDegreeLE (G : Type*) [Group G] (E : ℕ) : Prop :=
  ∃ S : Finset G, Subgroup.closure (S : Set G) = ⊤ ∧
    ∃ c : ℝ, 0 < c ∧ ∀ m : ℕ, 1 ≤ m → (growthFunction S m : ℝ) ≤ c * (m : ℝ) ^ E

/-- Wolf, Proposition 4.1 (1) (p. 433): a group is polycyclic if it has a normal series
`Γ = A₀ ⊇ A₁ ⊇ ⋯ ⊇ A_t = 1`, each `A_{i+1}` normal in `A_i`, with every quotient `A_i/A_{i+1}`
cyclic (finite or infinite). -/
def IsPolycyclic (G : Type*) [Group G] : Prop :=
  ∃ (t : ℕ) (A : Fin (t + 1) → Subgroup G), A 0 = ⊤ ∧ A (Fin.last t) = ⊥ ∧
    ∀ i : Fin t, A i.succ ≤ A i.castSucc ∧
      ∃ _ : ((A i.succ).subgroupOf (A i.castSucc)).Normal,
        IsCyclic (A i.castSucc ⧸ (A i.succ).subgroupOf (A i.castSucc))

/-- The `k`-th term `Γ_k` of the lower central series of `G`: `Γ₀ = G` and `Γ_{k+1} = ⁅Γ_k, G⁆` in
Mathlib's bracket order; Wolf writes `Γ_{k+1} = [Γ, Γ_k]`, the same subgroup by
`Subgroup.commutator_comm`. -/
abbrev lcs (G : Type*) [Group G] (k : ℕ) : Subgroup G :=
  (⊤ : Subgroup G).lowerCentralSeries k

/-- The abelian group `Γ_k/Γ_{k+1}` of the lower central series, realised as the quotient of the
abelianization of `Γ_k` by the image of `Γ_{k+1}`, so that it is a `CommGroup` by construction. -/
abbrev lcsFactor (G : Type*) [Group G] (k : ℕ) : Type _ :=
  Abelianization (lcs G k) ⧸
    Subgroup.map (Abelianization.of (G := lcs G k)) ((lcs G (k + 1)).subgroupOf (lcs G k))

/-- `n_k` of Wolf (3.3): the rank of the free abelian part of `Γ_k/Γ_{k+1}`, the `ℤ`-rank of that
abelian group. -/
noncomputable def lcsRank (G : Type*) [Group G] (k : ℕ) : ℕ :=
  Module.finrank ℤ (Additive (lcsFactor G k))

/-- Wolf's growth exponent `E₁(Γ) = ∑_{k=0}^{s} (k+1) n_k` of (3.3), for a nilpotent group with
`Γ_{s+1} = 1`; `s + 1` is Mathlib's `Group.nilpotencyClass`, which is `0` for a non-nilpotent
group, so that the sum is then empty. -/
noncomputable def growthExponentOne (G : Type*) [Group G] : ℕ :=
  ∑ k ∈ Finset.range (Group.nilpotencyClass G), (k + 1) * lcsRank G k

/-- Wolf's growth exponent `E₂(Γ) = ∑_{k=0}^{s} 2^k n_k` of (3.3). -/
noncomputable def growthExponentTwo (G : Type*) [Group G] : ℕ :=
  ∑ k ∈ Finset.range (Group.nilpotencyClass G), 2 ^ k * lcsRank G k

end MilnorWolf
Source
Wolf, J. A., Growth of finitely generated solvable groups and curvature of Riemannian manifolds, Journal of Differential Geometry 2 (1968) 421–446, https://doi.org/10.4310/jdg/1214428658, p. 426 (growth function), p. 431 (polynomial growth of degree ≤ E), Proposition 4.1 (1) p. 433 (polycyclic), (3.3) p. 426 (growth exponents); Milnor refers to Wolf for definitions (p. 447)
Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back: eight definitions

All eight declarations below are definitions, not theorems: each introduces a new symbol and fixes its meaning. Nothing below is asserted to be true or non-vacuous; what is recorded is what each symbol denotes.

Throughout, GGG denotes a type (in an arbitrary universe) carrying a group structure supplied as a typeclass assumption. In the first definition GGG is an implicit argument, inferred from the other arguments; in all the others it is given explicitly. Every definition applies to every group whatsoever: no finiteness, finite generation, nilpotence, solvability or commutativity is assumed anywhere.

Two conventions recur and are stated once here.

Counting. All cardinalities below are natural-number cardinalities, with the convention that an infinite set is assigned the value 000, exactly as an empty set is. So a cardinality of 000 records either "empty" or "infinite", and the two are not distinguished.

Ranks. The rank used below is the natural-number rank of a module: it is the supremum, over all subsets of the module that are linearly independent over the base ring, of the cardinality of that subset, converted to a natural number with the same convention — if that supremum is an infinite cardinal, the rank is 000.


1. The growth function of a finite subset

Given a group GGG, a finite subset S⊆GS \subseteq GS⊆G, and a natural number mmm, this defines a natural number, the number of elements of the ball of radius mmm.

The ball of radius mmm about the identity with respect to SSS is the set

BS(m)  =  { g∈G  ∣  ∃ ℓ≥0, ∃ x1,…,xℓ∈G: ℓ≤m, (∀j, xj∈S or xj−1∈S), x1x2⋯xℓ=g }.B_S(m) \;=\; \Bigl\{\, g \in G \;\Big|\; \exists\, \ell \ge 0,\ \exists\, x_1,\dots,x_\ell \in G :\ \ell \le m,\ \bigl(\forall j,\ x_j \in S \ \text{or}\ x_j^{-1} \in S\bigr),\ x_1 x_2\cdots x_\ell = g \,\Bigr\}.BS​(m)={g∈G​∃ℓ≥0, ∃x1​,…,xℓ​∈G: ℓ≤m, (∀j, xj​∈S or xj−1​∈S), x1​x2​⋯xℓ​=g}.

Points of detail, all of which are literally what is written:

  • The witness is a finite list x1,…,xℓx_1,\dots,x_\ellx1​,…,xℓ​ of elements of GGG, of length at most mmm, not exactly mmm. Repetitions are allowed; the xjx_jxj​ need not be distinct.
  • The product is taken in the order of the list, bracketed to the right against the identity: x1⋅(x2⋅(⋯⋅(xℓ⋅1)))x_1\cdot(x_2\cdot(\dots\cdot(x_\ell\cdot 1)))x1​⋅(x2​⋅(⋯⋅(xℓ​⋅1))). For a group this is the ordinary ordered product x1x2⋯xℓx_1x_2\cdots x_\ellx1​x2​⋯xℓ​.
  • The empty list (ℓ=0\ell = 0ℓ=0) is permitted, and its product is the identity. Hence the identity lies in BS(m)B_S(m)BS​(m) for every mmm, including m=0m = 0m=0, and BS(0)={1}B_S(0) = \{1\}BS​(0)={1}.
  • The condition on each letter is "xj∈Sx_j \in Sxj​∈S or xj−1∈Sx_j^{-1} \in Sxj−1​∈S". SSS itself is not required to be symmetric; the symmetrization is performed here, by the disjunction.
  • SSS is a finite subset, used through its underlying set {x:x∈S}\{x : x \in S\}{x:x∈S}. SSS may be empty, in which case only the identity is reachable and B∅(m)={1}B_\emptyset(m) = \{1\}B∅​(m)={1} for all mmm.

The value of the definition is the number of elements of BS(m)B_S(m)BS​(m), under the counting convention above: if BS(m)B_S(m)BS​(m) were infinite the value would be 000.

2. Polynomial growth of degree at most EEE

Given a group GGG and a natural number EEE, this defines a proposition. It holds precisely when:

there exists a finite subset S⊆GS \subseteq GS⊆G such that the subgroup generated by SSS is all of GGG, and there exists a real number ccc with c>0c > 0c>0 such that for every natural number mmm with m≥1m \ge 1m≥1,

∣BS(m)∣  ≤  c mE,\bigl|B_S(m)\bigr| \;\le\; c\,m^{E},​BS​(m)​≤cmE,

where ∣BS(m)∣|B_S(m)|∣BS​(m)∣ is the count of §1, cast from a natural number into the reals, mmm on the right is likewise cast into the reals, and mEm^EmE is the EEE-fold product of mmm with itself in the reals.

Points of detail:

  • "The subgroup generated by SSS" is the smallest subgroup of GGG containing SSS, i.e. the intersection of all subgroups containing SSS; the requirement is that this equals the whole group GGG.
  • The generating set is existentially quantified, and the constant ccc is existentially quantified after it, so ccc may depend on SSS. Nothing asserts the bound for every generating set.
  • The inequality is required only for m≥1m \ge 1m≥1. The case m=0m = 0m=0 is explicitly excluded, so no constraint is placed on ∣BS(0)∣|B_S(0)|∣BS​(0)∣.
  • The exponent EEE is a fixed natural number, and the bound is ≤\le≤, not <<<. The degenerate value E=0E = 0E=0 is allowed: the requirement is then ∣BS(m)∣≤c|B_S(m)| \le c∣BS​(m)∣≤c for all m≥1m \ge 1m≥1, since m0=1m^0 = 1m0=1 in the reals (including for mmm whose cast is 000 — but m≥1m \ge 1m≥1 there anyway).
  • ccc is required to be strictly positive, but no upper bound on ccc is imposed, and ccc need not be an integer.
  • Because an infinite set is counted as 000, any radius at which the ball were infinite would satisfy the inequality automatically rather than violating it.
  • SSS is permitted to be empty; the generation condition then forces GGG to be the trivial group.

3. Polycyclicity

Given a group GGG, this defines a proposition. It holds precisely when:

there exist a natural number ttt and a family of subgroups A0,A1,…,AtA_0, A_1, \dots, A_tA0​,A1​,…,At​ of GGG, indexed by the t+1t+1t+1 indices 0,1,…,t0,1,\dots,t0,1,…,t, such that

  1. A0=GA_0 = GA0​=G (the whole group);
  2. At={1}A_t = \{1\}At​={1} (the trivial subgroup);
  3. for every index iii with 0≤i≤t−10 \le i \le t-10≤i≤t−1, both of the following hold:
    • Ai+1≤AiA_{i+1} \le A_iAi+1​≤Ai​, and
    • writing HiH_iHi​ for the subgroup of the group AiA_iAi​ consisting of those x∈Aix \in A_ix∈Ai​ with x∈Ai+1x \in A_{i+1}x∈Ai+1​ (that is, Ai+1∩AiA_{i+1} \cap A_iAi+1​∩Ai​, regarded as living inside AiA_iAi​), the subgroup HiH_iHi​ is normal in AiA_iAi​, and the quotient group Ai/HiA_i / H_iAi​/Hi​ — taken with the group structure that this normality provides — is cyclic, meaning that there is an element ggg of Ai/HiA_i/H_iAi​/Hi​ for which the map n↦gnn \mapsto g^nn↦gn from Z\mathbb{Z}Z to Ai/HiA_i/H_iAi​/Hi​ is surjective.

Points of detail:

  • The normality of HiH_iHi​ in AiA_iAi​ and the cyclicity of Ai/HiA_i/H_iAi​/Hi​ are asserted together: the statement is "there is a proof of normality such that the resulting quotient group is cyclic", which amounts to the conjunction "HiH_iHi​ is normal in AiA_iAi​, and the quotient is cyclic". The cyclicity claim cannot even be phrased without the normality, since it is a claim about the quotient's group structure.
  • HiH_iHi​ is literally described as the intersection Ai+1∩AiA_{i+1}\cap A_iAi+1​∩Ai​ viewed inside AiA_iAi​, not as Ai+1A_{i+1}Ai+1​ itself; the inclusion Ai+1≤AiA_{i+1} \le A_iAi+1​≤Ai​ is imposed separately, in the same clause.
  • Cyclicity is stated via surjectivity of n↦gnn \mapsto g^nn↦gn for nnn ranging over all of Z\mathbb{Z}Z, so it covers both finite and infinite cyclic quotients. The trivial group is cyclic in this sense.
  • Nothing requires the chain to be strictly decreasing: Ai+1=AiA_{i+1} = A_iAi+1​=Ai​ is allowed at any step (the quotient is then trivial, hence cyclic).
  • Nothing requires any AiA_iAi​ to be normal in GGG; normality is required only of each term inside its immediate predecessor.
  • The degenerate case t=0t = 0t=0 is included. Then there is a single subgroup A0A_0A0​, conditions 1 and 2 read A0=GA_0 = GA0​=G and A0={1}A_0 = \{1\}A0​={1} simultaneously, and condition 3 is vacuous (there are no indices iii with 0≤i≤−10 \le i \le -10≤i≤−1). So t=0t = 0t=0 witnesses the property exactly when GGG is trivial.
  • ttt is existentially quantified with no bound, and the family is an arbitrary function of the index, subject only to the listed conditions.

4. The lower central series

Given a group GGG and a natural number kkk, this defines a subgroup of GGG, written γk\gamma_kγk​ below. It is the lower central series of GGG, computed as the lower central series of the subgroup GGG of itself, with the indexing

γ0  =  G,γk+1  =  [ γk, G ],\gamma_0 \;=\; G, \qquad \gamma_{k+1} \;=\; [\,\gamma_k,\ G\,],γ0​=G,γk+1​=[γk​, G],

where for subgroups H,K≤GH, K \le GH,K≤G the symbol [H,K][H,K][H,K] denotes the subgroup generated by the set of commutators { hkh−1k−1  :  h∈H, k∈K }\{\, hkh^{-1}k^{-1} \;:\; h \in H,\ k \in K \,\}{hkh−1k−1:h∈H, k∈K} (not merely that set of commutators).

Note the indexing: the series starts at 000 with the whole group, so γ1=[G,G]\gamma_1 = [G,G]γ1​=[G,G] is the commutator subgroup, γ2=[[G,G],G]\gamma_2 = [[G,G],G]γ2​=[[G,G],G], and so on. (This is one index lower than the convention in which the whole group is called γ1\gamma_1γ1​.)

5. The kkk-th lower central factor

Given a group GGG and a natural number kkk, this defines a type, which carries a commutative group structure. With γk\gamma_kγk​ as in §4, let

  • Ab(γk)=γk/[γk,γk]\mathrm{Ab}(\gamma_k) = \gamma_k / [\gamma_k,\gamma_k]Ab(γk​)=γk​/[γk​,γk​] be the abelianization of the group γk\gamma_kγk​ (the quotient of γk\gamma_kγk​ by its own commutator subgroup), and
  • πk:γk→Ab(γk)\pi_k : \gamma_k \to \mathrm{Ab}(\gamma_k)πk​:γk​→Ab(γk​) be the canonical projection.

Let Nk≤γkN_k \le \gamma_kNk​≤γk​ be the subgroup of γk\gamma_kγk​ consisting of those x∈γkx \in \gamma_kx∈γk​ with x∈γk+1x \in \gamma_{k+1}x∈γk+1​ — that is, γk+1∩γk\gamma_{k+1} \cap \gamma_kγk+1​∩γk​ regarded as a subgroup of γk\gamma_kγk​. Then the definition is the quotient group

Ab(γk) / πk(Nk),\mathrm{Ab}(\gamma_k) \,\big/\, \pi_k(N_k),Ab(γk​)/πk​(Nk​),

the quotient of the abelianization of γk\gamma_kγk​ by the image under πk\pi_kπk​ of NkN_kNk​. Since Ab(γk)\mathrm{Ab}(\gamma_k)Ab(γk​) is commutative, that image is automatically a normal subgroup and the quotient is a commutative group; no hypothesis is needed for this.

Two literal readings worth spelling out: the object quotiented is the abelianization of γk\gamma_kγk​, not γk\gamma_kγk​ itself; and what is divided out is the image of γk+1∩γk\gamma_{k+1}\cap\gamma_kγk+1​∩γk​ in that abelianization, not γk+1\gamma_{k+1}γk+1​ itself. In particular at k=0k = 0k=0 this is Ab(G)\mathrm{Ab}(G)Ab(G) divided by the image of [G,G]∩G[G,G] \cap G[G,G]∩G in Ab(G)\mathrm{Ab}(G)Ab(G).

6. The rank of the kkk-th lower central factor

Given a group GGG and a natural number kkk, this defines a natural number: the rank, over the ring Z\mathbb{Z}Z, of the abelian group of §5 written additively. Writing that commutative group additively makes it a Z\mathbb{Z}Z-module in the canonical way (with n⋅xn \cdot xn⋅x the nnn-fold sum of xxx), and the value is the natural-number rank of that module in the sense fixed at the top of this document: the supremum of the cardinalities of Z\mathbb{Z}Z-linearly independent subsets, turned into a natural number, and equal to 000 if that supremum is infinite.

Consequences of that convention, present in the definition: a factor group that is entirely torsion (for example a finite group, or the trivial group) has rank 000, and a factor group of infinite rank also has value 000. The two are not distinguished.

7. First growth exponent

Given a group GGG, this defines a natural number:

∑k=0c−1(k+1) rk,\sum_{k=0}^{c-1} (k+1)\, r_k,k=0∑c−1​(k+1)rk​,

where rkr_krk​ is the rank of §6 and ccc is the nilpotency class of GGG. The summation index kkk runs over 0,1,…,c−10, 1, \dots, c-10,1,…,c−1; the value k=ck = ck=c is not included. All arithmetic is in the natural numbers.

The nilpotency class is defined as the least natural number nnn for which the nnn-th term of the upper central series of GGG equals GGG, if GGG is nilpotent; if GGG is not nilpotent it is assigned the junk value 000. Consequently, for a non-nilpotent GGG the sum here is empty and the definition yields 000; the same happens for the trivial group, whose class is 000.

8. Second growth exponent

Given a group GGG, this defines a natural number:

∑k=0c−12k rk,\sum_{k=0}^{c-1} 2^{k}\, r_k,k=0∑c−1​2krk​,

with rkr_krk​ and ccc exactly as in §7: rkr_krk​ the rank of §6, ccc the nilpotency class of GGG with the junk value 000 when GGG is not nilpotent, the index kkk running over 0,1,…,c−10,1,\dots,c-10,1,…,c−1 and k=ck=ck=c excluded, and all arithmetic — including 2k2^k2k — performed in the natural numbers. The k=0k=0k=0 term is 20r0=r02^0 r_0 = r_020r0​=r0​.

This differs from §7 only in the coefficient: 2k2^k2k here in place of k+1k+1k+1 there. The two agree in the first two terms (k=0k = 0k=0 and k=1k = 1k=1) and differ from k=2k = 2k=2 onwards.

Human review
  • Endorsed by Shuze Chen · Sep 19, 2026

  • Endorsed by dbenbenn · Sep 19, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me