A weighted Golod–Shafarevich infinitude criterion

A nonpositive presentation polynomial certifies that an actual pro-p group is infinite.

Relator depths matter because deep relations contribute little to the polynomial, allowing extra conditions to be imposed while preserving infinitude. Countably many added relations also require a limiting argument. Golod and Shafarevich’s 1964 paper established infinite class field towers through generator–relation inequalities; retaining individual depths makes that method useful for constructions with additional splitting conditions.

Mathematical statement

Let $p$ be prime and let $G$ be a profinite group with a displayed finite pro-$p$ presentation on $d$ generators and $r$ relators. For each relator choose a lower Zassenhaus depth $\nu_i$, and assume those depth bounds hold for the displayed presentation. No minimality assumption is required.

If some real $t$ satisfies $0\le t<1$ and $$1-dt+\sum_{i=1}^{r}t^{\nu_i}\le0,$$ then $G$ is infinite. The theorem takes an actual presentation object, not merely numerical values for $d$, $r$, and the depths.

Lean code

`ClassFieldTower.ProP.FiniteProPPresentation.infinite_of_gsPolynomial_nonpos`

Published library source ↗Same source in NYLL ↗

theorem infinite_of_gsPolynomial_nonpos
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ i, P.RelatorZassenhausDepthAtLeast (ν i) i)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1)
    (hpoly : 1 - (d : ℝ) * t + ∑ i : Fin r, t ^ ν i ≤ 0) :
    Infinite G

In-scope Lean context

namespace ClassFieldTower.ProP

open ProCGroups

noncomputable section

universe u

namespace FiniteProPPresentation

variable {p d r : ℕ} [Fact p.Prime]

variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}

variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Full declaration and proof

/-- A nonpositive weighted polynomial forces the target of an actual
finite presentation to be infinite. -/
theorem infinite_of_gsPolynomial_nonpos
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ i, P.RelatorZassenhausDepthAtLeast (ν i) i)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1)
    (hpoly : 1 - (d : ℝ) * t + ∑ i : Fin r, t ^ ν i ≤ 0) :
    Infinite G := by
  by_contra hfinite
  let : Finite G := Finite.of_not_infinite hfinite
  exact (not_lt_of_ge hpoly) (P.finite_gsPolynomial_pos ν hν ht0 ht1)

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

Mathematical statement

Lean code

ClassFieldTower.ProP.FiniteProPPresentation.infinite_of_gsPolynomial_nonpos

References

`ClassFieldTower.ProP.FiniteProPPresentation.infinite_of_gsPolynomial_nonpos`