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.
Coordinate boxes and word balls have matching size
Statement
For a fixed mixed lower-central coordinate system of a finitely generated nilpotent group G and fixed finite generating set S, there exist a,b>0 such that for all sufficiently large integers n. For real , . Consequently is between positive multiples of .
Facts & Assumptions
Given: uses all canonical finite residues and the chosen free coordinate bounds; G and S are fixed.
Mixed lower-central coordinates are unique (Finite lower-central coordinate systems with torsion accounted for).
Weighted words collect with coordinate bounds O(R^i), with all earlier coordinates zero in the last term (Weighted collection with finite-order carries).
Last-term elements of intrinsic length O(R^c) have ambient length O(R) (Both bounds for last-term weighted distortion).
Proof
A word of length at most n has layer-i free exponents at most by F2. Choose b>=1 such that for all finitely many i. Then for every such integer exponent is at most in absolute value; its residues are allowed in Q. Thus .
We prove for by induction on class. For G=1 the empty tuple represents only 1. For class one, if is in Q(R), repeating fixed S-words for the u_j costs at most , and the finite residues cost at most . Since this is at most KR.
For class put . The coordinate system truncated before layer c is a mixed coordinate system of G/H: for i<c the subgroup H lies in , so those quotient factors are unchanged. For g in Q(R), its image lies in the quotient box. By induction it has a word of length at most K_0 R in the quotient generators; lift its letters to an S-word w with the same length. The element lies in H. An explicit weighted word for it is the reversed inverse S-word for w followed by the ordered coordinate word for g. In weight i this has at most letters for a fixed lambda: w contributes only O(R) weight-one letters, the free powers contribute O(R^i), and finite residues contribute fixed bounded counts.
Apply F2 to that weighted word. Since h is in H, only last-layer coordinates remain; their free exponents are O(R^c), with bounded residues. The corresponding coordinate generators are a finite generating set of the abelian H, so after increasing K_1. F3 gives . If H is finite its fixed ambient diameter gives the same conclusion. Hence , completing the induction. Taking K>=1 and a=1/K gives whenever a.
By uniqueness, every permitted tuple represents a different element. A free weight-i coordinate has exactly possible values, and a residue coordinate has d possible values, independently. This proves the product formula, including the empty product 1. For , . Thus with and , . Combining the two box inclusions gives positive upper and lower multiples of for all sufficiently large n. If all ranks vanish, Q(R) has the constant size T and the same argument gives degree zero.
Source notes
Druţu–Kapovich, Geometric Group Theory (837-page edition), Proposition 14.25 and Theorem 14.26, pp.510–512; two-sided box inclusion proved by the stated local induction. Revised Proposition 14.25 provides controlled normal forms. The converse inclusion is proved locally by quotient lifting and a compressed central correction; uniqueness, not redundant alphabets, justifies counting.
Depends on
- Finite lower-central coordinate systems with torsion accounted for
- Weighted collection with finite-order carries
- Both bounds for last-term weighted distortion
- Bass–Guivarc’h dimension and nilpotent Hirsch length
- Finite normal quotients preserve ball growth
- Finite normal quotients preserve lower-central ranks
Used by
Dependency tree · two levels
19 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
- Druţu–Kapovich, Geometric Group Theory (837-page edition) (standard reference, not scraped)