{"id":"palomar/PALOMAR-2026-08-31-000002","url":"https://github.com/Arthur742Ramos/GraphCoveringTheory/tree/be06b655ae6d2cfee8fee8033b2ff0f5a4f99bf5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000002-v1.json","repo":"https://github.com/Arthur742Ramos/GraphCoveringTheory","tags":["math.GR","math.AT","math.LO","msc:20E07","msc:05C25","msc:18B40","group-theory","free-groups","lean-formalization","covering-theory"],"score":0,"title":"Arthur742Ramos/GraphCoveringTheory","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 a finite-index subgroup of a free group on a finite nonempty generating type. For a finite nonempty type alpha, a subgroup H of FreeGroup alpha with finite index d is proved equivalent, as a group, to FreeGroup (Fin (1 + d * (card alpha - 1))). More strongly, the repository exposes a FreeGroupBasis for H with this indexing type. The proof realizes H as the vertex group of the finite action-groupoid covering on the coset space, verifies the covering locally by explicit star and costar bijections, and counts the complement of a geodesic spanning…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"Mathlib GroupTheory.FreeGroup.NielsenSchreier","identifier":"","relationship":"adapts"},{"title":"Mathlib Combinatorics.Quiver.Covering","identifier":"","relationship":"adapts"},{"title":"Mathlib Combinatorics.Quiver.Arborescence","identifier":"","relationship":"adapts"}]}