feat: add Golod-Shafarevich inequality eval problem

LeanEval/GroupTheory/GolodShafarevich.lean

@@ -0,0 +1,88 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace GroupTheory
+
+/-!
+# The Golod–Shafarevich inequality
+
+`golod_shafarevich_inequality` is the Golod–Shafarevich inequality for finite
+`p`-groups: for a nontrivial finite `p`-group `Q`,
+
+```
+d(Q) ^ 2 < 4 r(Q),
+```
+
+where `d(Q)` is the generator rank (minimal size of a generating set) and
+`r(Q)` is the relation rank (`𝔽_p`-dimension of `H²(Q; 𝔽_p)`).
+
+References: NSW (Neukirch–Schmidt–Wingberg, *Cohomology of Number Fields*),
+Theorem 3.9.7; Serre, *Galois Cohomology*, Chapter I, Appendix 2, Theorem 1.
+
+This is one of the two external inputs of Logical Intelligence's formalization
+of the disproof of Erdős's unit-distance conjecture
+(<https://github.com/logical-intelligence/erdos-unit-distance>,
+`Hyp_GolodShafarevichInequality`), where it is taken as a hypothesis. It is not
+currently available in Mathlib.
+
+The two helper definitions `generatorRank` and `relationRank` below are trusted
+(they are not holes); they fix the meaning of `d(Q)` and `r(Q)`. A finite
+`p`-group is viewed as a topological group with the discrete topology, so that
+topological generation agrees with ordinary generation and continuous
+cohomology agrees with ordinary group cohomology. These definitions follow
+`ErdosUnitDistance.Defs.ProPGroups`.
+-/
+
+open CategoryTheory
+
+/-- The generator rank `d(G)`: the minimal cardinality of a (topological)
+generating set of `G`. For a finite discrete group this is the ordinary minimal
+number of generators. -/
+noncomputable def generatorRank
+    (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ :=
+  sInf {k : ℕ | ∃ S : Finset G, S.card = k ∧
+    (Subgroup.closure (S : Set G)).topologicalClosure = ⊤}
+
+/-- The trivial `ZMod p`-representation of `G`, as an object of
+`Action (TopModuleCat (ZMod p)) G`. -/
+noncomputable def trivialZModpRep
+    (p : ℕ) (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
+    Action (TopModuleCat (ZMod p)) G :=
+  Action.trivial G (TopModuleCat.of (ZMod p) (ZMod p))
+
+/-- The relation rank `r(G) = dim_{𝔽_p} H²(G; 𝔽_p)`, computed via continuous
+cohomology in degree `2` with trivial `ZMod p` coefficients. -/
+noncomputable def relationRank
+    (p : ℕ) [Fact p.Prime] (G : Type)
+    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ :=
+  Module.finrank (ZMod p)
+    ((continuousCohomology (ZMod p) G 2).obj (trivialZModpRep p G))
+
+/-- **Golod–Shafarevich inequality.**
+
+For every prime `p` and every nontrivial finite `p`-group `Q`,
+
+```
+d(Q) ^ 2 < 4 r(Q),
+```
+
+where `d(Q) = generatorRank Q` is the generator rank and
+`r(Q) = relationRank p Q` is the relation rank `dim_{𝔽_p} H²(Q; 𝔽_p)`.
+
+A finite `p`-group is presented as a topological group with the discrete
+topology (`[DiscreteTopology Q] [Finite Q]`), in which setting both ranks
+agree with their abstract group-theoretic counterparts.
+
+References: NSW, Theorem 3.9.7; Serre, Chapter I, Appendix 2, Theorem 1. -/
+@[eval_problem]
+theorem golod_shafarevich_inequality
+    (p : ℕ) [Fact p.Prime] (Q : Type)
+    [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
+    [DiscreteTopology Q] [Finite Q] :
+    IsPGroup p Q → Nontrivial Q →
+      (generatorRank Q : ℝ) ^ 2 < 4 * (relationRank p Q : ℝ) := by
+  sorry
+
+end GroupTheory
+end LeanEval

manifests/problems/golod_shafarevich_inequality.toml

@@ -0,0 +1,9 @@
+id = "golod_shafarevich_inequality"
+title = "The Golod–Shafarevich inequality"
+test = false
+module = "LeanEval.GroupTheory.GolodShafarevich"
+holes = ["golod_shafarevich_inequality"]
+submitter = "Kim Morrison"
+notes = "For every prime p and every nontrivial finite p-group Q, d(Q)² < 4 r(Q), where d(Q) is the generator rank (minimal size of a generating set) and r(Q) = dim_{𝔽_p} H²(Q; 𝔽_p) is the relation rank. The trusted helpers generatorRank and relationRank (non-holes) fix the meaning of d and r, viewing a finite p-group as a discrete topological group so that topological generation and continuous cohomology agree with their abstract counterparts. This is one of the two external inputs taken as a hypothesis in Logical Intelligence's formalization of the disproof of Erdős's unit-distance conjecture (Hyp_GolodShafarevichInequality). The statement was reviewed for faithfulness against NSW Theorem 3.9.7 and Serre."
+source = "NSW (J. Neukirch, A. Schmidt, K. Wingberg, *Cohomology of Number Fields*, 2nd ed., Grundlehren 323, Springer 2008), Theorem 3.9.7; J.-P. Serre, *Galois Cohomology*, Chapter I, Appendix 2, Theorem 1. Lean hypothesis: https://github.com/logical-intelligence/erdos-unit-distance (Hyp_GolodShafarevichInequality)."
+informal_solution = "The Golod–Shafarevich theorem: a finite p-group with generator rank d and relation rank r, where r is identified with dim_{𝔽_p} H²(Q; 𝔽_p) (equivalently the number of relations in a minimal pro-p presentation), satisfies r > d²/4. Proof via the graded 𝔽_p-algebra of the group: form the completed group algebra 𝔽_p⟦Q⟧, filter by powers of the augmentation ideal, and study the associated graded algebra A = ⊕ 𝔞ⁿ/𝔞ⁿ⁺¹. With d generators and r relations its Hilbert series H_A(t) is bounded below termwise by (1 - dt + rt²)⁻¹; if d² ≥ 4r the quadratic 1 - dt + rt² has a positive real root, forcing the (nonnegative) coefficients to fail to terminate, contradicting finiteness of Q. Hence d² < 4r."