GromovGrowthBridge.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Gromov's theorem from Aaron Hill's formalization

Aaron Hill's FormalConjecturesCheck.gromov_forward proves Gromov's polynomial-growth theorem for arbitrary groups. Its list-defined Cayley balls agree with the finite word balls used here, and their polynomial bounds are equivalent without an additional finite-generation or countability hypothesis.

theorem OAI.PolycyclicRecognition.cayleyBall_eq_wordBall line 21
Source documentation
For symmetric generators the two concrete definitions of word ball agree.
```
theorem cayleyBall_eq_wordBall (T : Finset J)
    (hT : ∀ t ∈ T, t⁻¹ ∈ T) (n : ℕ) :
    FormalConjecturesCheck.CayleyBall (T : Set J) n = (wordBall T n : Set J) := by
…
```
Mentions: OAI.PolycyclicRecognition.wordBall
theorem OAI.PolycyclicRecognition.growthFunction_eq_card_wordBall line 36
Source documentation
The imported theorem's growth function counts exactly our finite ball.
```
theorem growthFunction_eq_card_wordBall (T : Finset J)
    (hT : ∀ t ∈ T, t⁻¹ ∈ T) (n : ℕ) :
    FormalConjecturesCheck.GrowthFunction (T : Set J) n = (wordBall T n).card := by
…
```
Mentions: OAI.PolycyclicRecognition.wordBall

theorem OAI.PolycyclicRecognition.hasPolynomialGrowth_of_wordBall line 44

Source documentation

The positive real constant in the imported growth convention can absorb both the shift by one and a possibly zero natural constant.

theorem hasPolynomialGrowth_of_wordBall (T : Finset J)
    (hT : ∀ t ∈ T, t⁻¹ ∈ T)
    (hgen : Subgroup.closure (T : Set J) = ⊤)
    (hgrowth : ∃ C b : ℕ, ∀ n, (wordBall T n).card ≤ C * (1 + n) ^ b) :
    FormalConjecturesCheck.HasPolynomialGrowth J := by
…

Mentions: OAI.PolycyclicRecognition.wordBall