Total eight-colorings of maximal planar graphs of maximum degree six

Source abstract

We prove that every finite simple maximal planar graph of maximum degree at most six admits a total eight-coloring. We first show that every proper vertex four-coloring of a subcubic graph extends to a total five-coloring. A curvature inequality for boundary walks then gives a matching decomposition of four-connected triangulations with degrees five and six, extending their prescribed vertex four-colorings to total eight-colorings. In a minimum counterexample, two local boundary colorings force the degree-four vertices to have disjoint neighborhoods. A characterization of the local extension obstructions permits these vertices to be restored simultaneously. The proof uses Hamiltonian-connectedness of four-connected planar graphs and the computer-assisted Four-Color Theorem; it requires no further computation.