Five-coloring connected sphere rotation systems with incident vertices and face length at least three

Let $V,D$ be finite sets with decidable equality, with $D\ne\varnothing$. Let $G$ be a connected simple graph on $V$. Suppose a dart representation consists of maps $t,h:D\to V$ and permutations $\alpha,\sigma$ of $D$ satisfying: $\alpha^2=\mathrm{id}$; $\alpha(d)\ne d$ for every dart; $t(\alpha(d))=h(d)$ and $h(\alpha(d))=t(d)$; each dart joins adjacent vertices of $G$; and for every ordered adjacent pair $(u,v)$ there is exactly one dart $d$ with $t(d)=u$ and $h(d)=v$. Also assume $t(\sigma(d))=t(d)$ and that any two darts with the same tail lie in the same $\sigma$-orbit. These are the fields of PlaneSimpleGraph; connectedness is a required field, not supplied by the name alone.

Put $\varphi=\sigma\circ\alpha$, let $f$ be the number of $\varphi$-orbits, and let $e=|D|/2$ (natural-number division; the fixed-point-free involution pairs the darts). Assume the sphere condition, the incidence condition, and the face-length condition:

The Euler equality is in the integers. The incidence condition excludes isolated vertices; the face-length condition covers every face, including any face subsequently designated as outer. Then there exists a coloring $c:V\to\{0,1,2,3,4\}$ such that

This result supplies the triangulation extension internally, but retains the stated connectedness, nonempty dart set, incidence, sphere, and face-length inputs. It is not a declaration for all abstract planar graphs without those inputs.