{"id":"palomar/PALOMAR-2026-11-01-000033","url":"https://github.com/jtraverso/madaras-light-stars/tree/053a5caff546c2f700025081e5d3e0b7bf873f62","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000033-v1.json","repo":"https://github.com/jtraverso/madaras-light-stars","tags":["math.CO","msc:05C10","msc:05C07"],"score":0,"title":"Light 3-stars in plane graphs of minimum face size five (Madaras)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Theorem 1.1 of Madaras (2004), for finite simple graphs with the combinatorial planarity (genus-zero rotation systems) of the registered entry Kuratowski's theorem. In every plane map of a finite simple graph of minimum degree at least three whose faces all have length at least five, some vertex x of degree three has three distinct neighbours a, b, c with deg a = deg b = 3 and deg c ≤ 4 (light_star3); in particular the star K1,3 is light, with degree sum at most 13. One statement. The proof is a discharging argument on the rotation system with charges deg…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"On the structure of plane graphs of minimum face size 5","identifier":"doi:10.7151/dmgt.1239","relationship":"formalizes"}]}