Light paths and only paths in 3-connected planar graphs (Fabrici–Jendrol')
A Lean 4 / Mathlib formalization of the two theorems of Fabrici and Jendrol' (1997), for finite simple graphs with the combinatorial planarity (genus-zero rotation systems) of the registered entry Kuratowski's theorem. Theorem 1 (light_path): a 3-connected planar graph that contains a path on k ≥ 1 vertices contains such a path whose vertices all have degree at most 5k. Theorem 2 (only_paths_light): for every connected planar graph H that is not a path (not isomorphic to pathGraph on its vertex count) and every m, there is a 3-connected planar graph containing a copy of H in which every copy…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-02-000013
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-02-000013/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-02-000013/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'