Five-colorability of finite combinatorial near-triangulations

Let $D$ be a finite set with decidable equality. A combinatorial map on $D$ consists of permutations $\alpha,\sigma:D\to D$ with $\alpha^2=\mathrm{id}$ and $\alpha(d)\ne d$ for every $d\in D$. Put $\varphi=\sigma\circ\alpha$. Vertices, edges, and faces are respectively the orbits of $\sigma$, $\alpha$, and $\varphi$; write $V,E,F$ for their numbers. For each dart $d$, its tail is $[d]_\sigma$ and its head is $[\alpha(d)]_\sigma$. The associated simple graph has an edge between two distinct vertices precisely when some dart has those unordered endpoints. A face length is the number of darts in its $\varphi$-orbit.

Assume the supplied near-triangulation data have the following properties. The map is connected: every pair of darts can be joined by finitely many steps, each of which either stays in a $\sigma$-orbit or replaces $d$ by $\alpha(d)$. Its integer Euler characteristic is $V-E+F=2$. The map has no loops, meaning $[d]_\sigma\ne[\alpha(d)]_\sigma$ for every dart, and no parallel edges, meaning any two darts with the same unordered vertex endpoints lie in the same $\alpha$-orbit. There is a distinguished face $f_\infty$ with a chosen root and a nonempty cyclic dart list, without repetitions, enumerating exactly that face orbit and advancing by $\varphi$. Its induced tail-vertex list has no repetitions and has length at least three. Every other face has length exactly three. The boundary data also include the following certificate for every pair of distinct vertices $u,v$ in the distinguished boundary list: there are simple vertex lists from $u$ to $v$ and from $v$ to $u$, with all entries on the boundary, together covering the boundary vertices and having disjoint interior vertex lists. Each list has an interior vertex whenever the unordered pair $\{u,v\}$ is not one of the boundary edges. The certificate includes edge lists as part of its path data; the path structure does not independently impose an adjacency relation between those edge lists and consecutive vertices. Then the associated simple graph has a proper coloring with five colors. Equivalently, there exists $c:D/\langle\sigma\rangle\to\{0,1,2,3,4\}$ such that

The input is the specified finite near-triangulation map, including its boundary certificate. Isolated vertices are not separately represented: every vertex is a dart orbit and, under the no-loop hypothesis, is incident to an edge with a distinct other endpoint. The declaration does not quantify over arbitrary planar graphs or provide their augmentation to near-triangulations.