{"id":"palomar/PALOMAR-2026-08-31-000016","url":"https://github.com/Arthur742Ramos/KuroshSubgroupTheorem/tree/911707126c8b9bb0c764bf853008fe1053c0aad9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000016-v1.json","repo":"https://github.com/Arthur742Ramos/KuroshSubgroupTheorem","tags":["math.GR","math.AT","math.LO","msc:20E07","msc:05C25","msc:18B40","group-theory","bass-serre-theory","lean-formalization"],"score":0,"title":"Arthur742Ramos/KuroshSubgroupTheorem","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 sharp Schreier index formula for finite-index subgroups of free groups and the Kurosh subgroup theorem for arbitrary subgroups of indexed free products. The Schreier proof realizes a subgroup as the vertex group of a finite action-groupoid covering, while the Kurosh proof constructs the Bass--Serre tree, a locally bijective graph-of-groups cover, and its path-lifting normal form. The Kurosh factor-only statement is a free product of the nontrivial quotient vertex stabilizers and the free group of the quotient graph; each vertex stabilizer is identified with an intersection…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true}