CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-09 (gpt-6-astra)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finitely generated nilpotent groups have polynomial growth

Statement

Every finitely generated nilpotent group has polynomial growth.

Facts & Assumptions

Given: A finitely generated nilpotent group $G$ .

[L1]

For every finite generating set $S$ , the proved Bass–Guivarc'h bound gives $β_{G, S} (n) \leq C_{S} n^{D (G)}$ for all integers $n \geq 1$ , where $C_{S} > 0$ (The Bass–Guivarc’h growth degree formula). Here $D (G) = \sum_{i} i r_{i}$ is a nonnegative integer, including $D (G) = 0$ for finite groups (Bass–Guivarc’h dimension and nilpotent Hirsch length).

[L2]

Polynomial growth means that $β_{G} ≼ n^{d}$ for some integer $d \geq 0$ (Polynomial, subexponential, exponential, and intermediate growth).

[F1]

The comparison $f ≼ g$ means that some integer $C \geq 1$ satisfies $f (n) \leq C g (C n + C) + C$ for every $n \geq 0$ (Growth comparison and growth type).

Proof

technique · direct

1.1L1F1algebra

Fix a finite generating set $S$ and put $d = D (G)$ . Choose an integer $C \geq \max (1, C_{S})$ . For $n \geq 1$ , [L1] gives $β_{G, S} (n) \leq C_{S} n^{d} \leq C (C n + C)^{d} + C$ . At $n = 0$ , the word ball consists of the identity, so the same inequality holds. Thus $β_{G, S} ≼ n^{d}$ by [F1]; for $d = 0$ use the constant polynomial $1$ .

2.1L2step 1.1∎

Therefore [L2] makes $G$ a group of polynomial growth.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

C. Löh, Geometric Group Theory, Sections 5.1-5.3 (standard reference, not scraped)
C. Drutu and M. Kapovich, Lectures on Geometric Group Theory, Chapter 5 (standard reference, not scraped)