{"id":"palomar/PALOMAR-2026-09-01-000013","url":"https://github.com/Arthur742Ramos/GrushkoNeumannTheorem/tree/ef1f70db49792bb9bdb0c40eeec48168fca53393","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000013-v1.json","repo":"https://github.com/Arthur742Ramos/GrushkoNeumannTheorem","tags":["math.GR","msc:20E07","msc:20F65","msc:05C25","group-theory","free-products","lean","grushko-theorem"],"score":0,"title":"Grushko--Neumann rank additivity for free products","trust":"high","domain":"math.GR","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.GR","summary":"Formalizes the binary Grushko--Neumann theorem: the minimal number of generators of a free product of two finitely generated groups is the sum of the minimal numbers of generators of the factors. The central theorem is proved by a kernel-checked finite labelled-graph reduction. For a minimal null path, the implemented reduction uniformly performs a source unfold, a subsequent safe fold, and an explicit monochromatic-vertex contraction; this gives the strict decrease used by strong induction and the separated-generator lower bound. The repository also retains the finite-core and free-group…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"On the Number of Generators of a Free Product","identifier":"10.1112/jlms/s1-18.1.12","relationship":"formalizes"}]}