Proposition 3.6: the growth function of a free abelian group of rank
DisprovedWolf.growthFunction_freeAbelian_eq_and_boundsLet be free abelian of rank , taken as written multiplicatively, and let be a minimal generating set, that is, a generating set no proper subset of which generates. Then for every ; and for any finite generating set there are constants with for every .
import Definitions.Def_Chou_Growth import Definitions.Def_MilnorWolf_Growth import Mathlib
namespace Wolf
theorem growthFunction_freeAbelian_eq_and_bounds (n : ℕ)
(T : Finset (Multiplicative (Fin n → ℤ)))
(hT : Subgroup.closure (T : Set (Multiplicative (Fin n → ℤ))) = ⊤)
(hmin : ∀ T' ⊂ T, Subgroup.closure (T' : Set (Multiplicative (Fin n → ℤ))) ≠ ⊤) :
(∀ m : ℕ, MilnorWolf.growthFunction T m = ∑ l ∈ Finset.range (n + 1), 2 ^ l * n.choose l * m.choose l) ∧
∀ S : Finset (Multiplicative (Fin n → ℤ)),
Subgroup.closure (S : Set (Multiplicative (Fin n → ℤ))) = ⊤ →
∃ c₁ c₂ : ℝ, 0 < c₁ ∧ c₁ ≤ c₂ ∧ ∀ m : ℕ, 1 ≤ m →
c₁ * (m : ℝ) ^ n ≤ (MilnorWolf.growthFunction S m : ℝ) ∧
(MilnorWolf.growthFunction S m : ℝ) ≤ c₂ * (m : ℝ) ^ n := by
sorry
end Wolf
Read-back
What the Lean code literally says, in plain math · claude-opus-5
Read-back: growthFunction_freeAbelian_eq_and_bounds
The group that the statement is about
Fix a natural number (the statement quantifies over all , including ).
The ambient group, call it , has as its underlying set all functions from to — that is, all -tuples of integers. Its group law is written multiplicatively throughout the statement, but it is defined to be componentwise integer addition:
for each coordinate . So is the free abelian group of rank , , with additive notation relabelled as multiplicative notation. Every product, inverse, power and identity appearing below is to be read through this relabelling. When the underlying set has exactly one element (the empty tuple), so is the trivial group.
The word ball and the growth function
For a subset and a natural number , define the word ball
Points of detail that the definition fixes:
- The witnessing datum is a finite list of elements of , so repetitions among the are allowed, and the constraint is on the list's length, namely — a closed ball of radius , not a sphere.
- The condition on each entry is or ; equivalently each lies in . The set is not required to be symmetric, nor to omit the identity.
- The product is the right-nested product , with the empty list () having product . Since for every , the identity therefore belongs to for every , including . (In the group law is commutative and associative, so the nesting and the order of the factors do not affect which elements are obtained.)
- is a set of group elements, not of words; distinct words with the same product are counted once.
For a finite subset of and a natural number , the growth function is
the number of elements of the word ball, returned as a natural number. The counting operation used is the one that is defined for an arbitrary set and, by convention, returns when the set is infinite; so would be the value reported for an infinite ball. (The sets occurring in the statement are all finite.)
Generation and minimality
For a subset , the subgroup generated by is the intersection of all subgroups of containing , i.e. the smallest such subgroup. Saying that this subgroup is the whole group is what " generates " means below.
The assertion
For every natural number , and for every finite subset such that
- generates , and
- (minimality) for every finite set with and , the subgroup generated by is not the whole of ,
both of the following hold.
Part (a) — an exact formula for the minimal generating set
For every natural number — including —
This is an equality of natural numbers; all of the arithmetic on the right-hand side takes place in . The index runs over inclusive (that is, terms). Each summand is the natural number , where is the -th power of in and both binomial coefficients are the total natural-number binomial coefficient, which takes the value whenever its lower index exceeds its upper index. Consequently the term indexed by vanishes as soon as ; in particular for only the term survives and the right-hand side equals .
Part (b) — two-sided polynomial bounds for every generating set
For every finite subset such that generates , there exist real numbers and satisfying
such that for every natural number with ,
Here and are natural numbers regarded as real numbers via the standard embedding, the inequalities are inequalities of real numbers, and is the -th power of the real number with natural-number exponent .
Points of logical precision:
- The quantifier order is: first, then , then . So the constants are allowed to depend on (and on ); nothing asserts a choice of constants uniform over the generating sets .
- The constants are only asserted to exist; no uniqueness, no explicit value, and no optimality is claimed.
- The range excludes ; nothing is asserted about in part (b).
- The chain is (strict at the left end, non-strict between the two constants), and both displayed bounds are non-strict ().
- Part (b) does not mention at all, and does not require to be minimal in the sense of hypothesis 2. It is asserted, however, only under hypotheses 1 and 2 about — those hypotheses are part of the ambient assumptions of the whole conjunction.
Degenerate and edge cases silently included
- . is the trivial group. Hypothesis 1 then holds for every finite , while hypothesis 2 forces : if were , then is a finite proper subset of that nevertheless generates the (trivial) whole group, contradicting hypothesis 2. The sum in part (a) reduces to the single term , whose value is , so part (a) asserts for all . In part (b), , so the assertion becomes with no dependence on .
- in part (a). Included by the universal quantifier; as noted, the right-hand side is then .
- or . Both are admissible finite sets as far as the types go; each is additionally subject to the requirement that it generate . The word ball of the empty set is at every radius.
- Satisfiability of the hypotheses. Hypotheses 1 and 2 are constraints on , and a reader should check they can be met. They can: for each , the set of the standard basis tuples (the tuple with in coordinate and elsewhere, for ) generates , and removing any one of them leaves a set generating a proper subgroup. So neither hypothesis is impossible, and the assertion is not vacuous for any .
- No finiteness or decidability assumptions beyond those recorded above are imposed: the only hypotheses in the statement are the two conditions on , plus the generation condition on inside part (b). In particular no separate assumption of the form " is finitely generated" or " is nonempty" appears.
What the two parts do not jointly claim
Part (a) gives the exact count only for sets satisfying both hypothesis 1 and hypothesis 2; part (b) gives only two-sided bounds with unspecified constants, and gives them for all generating finite sets , minimal or not. No exact formula is claimed for a non-minimal generating set, and no relation between the constants of part (b) and the polynomial of part (a) is asserted.