{"id":"palomar/PALOMAR-2026-11-01-000025","url":"https://github.com/jtraverso/lebesgue-light-stars/tree/76c43b645dc6dbf14dbf6d5151fac448a1c34835","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000025-v1.json","repo":"https://github.com/jtraverso/lebesgue-light-stars","tags":["math.CO","msc:05C10","msc:05C07"],"score":0,"title":"Light stars and paths in planar graphs of minimum degree five (Jendrol'–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 Theorems 1, 2 and 3 of Jendrol' and Madaras (1996), for finite simple graphs with the combinatorial planarity (genus-zero rotation systems) of the registered entry Kuratowski's theorem. Every planar graph of minimum degree at least five has: a vertex X of degree five with three distinct neighbours A1, A2, A3 such that deg A1 = 5, deg A2 ≤ 6 and deg A3 ≤ 7, or deg A1 = deg A2 = deg A3 = 6 (light_star, Theorem 1; in particular a 5-vertex with three neighbours of degree at most seven, \"Lebesgue's star\"); a vertex of degree five with four distinct neighbours…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"On light subgraphs in plane graphs of minimum degree five","identifier":"doi:10.7151/dmgt.1035","relationship":"formalizes"}]}