Standalone Lake projects for Mathlib-adjacent experiments (Euler's polyhedron formula via convex polyhedra and combinatorial maps)