Lemma 3.5: polynomial growth bounds do not depend on the generating set
ProvedWolf.exists_const_polynomial_bounds_of_generatingLet and be finite generating sets for the same group . If there are constants and natural numbers with for every , then there are constants with for every .
import Definitions.Def_Chou_Growth import Definitions.Def_MilnorWolf_Growth import Mathlib
namespace Wolf
theorem exists_const_polynomial_bounds_of_generating {Γ : Type*} [Group Γ] (S T : Finset Γ)
(hS : Subgroup.closure (S : Set Γ) = ⊤) (hT : Subgroup.closure (T : Set Γ) = ⊤)
(b₁ b₂ : ℝ) (hb₁ : 0 < b₁) (hb : b₁ ≤ b₂) (p q : ℕ) (hpq : p ≤ q)
(hbounds : ∀ m : ℕ, 1 ≤ m →
b₁ * (m : ℝ) ^ p ≤ (MilnorWolf.growthFunction T m : ℝ) ∧ (MilnorWolf.growthFunction T m : ℝ) ≤ b₂ * (m : ℝ) ^ q) :
∃ c₁ c₂ : ℝ, 0 < c₁ ∧ c₁ ≤ c₂ ∧ ∀ m : ℕ, 1 ≤ m →
c₁ * (m : ℝ) ^ p ≤ (MilnorWolf.growthFunction S m : ℝ) ∧
(MilnorWolf.growthFunction S m : ℝ) ≤ c₂ * (m : ℝ) ^ q := by
sorry
end Wolf
Read-back
What the Lean code literally says, in plain math · claude-opus-5
Read-back: exists_const_polynomial_bounds_of_generating
The vocabulary the statement uses, written out
Two auxiliary notions occur in the statement. Neither is standard, so both are unfolded here in full; after this section they are used only through the descriptions given.
Balls of words. Let be a group, let be a subset, and let . The word ball is the set of all for which there exists a finite list of elements of such that
- its length satisfies (so lists shorter than , and the empty list, are allowed);
- every entry satisfies or — that is, every letter is drawn from the symmetrised alphabet ; and
- the product of the entries, taken in the order in which they are listed, equals :
The product is the group product in list order, left factor first; since no commutativity is assumed anywhere, this order is part of the definition. The empty list is permitted and its product is the identity, so for every , including . Letters may repeat, and the same element may be reachable by many lists. So is the closed ball of radius around the identity in the word metric determined by the symmetrised alphabet .
The growth function. For a finite subset and , write
the number of elements of the word ball of radius . The cardinality here is the natural-number-valued cardinality, which is defined for every set and returns when the set is infinite. That degenerate branch is never reached in this statement: because is finite, the alphabet is finite, there are only finitely many lists of length at most over it, and is the image of that finite collection of lists under the product map. Hence is an honest count, and for all , since the identity always lies in the ball.
Generation. "The subgroup generated by is all of " means: the smallest subgroup of containing is itself. Equivalently, every element of is a product of finitely many elements of and inverses of elements of — no bound on the number of factors. Note that this is subgroup generation, so inverses are available for free.
What the statement asserts
Fix the following data.
- A type — arbitrary, in an arbitrary universe — carrying a group structure. Nothing further is assumed of : it is not assumed abelian, nilpotent, solvable, finite, or torsion-free, and it may be finite or infinite. (Finite generation is not assumed either, but it follows from hypothesis 3 below.)
- Two finite subsets . They are given as finite sets, with no multiplicities, and no relation between them is assumed: they may coincide, overlap, or be disjoint, and either may be empty.
- The subgroup generated by is all of .
- The subgroup generated by is all of .
- Two real numbers .
- .
- (hence also ).
- Two natural numbers .
- .
- For every natural number with , both of the following inequalities hold, as inequalities between real numbers (the integer count and the integer are each read as real numbers in the usual way, and the exponent is a natural number, so ):
Nothing is assumed at $m = 0$.
Under these assumptions the statement asserts:
There exist real numbers and such that
and such that for every natural number with ,
Fine print
The quantifier order. The two constants are chosen once and then serve all : the universal quantifier over sits inside the existential over . The constants may depend on everything fixed beforehand — on , on , on , on , on , and on the hypotheses themselves.
Existence, not uniqueness. Mere existence of such a pair is asserted, not uniqueness, and no formula, bound, or method for producing from the given data is asserted. In particular nothing is claimed about the size of or relative to or : the conclusion does not say one may take , or , or that and are bounded in terms of and the two alphabets in any stated way.
The exponents are unchanged. The exponents in the conclusion are the same natural numbers and as in the hypothesis. The statement transfers the two-sided polynomial bound from the alphabet to the alphabet keeping both exponents, changing only the two constants. The hypothesis concerns only and the conclusion concerns only.
The direction of each inequality. The lower bounds are and , non-strict, with the multiple of the power on the small side; the upper bounds are and , non-strict, with the multiple of the power on the large side. The positivity condition on the first constant is strict (, and in the conclusion), while the comparison between the two constants is non-strict (, and in the conclusion). Likewise is non-strict, so is permitted, in which case hypothesis and conclusion each pin the growth function between two constant multiples of the same power.
The range of . Both the hypothesis and the conclusion quantify over natural numbers and say nothing whatsoever about . This matters, because at the ball is , so , while is for and for ; the excluded case is exactly where the upper bound would fail for .
Degenerate exponents. is permitted, and then and the lower bounds read and . Likewise is permitted, which combined with forces ; the hypothesis then says the growth function of is bounded between the two constants and for all , and the conclusion says the growth function of is bounded between two constants as well.
Empty alphabets. Either or may be empty as a finite set. The subgroup generated by the empty set is the trivial subgroup, so the generation hypothesis then forces to be the trivial group; in that situation every ball is and both growth functions are identically , and the hypothesis at large additionally forces . This is a constrained but not contradictory corner of the statement.
The hypotheses are satisfiable. No hypothesis is vacuous or impossible. For instance, taking and : the ball of radius is , so , and the choices , , satisfy for all , with generating as a group. So the implication has non-trivial instances; conversely the hypothesis is a real restriction, since it requires to have a finite generating set whose growth function is bounded above by a constant multiple of .
Nothing about limits or rates. The statement is purely a pair of inequalities holding for all . It does not mention limits, asymptotic equivalence, growth types up to quasi-isometry, or any comparison of growth functions of two different alphabets pointwise — in particular it does not assert or any such change-of-alphabet inequality, only the existence of the two constants described above.
Confirmed by the mission captain (proposal self-audit).