Gap conjecture

Conjecture · gap_conjecture

If a finitely generated group has superpolynomial growth, then with respect to any finite generating set its growth function is at least $e^{\sqrt n}$ in Grigorchuk's preorder on growth functions, where the comparison is witnessed by linearly rescaling the radius.

Formal statement · Lean 4.lean

theorem gap_conjecture :
    ∀ (G : Type) [Group G] (S : Set G), S.Finite → Subgroup.closure S = ⊤ →
      HasSuperPolynomialGrowth G →
      ∃ C : ℕ, 0 < C ∧
        ∀ᶠ n : ℕ in atTop, Real.exp (Real.sqrt (n : ℝ)) ≤
          (GrowthFunction S (C * n) : ℝ) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗