PolynomialGrowth.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The polynomial-growth branch of recognition

Gromov's polynomial-growth implication gives virtual nilpotence, and finite generation converts virtual nilpotence to virtual polycyclicity.

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_polynomial_word_growth line 20
Source documentation
Gromov's published input, combined with the proved algebraic step, turns polynomial growth of a finite symmetric generating set into virtual polycyclicity.
```
theorem virtuallyPolycyclic_of_polynomial_word_growth
    (gromov : GromovPolynomialGrowthInput G) (T : Finset G)
    (hsymmetric : ∀ t ∈ T, t⁻¹ ∈ T)
    (hgenerates : Subgroup.closure (T : Set G) = ⊤)
    (hgrowth : ∃ C b : ℕ, ∀ n, (wordBall T n).card ≤ C * (1 + n) ^ b) :
    IsVirtuallyPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.wordBall

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_polynomial_cover line 31

Source documentation

The fully checked polynomial-cover deduction needed in the nilpotent branch.

theorem virtuallyPolycyclic_of_polynomial_cover
    (gromov : GromovPolynomialGrowthInput G) (T : Finset G)
    (hsymmetric : ∀ t ∈ T, t⁻¹ ∈ T)
    (hgenerates : Subgroup.closure (T : Set G) = ⊤)
    (f : G → X) (C b M : ℕ) (centers : ℕ → Finset X)
    (hcenters : ∀ n, (centers n).card ≤ C * (1 + n) ^ b)
    (hcover : ∀ n h, h ∈ wordBall T n → ∃ c ∈ centers n, dist (f h) c ≤ 1)
    (hmultiplicity : ∀ (c : X) (A : Finset G),
      (∀ h ∈ A, dist (f h) c ≤ 1) → A.card ≤ M) :
    IsVirtuallyPolycyclic G := by
…

Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.wordBall