{"id":"palomar/PALOMAR-2026-10-23-000007","url":"https://github.com/ispacex/group-dimension/tree/533dc1c66d26de4863983fc303382151a593df3a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000007-v1.json","repo":"https://github.com/ispacex/group-dimension","tags":["math.GR","msc:20F14","msc:20D15","msc:20C05","msc:16S34","group-theory","dimension-subgroups","formalization"],"score":0,"title":"Fifth dimension subgroups: D₅ = γ₅ when G/γ₂ is finite of exponent 3, candidates for a counterexample, and a reduction of Kourovka 20.84","trust":"high","domain":"math.GR","source":"palomar","authors":["Stanislav Vorobev"],"reviews":0,"subject":"math.GR","summary":"Lean 4 / Mathlib formalization accompanying S. Vorobev, \"On the inclusion D_5(G) ⊆ γ_4(G): reductions, the Lie-ring proof, and evidence\" (preprint, 2026; submitted to arXiv math.GR on 2026-10-22). The integral dimension subgroups D_n(G) = {g ∈ G : g − 1 ∈ Δ(G)^n} are defined from the augmentation ideal of Mathlib's integral group ring. Kourovka Problem 20.84 asks whether D_5(G) ⊆ γ_4(G) for every group; it is open and is not claimed here. Unconditional results: D_5(G) = γ_5(G) whenever G/γ_2(G) is finite of exponent 3, and more generally whenever G/γ_2(G) is a finite 3-group whose cubes form…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"On the inclusion D_5(G) ⊆ γ_4(G): reductions, the Lie-ring proof, and evidence","identifier":"https://ispacex.github.io/d5/paper/d5.pdf","relationship":"formalizes"},{"title":"S. A. Jennings, The structure of the group ring of a p-group over a modular field, Trans. Amer. Math. Soc. 50 (1941) 175-185","identifier":"","relationship":"adapts"}]}