Light stars and paths in planar graphs of minimum degree five (Jendrol'–Madaras)
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000025
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000025/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000025/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'