Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 3.2: a finitely generated nilpotent group has polynomial growth between mE1m^{E_1}mE1​ and mE2m^{E_2}mE2​

Open
Wolf.fg_lcsFactor_and_growth_bounds_of_isNilpotent

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

group-growthgroup-theorynilpotent-groupspolycyclic-groupssolvable-groups

Let Γ\GammaΓ be a finitely generated nilpotent group. Each factor Γk/Γk+1\Gamma_k/\Gamma_{k+1}Γk​/Γk+1​ of the lower central series is a finitely generated abelian group; writing nkn_knk​ for the rank of its free part, set E1=∑k(k+1)nkE_1 = \sum_k (k+1)n_kE1​=∑k​(k+1)nk​ and E2=∑k2knkE_2 = \sum_k 2^k n_kE2​=∑k​2knk​, the sums running over the factors of the series. Then for any finite generating set SSS there are constants 0<c1≤c20 < c_1 \le c_20<c1​≤c2​ with c1mE1≤gS(m)≤c2mE2c_1 m^{E_1} \le g_S(m) \le c_2 m^{E_2}c1​mE1​≤gS​(m)≤c2​mE2​ for every m≥1m \ge 1m≥1.

Preamble
import Definitions.Def_Chou_Growth
import Definitions.Def_MilnorWolf_Growth
import Mathlib
Formal statement
namespace Wolf

theorem fg_lcsFactor_and_growth_bounds_of_isNilpotent {Γ : Type*} [Group Γ] [Group.FG Γ]
    [Group.IsNilpotent Γ] (S : Finset Γ) (hS : Subgroup.closure (S : Set Γ) = ⊤) :
    (∀ k : ℕ, Group.FG (MilnorWolf.lcsFactor Γ k)) ∧
      ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ c₁ ≤ c₂ ∧ ∀ m : ℕ, 1 ≤ m →
        c₁ * (m : ℝ) ^ (MilnorWolf.growthExponentOne Γ) ≤ (MilnorWolf.growthFunction S m : ℝ) ∧
          (MilnorWolf.growthFunction S m : ℝ) ≤
            c₂ * (m : ℝ) ^ (MilnorWolf.growthExponentTwo Γ) := by
  sorry

end Wolf
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, Theorem 3.2, p. 426, with the growth exponents of (3.3)
Read-back

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

Read-back: fg_lcsFactor_and_growth_bounds_of_isNilpotent

The objects the statement is built from

Throughout, Γ\GammaΓ is a group. Three constructions have to be spelled out before the assertion can be stated; each is expanded here exactly as the formal text defines it.

Commutators and the lower central series. For elements, [p,q]:=p q p−1q−1[p,q] := p\,q\,p^{-1}q^{-1}[p,q]:=pqp−1q−1. For two subgroups H,K≤ΓH,K \le \GammaH,K≤Γ, [H,K][H,K][H,K] denotes the subgroup generated by the set { [p,q]:p∈H, q∈K }\{\,[p,q] : p \in H,\ q \in K\,\}{[p,q]:p∈H, q∈K} (not that set itself). The series used here is indexed from 000 and starts at the whole group:

Γ0=Γ,Γk+1=[Γk,Γ].\Gamma_0 = \Gamma, \qquad \Gamma_{k+1} = [\Gamma_k, \Gamma].Γ0​=Γ,Γk+1​=[Γk​,Γ].

So Γ1\Gamma_1Γ1​ is the commutator subgroup [Γ,Γ][\Gamma,\Gamma][Γ,Γ]. These subgroups are nested decreasingly, Γk+1≤Γk\Gamma_{k+1} \le \Gamma_kΓk+1​≤Γk​.

The kkk-th factor group. For each natural number kkk, write Γkab\Gamma_k^{\mathrm{ab}}Γkab​ for the abelianization of Γk\Gamma_kΓk​, i.e. the quotient of Γk\Gamma_kΓk​ by the subgroup generated by all commutators [a,b][a,b][a,b] with a,b∈Γka,b \in \Gamma_ka,b∈Γk​, and write πk:Γk→Γkab\pi_k : \Gamma_k \to \Gamma_k^{\mathrm{ab}}πk​:Γk​→Γkab​ for the canonical projection. The object of interest is

Qk:=Γkab/πk ⁣(Γk+1∩Γk).Q_k := \Gamma_k^{\mathrm{ab}} \big/ \pi_k\!\left(\Gamma_{k+1} \cap \Gamma_k\right).Qk​:=Γkab​/πk​(Γk+1​∩Γk​).

Two points of literal detail. First, the subgroup being divided out is described in the formal text as "Γk+1\Gamma_{k+1}Γk+1​ viewed inside Γk\Gamma_kΓk​", which by definition is the intersection Γk+1∩Γk\Gamma_{k+1}\cap\Gamma_kΓk+1​∩Γk​ regarded as a subgroup of Γk\Gamma_kΓk​; because the series is decreasing this intersection is Γk+1\Gamma_{k+1}Γk+1​ itself, so QkQ_kQk​ is Γkab\Gamma_k^{\mathrm{ab}}Γkab​ modulo the image of Γk+1\Gamma_{k+1}Γk+1​. Second, the quotient is formed as a group quotient, which is legitimate for every subgroup here because Γkab\Gamma_k^{\mathrm{ab}}Γkab​ is abelian and hence all of its subgroups are normal. QkQ_kQk​ is again an abelian group.

At k=0k=0k=0 this reads: the abelianization of Γ\GammaΓ modulo the image of [Γ,Γ][\Gamma,\Gamma][Γ,Γ].

Rank of the kkk-th factor. Let AkA_kAk​ be the abelian group QkQ_kQk​ written additively, viewed as a Z\mathbb{Z}Z-module in the only way possible (the module structure coming from the additive group structure). Put

rk:=rank⁡ZAk,r_k := \operatorname{rank}_{\mathbb{Z}} A_k,rk​:=rankZ​Ak​,

where this rank is defined as follows: take the supremum of the cardinalities of all Z\mathbb{Z}Z-linearly independent subsets of AkA_kAk​, and convert it to a natural number, with the convention that the value is 000 if that supremum is infinite. In particular rk=0r_k = 0rk​=0 both when AkA_kAk​ has infinite rank and when AkA_kAk​ is a torsion group (over Z\mathbb{Z}Z, rank 000 is equivalent to being torsion). For a finitely generated abelian group this rkr_krk​ is the ordinary torsion-free rank, i.e. the number of infinite cyclic summands. Nothing in the definition of rkr_krk​ presupposes that QkQ_kQk​ is finitely generated.

Nilpotency class. Let Z0=1Z_0 = 1Z0​=1 and Zn+1={x∈Γ:[x,y]∈Zn for all y∈Γ}Z_{n+1} = \{x \in \Gamma : [x,y] \in Z_n \text{ for all } y \in \Gamma\}Zn+1​={x∈Γ:[x,y]∈Zn​ for all y∈Γ} be the upper central series, and let ccc be the least nnn with Zn=ΓZ_n = \GammaZn​=Γ (equivalently, the least nnn with Γn=1\Gamma_n = 1Γn​=1); by convention c=0c = 0c=0 if no such nnn exists, though under the hypotheses below one does. Define two natural numbers

d1:=∑k=0c−1(k+1) rk,d2:=∑k=0c−12k rk,d_1 := \sum_{k=0}^{c-1} (k+1)\, r_k, \qquad\qquad d_2 := \sum_{k=0}^{c-1} 2^{k}\, r_k,d1​:=k=0∑c−1​(k+1)rk​,d2​:=k=0∑c−1​2krk​,

both sums being over the ccc indices k=0,1,…,c−1k = 0, 1, \dots, c-1k=0,1,…,c−1 (empty, hence 000, when c=0c=0c=0).

Growth function. For a finite subset S⊆ΓS \subseteq \GammaS⊆Γ and a natural number mmm, let

βS(m):=#{ g∈Γ  |  there is a finite list (x1,…,xℓ) of elements of Γ with ℓ≤m,with xi∈S or xi−1∈S for each i, and x1x2⋯xℓ=g}.\beta_S(m) := \#\left\{\, g \in \Gamma \;\middle|\; \begin{array}{l}\text{there is a finite list } (x_1,\dots,x_\ell) \text{ of elements of } \Gamma \text{ with } \ell \le m,\\ \text{with } x_i \in S \text{ or } x_i^{-1} \in S \text{ for each } i, \text{ and } x_1x_2\cdots x_\ell = g\end{array} \right\}.βS​(m):=#{g∈Γ​there is a finite list (x1​,…,xℓ​) of elements of Γ with ℓ≤m,with xi​∈S or xi−1​∈S for each i, and x1​x2​⋯xℓ​=g​}.

The product of the empty list is the identity, so the identity always belongs to this set, and βS(m)≥1\beta_S(m) \ge 1βS​(m)≥1 for every mmm including m=0m=0m=0. The condition is ℓ≤m\ell \le mℓ≤m, not ℓ=m\ell = mℓ=m, so this is a closed ball of radius mmm and the sets increase with mmm. The generators are used together with their inverses (xi∈S∪S−1x_i \in S \cup S^{-1}xi​∈S∪S−1), and repetitions in the list are allowed. The counting is by a cardinality function that returns 000 for an infinite set; that convention is not triggered here, since the set is finite whenever SSS is finite.

What the theorem asserts

Let Γ\GammaΓ be any group (in any universe) which is

  • finitely generated — some finite subset of Γ\GammaΓ generates Γ\GammaΓ; and
  • nilpotent — some term of its upper central series is all of Γ\GammaΓ.

Let SSS be a finite subset of Γ\GammaΓ and assume

  • the subgroup generated by SSS (the smallest subgroup of Γ\GammaΓ containing SSS) is all of Γ\GammaΓ.

(The last assumption already exhibits a finite generating set, so the finite-generation assumption is separately listed but not independent of it. Both are present.)

Then both of the following hold.

(A) For every natural number kkk, the group QkQ_kQk​ is finitely generated, i.e. some finite subset of QkQ_kQk​ generates it. This is asserted for all k∈Nk \in \mathbb{N}k∈N without restriction — including k=0k = 0k=0 and including every kkk beyond the nilpotency class, where Γk\Gamma_kΓk​ is trivial and so is QkQ_kQk​.

(B) There exist real numbers c1c_1c1​ and c2c_2c2​ such that

0<c1,c1≤c2,0 < c_1, \qquad c_1 \le c_2,0<c1​,c1​≤c2​,

and such that for every natural number mmm with m≥1m \ge 1m≥1, both inequalities

c1 m d1  ≤  βS(m)andβS(m)  ≤  c2 m d2c_1 \, m^{\,d_1} \;\le\; \beta_S(m) \qquad\text{and}\qquad \beta_S(m) \;\le\; c_2 \, m^{\,d_2}c1​md1​≤βS​(m)andβS​(m)≤c2​md2​

hold, where βS(m)\beta_S(m)βS​(m) is read as a real number, mmm is the natural number mmm read as a real number, and the powers are ordinary integer powers of a real number with exponents the natural numbers d1d_1d1​ and d2d_2d2​ defined above (so m0=1m^0 = 1m0=1).

Precision notes on (B)

  • The two constants are quantified before mmm: a single pair (c1,c2)(c_1,c_2)(c1​,c2​) must work for all m≥1m \ge 1m≥1 simultaneously. They may depend on Γ\GammaΓ and on SSS.
  • m=0m = 0m=0 is excluded from the inequalities; nothing is claimed there.
  • The inequalities are non-strict (≤\le≤) in both directions. The strict inequality in the statement is only 0<c10 < c_10<c1​; there is no requirement that c2c_2c2​ be strictly positive beyond what c1≤c2c_1 \le c_2c1​≤c2​ and 0<c10 < c_10<c1​ give, and no upper bound on c2c_2c2​.
  • The lower bound uses the exponent d1d_1d1​ and the upper bound uses the exponent d2d_2d2​. The statement asserts no relation between d1d_1d1​ and d2d_2d2​ — not that they are equal, and not that d1≤d2d_1 \le d_2d1​≤d2​.
  • The existence claim is plain existence, not uniqueness, and the exponents d1,d2d_1, d_2d1​,d2​ are fixed quantities determined by Γ\GammaΓ, not existentially quantified.
  • The growth function is taken with respect to the given generating set SSS; no claim is made about other generating sets.
  • Degenerate case: if Γ\GammaΓ is trivial then c=0c = 0c=0, so d1=d2=0d_1 = d_2 = 0d1​=d2​=0 (empty sums) and βS(m)=1\beta_S(m) = 1βS​(m)=1 for all mmm; the assertion reduces to the existence of 0<c1≤c20 < c_1 \le c_20<c1​≤c2​ with c1≤1≤c2c_1 \le 1 \le c_2c1​≤1≤c2​.
  • Degenerate case: if every rkr_krk​ with k<ck < ck<c is 000 (for instance if all the factors QkQ_kQk​ are finite), then again d1=d2=0d_1 = d_2 = 0d1​=d2​=0 and the assertion reduces to a two-sided bound of βS(m)\beta_S(m)βS​(m) by constants for all m≥1m \ge 1m≥1.
  • SSS is allowed to be empty, but then the generation hypothesis forces Γ\GammaΓ to be trivial; the hypotheses are not vacuous — the trivial group satisfies all of them.
  • (A) and (B) are joined by "and": the theorem asserts the conjunction, so both parts are claimed under the same hypotheses.
Human review
  • Endorsed by Shuze Chen · Sep 22, 2026

  • Endorsed by dbenbenn · Sep 22, 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