GrowthFunction.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

14 declarations, 0 contain sorry, 0 declared as axioms

Imports (7)

Imported by 1 file

FormalConjecturesForMathlib.lean

def GromovPolynomialGrowth.CayleyBall The CayleyBall is the ball of radius n in the Cayley graph of a group G with generating set S line 37 source
Source documentation
The CayleyBall is the ball of radius n in the Cayley graph of a group G with generating set S.

standard axioms: propext what this means
Statement uses: Group, Set, Nat
Proof uses: Set.ofPred, Exists, List, And, LE.le, List.length, Membership.mem, Or, Inv.inv, Eq, List.prod
13 instances, coercions and auxiliary constants left out.
```
def CayleyBall (S : Set G) (n : ℕ) : Set G :=
…
```
theorem GromovPolynomialGrowth.cayleyBall_zero line 40 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Set, Eq, GromovPolynomialGrowth.CayleyBall, OfNat.ofNat, Nat, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.ofPred, Exists, List, And, LE.le, List.length, Membership.mem, Or, Inv.inv, List.prod, funext, List.nil, forall_congr, False, implies_congr and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma GromovPolynomialGrowth.cayleyBall_finite line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, Set.Finite, Nat, GromovPolynomialGrowth.CayleyBall
Proof uses: Union.union, Set.image, Inv.inv, Set.Finite.union, Eq.mpr, id, Eq, Eq.trans, Set.inv, congrArg, Set.image_congr, Membership.mem, Eq.refl, Set.image_inv_eq_inv, Eq.mp, Set.preimage, Set.Finite.preimage, Function.Injective.injOn, inv_injective, Fin and 34 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def GromovPolynomialGrowth.GrowthFunction The GrowthFunction of a group G with respect to a set S counts the number of group elements that can be reached by words of length at most n in S line 55 source
Source documentation
The GrowthFunction of a group G with respect to a set S counts the number of group elements that can be reached by words of length at most n in S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, Nat
Proof uses: Set.ncard, GromovPolynomialGrowth.CayleyBall
```
noncomputable def GrowthFunction (S : Set G) (n : ℕ) : ℕ :=
…
```
theorem GromovPolynomialGrowth.growthFunction_zero line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, Eq, Nat, GromovPolynomialGrowth.GrowthFunction, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.ncard, GromovPolynomialGrowth.CayleyBall, Singleton.singleton, Set.ofPred, Exists, List, And, LE.le, List.length, Membership.mem, Or, Inv.inv, List.prod, funext, List.nil and 9 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma GromovPolynomialGrowth.one_mem_cayleyBall The identity is always in the Cayley ball line 63 source
Source documentation
The identity is always in the Cayley ball.

standard axioms: Quot.sound, propext what this means
Statement uses: Group, Set, Nat, Membership.mem, GromovPolynomialGrowth.CayleyBall, OfNat.ofNat
Proof uses: id, Exists.intro, List, And, LE.le, List.length, Or, Inv.inv, Eq, List.prod, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congr, congrArg, List.nil, forall_congr, False, implies_congr and 4 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma one_mem_cayleyBall (S : Set G) (n : ℕ) :
    1 ∈ CayleyBall S n := by
…
```
Mentions: GromovPolynomialGrowth.CayleyBall
lemma GromovPolynomialGrowth.cayleyBall_monotone The Cayley ball is monotonic in its radius line 70 source
Source documentation
The Cayley ball is monotonic in its radius.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, Nat, LE.le, GromovPolynomialGrowth.CayleyBall
Proof uses: Eq.mpr, List, List.length, Membership.mem, Or, Inv.inv, Eq, List.prod, Exists, And, id, Eq.trans, Set.ofPred, forall_congr, implies_congr, Eq.refl, Exists.intro, And.intro, le_of_not_gt, LT.lt and 49 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma cayleyBall_monotone (S : Set G) {m n : ℕ} (h : m ≤ n) :
    CayleyBall S m ⊆ CayleyBall S n := by
…
```
Mentions: GromovPolynomialGrowth.CayleyBall
lemma GromovPolynomialGrowth.cayleyBall_mul Closure property: if g ∈ CayleyBall S m and h ∈ CayleyBall S n, then g * h ∈ CayleyBall S (m + n) line 77 source
Source documentation
Closure property: if g ∈ CayleyBall S m and h ∈ CayleyBall S n, then g * h ∈ CayleyBall S (m + n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, Nat, Membership.mem, GromovPolynomialGrowth.CayleyBall, HAdd.hAdd, HMul.hMul
Proof uses: id, List, And, LE.le, List.length, Or, Inv.inv, Eq, List.prod, Exists, Exists.intro, HAppend.hAppend, And.intro, Eq.mpr, congrFun', congrArg, List.length_append, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 55 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma cayleyBall_mul (S : Set G) {g h : G} {m n : ℕ}
    (hg : g ∈ CayleyBall S m) (hh : h ∈ CayleyBall S n) :
    g * h ∈ CayleyBall S (m + n) := by
…
```
Mentions: GromovPolynomialGrowth.CayleyBall
lemma GromovPolynomialGrowth.cayleyBall_inv If g ∈ CayleyBall S n, then g⁻¹ ∈ CayleyBall S n line 93 source
Source documentation
If g ∈ CayleyBall S n, then g⁻¹ ∈ CayleyBall S n.

standard axioms: Quot.sound, propext what this means
Statement uses: Group, Set, Nat, Membership.mem, GromovPolynomialGrowth.CayleyBall, Inv.inv
Proof uses: id, List, And, LE.le, List.length, Or, Eq, List.prod, Exists, Exists.intro, List.map, List.reverse, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, List.map_reverse, List.length_reverse and 10 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma cayleyBall_inv (S : Set G) {g : G} {n : ℕ}
    (hg : g ∈ CayleyBall S n) :
    g⁻¹ ∈ CayleyBall S n := by
…
```
Mentions: GromovPolynomialGrowth.CayleyBall
lemma GromovPolynomialGrowth.mem_cayleyBall_one_of_mem line 107 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Set, Membership.mem, GromovPolynomialGrowth.CayleyBall, OfNat.ofNat, Nat
Proof uses: Exists.intro, List, And, LE.le, List.length, Or, Inv.inv, Eq, List.prod, List.cons, List.nil, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', zero_add, forall_congr, implies_congr_ctx and 8 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma GromovPolynomialGrowth.exists_cayleyBall_mem_of_closure_eq_top line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, Eq, Subgroup, Subgroup.closure, Top.top, Exists, Nat, Membership.mem, GromovPolynomialGrowth.CayleyBall
Proof uses: Subgroup.closure_induction, Exists.intro, OfNat.ofNat, GromovPolynomialGrowth.mem_cayleyBall_one_of_mem, GromovPolynomialGrowth.one_mem_cayleyBall, HMul.hMul, HAdd.hAdd, GromovPolynomialGrowth.cayleyBall_mul, Inv.inv, GromovPolynomialGrowth.cayleyBall_inv, Eq.rec, Subgroup.mem_top, Eq.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem GromovPolynomialGrowth.tendsto_atTop_growthFunction_of_infinite In an infinite group, the growth function with respect to a finite generating set is unbounded line 125 source
Source documentation
In an infinite group, the growth function with respect to a finite generating set is unbounded.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Infinite, Set, Set.Finite, Eq, Subgroup, Subgroup.closure, Top.top, Filter.Tendsto, Nat, GromovPolynomialGrowth.GrowthFunction, Filter.atTop
Proof uses: id, Fintype, GromovPolynomialGrowth.CayleyBall, Set.Finite.fintype, GromovPolynomialGrowth.cayleyBall_finite, Filter.Tendsto.congr, Function.comp, Finset, Finset.card, Set.toFinset, Set.ncard, of_eq_true, Eq.trans, True, forall_congr, congrFun', congrArg, Fintype.card, Set.toFinset_card, Set.fintypeCard_eq_ncard and 35 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem tendsto_atTop_growthFunction_of_infinite [Infinite G] {S : Set G} (hS : S.Finite)
    (h : Subgroup.closure S = ⊤) : atTop.Tendsto (GrowthFunction S) atTop := by
…
```
Mentions: GromovPolynomialGrowth.GrowthFunction
def GromovPolynomialGrowth.HasPolynomialGrowth A group has polynomial growth if there exists a finite generating set whose growth function is bounded above by a polynomial line 142 source
Source documentation
A group has polynomial growth if there exists a finite generating set whose growth function is bounded above by a polynomial.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group
Proof uses: Exists, Set, And, Set.Finite, Eq, Subgroup, Subgroup.closure, Top.top, Real, Nat, GT.gt, OfNat.ofNat, LE.le, GromovPolynomialGrowth.GrowthFunction, HMul.hMul, HPow.hPow
15 instances, coercions and auxiliary constants left out.
```
def HasPolynomialGrowth (G : Type*) [Group G] : Prop :=
…
```
def GromovPolynomialGrowth.HasSuperPolynomialGrowth Documented declaration: HasSuperPolynomialGrowth line 150 source
Source documentation
A group has superpolynomial growth if there exists a finite generating set whose growth function eventually dominates every polynomial in the growth-function preorder, up to linearly rescaling the radius.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group
Proof uses: Exists, Set, And, Set.Finite, Eq, Subgroup, Subgroup.closure, Top.top, Nat, LT.lt, OfNat.ofNat, Filter.Eventually, LE.le, Real, HPow.hPow, GromovPolynomialGrowth.GrowthFunction, HMul.hMul, Filter.atTop
13 instances, coercions and auxiliary constants left out.
```
def HasSuperPolynomialGrowth (G : Type*) [Group G] : Prop :=
…
```