Hoang La

Petru Valicov

Computer assisted discharging procedure on planar graphs: application to 2-distance coloring

Using computational techniques we provide a framework for proving results on subclasses of planar graphs via discharging method. The aim of this paper is to apply these techniques to study the 2-distance coloring of planar subcubic graphs. Applying these techniques we show that every subcubic planar graph G of girth at least 8 has 2-distance chromatic number at most 6.

 we are done. Otherwise, since

 we are done.

 and finish by coloring vertices v 4 and v 5 .

 and finish by coloring v ′ 3 , v 2 and v 1 in this order. Therefore, we have

), then we color vertex v 4 with x / ∈ L(v ′ 3 ), color v 5 and v 6 (because theirs lists are different) and finish by coloring v ′ 4 , v 3 , v 1 , v 2 and v ′ 3 in this order. Thus we have

 and finish by coloring

. Now, we look at the two following cases:

. We color v 2 and v 1 last. So, L(v 2 ) ⊂ L(v 3 ). We can thus assume w.l.o.g. that L(v 3 ) = {a, b, c, d, e}.

1 in this order. The same holds for e. So, we must have {d,

3 ), and v 5 , v ′ 4 , v 3 , v 1 in this order. We can finish by coloring v ′ 3 and v ′′ 3 since L(v ′ 3 ) = L(v ′′ 3 ). So, c ∈ L(v ′ 3 ). To summarize the previous observations, we have L(v 1 ) = {a, b}, L(v 2 ) = {a, b, c}, L(v 3 ) = {a, b, c, d, e}, L(v ′ 3 ) = {c, d} and e ∈ L(v ′′ 3 ). We color v ′′ 3 with e. We restrict L(v 3 ) to {c, d}. We color v ′ 3 , v 3 , v 4 , v ′ 4 , v 5 by

The discharging method is a very common tool used for proving coloring results on sparse graphs. At heart, it is a counting argument that guarantees the existence of (easily) colorable structures in a given sparse graph. Such structures are commonly named reducible configurations as they cannot appear in a minimal counterexample to a desired theorem. A typical counting argument in the discharging method consists in translating the global sparseness of the graph into local weights, called charges. For instance, a charge can be the degree of a vertex or the size of a face (when the graph is planar). The goal then is to obtain, through a clever redistribution of these charges, a contradiction by showing that there exists a reducible configuration in a minimal counterexample. This redistribution is done via discharging rules. See the survey of Cranston and West [START_REF] Cranston | An introduction to the discharging method via graph coloring[END_REF] for more detailed explanation.

The limit of this method is achieved when one needs to consider a large amount of case distinctions in a proof. This happens essentially for two main reasons: the coloring of a configuration involves a complicated case analysis, or the set of reducible configurations needed in the proof is (too) large. Hence, using computer assistance seems to be the most natural way to overcome this hurdle. Showing that a configuration is reducible is very dependent on the type of coloring. On the other hand, generating a set of unavoidable configurations is more dependent on the class of graphs. The most famous example of computer assistance in discharging is the proof of the Four Color Theorem [START_REF] Appel | Every planar map is four colorable. part I. discharging[END_REF][START_REF] Appel | Every planar map is four colorable. part II. reducibility[END_REF][START_REF] Robertson | The four-colour theorem[END_REF]. In this paper, we present an algorithm that, given a particular set of discharging rules, generates all to-be-reduced configurations for planar graphs. We implemented this algorithm and applied it to show the 2-distance colorability of a subclass of subcubic planar graphs. The source code can be found at https://gite.lirmm.fr/discharging/planar-graphs.

Before going into the details of 2-distance coloring problems, we wish to highlight that, even though the majority of the paper deals with the technicality of this particular problem, our algorithm is independent from the coloring problem.

A 2-distance k-coloring of a graph G = (V, E) is a map φ : V → {1, 2, . . . , k} such that no pair of vertices at distance at most 2 receives the same color c ∈ {1, 2, . . . , k}. Wegner [START_REF] Wegner | Graphs with given diameter and a coloring problem[END_REF] conjectured that subcubic planar graphs are 7-colorable. This conjecture was proved by two independent group of authors, the first one using a graph decomposition (Thomassen [START_REF] Thomassen | The square of a planar cubic graph is 7-colorable[END_REF]), the second one using a computer-assisted discharging method (Hartke et al. [START_REF] Hartke | The chromatic number of the square of subcubic planar graphs[END_REF]). The authors in [START_REF] Hartke | The chromatic number of the square of subcubic planar graphs[END_REF] used computer assistance to 2-distance color a given set of large configurations. Our approach differs as we use the computer in order to generate the set of configurations needed to be reduced (according to the discharging rules) instead. Moreover, for our specific problem, the reducible configurations are not always colorable by computer with a naive exhaustive precoloring extension algorithm (see discussion after Lemma 10).

The 2-distance colorability of planar graphs with high girth is extensively studied in the literature. See [START_REF] Hoang | 2-distance list (∆ + 2)-coloring of planar graphs with girth at least 10[END_REF] for a detailed state of art. We focus on the case of subcubic graphs. In 2008, Cranston and Kim proved the following result: Theorem 1 ( [START_REF] Cranston | List-coloring the square of a subcubic graph[END_REF]). Let G be a planar subcubic graph with girth g ≥ 9. Then χ 2 (G) ≤ 6.

Note that their result also applies for the list version of the problem. We improve Theorem 1 by lowering the bound on the girth. Our proof relies heavily on the assumption that the colors are taken from the same set of six colors, thus it does not seem to be extendable to the list version of the problem.

Theorem 2. Let G be a planar subcubic graph with girth g ≥ 8. Then χ 2 (G) ≤ 6.

The proof is done by induction on the order of the graph using the discharging method. We will assume a minimum counterexample and show a set of reducible configurations which it cannot contain (Section 2). Then, using Euler's formula, we define a distribution of charges on the vertices and faces of this hypothetical counterexample such that the total amount of charges is negative. In order to obtain a non-negative total amount of charges on the vertices, we use the same distribution of charges on the vertices as in the proof of Theorem 1 (Section 3.1). With this distribution, the only faces with negative charge are of length 8. With the assistance of a computer program, we list each possible close neighbourhoods around a face of length 8. For each of these neighborhoods, our algorithm shows that either it contains a reducible configuration or it can get enough charge from its incident vertices (Section 3.2). This leads to a contradiction.

In Section 4, we discuss the tightness of Theorem 2 and possible extensions. Finally, in Section 5, we explain how to use our algorithm to solve problems on other subclasses of planar graphs.

Notations: In the following, we only consider plane graphs that is planar graphs together with their embedding into the plane. For a plane graph G, we denote V , E, F the sets of vertices, edges and faces respectively. We denote d(v) (resp. d(f )) the degree of vertex v ∈ V (resp. the size of face f ∈ F ). Some more notations:

• A d-vertex is a vertex of degree d.

• A d-face is a face of size d.

• A k-path is a path of length k + 1 where the k internal vertices are 2-vertices.

• A (k 1 , k 2 , k 3 )-vertex is a 3-vertex incident to a k 1 -path, a k 2 -path and a k 3 -path.

Recall that in the whole paper we do a 2-distance 6-coloring. Thus, for a vertex v, we denote L(v) the set of available colors from {a, b, c, d, e, f }. For convenience, in the figures a vertex v will be represented by a circle labeled v. Additionally, when a lower bound on |L(v)| is known, it will be depicted on the figure. For example, the graph depicted in Figure 1i is a path v 1 v 2 v 3 v 4 with the following size of lists of available colors:

|L(v 1 )| ≥ 2, |L(v 2 )| ≥ 3, |L(v 3 )| ≥ 2, |L(v 4 )| ≥ 2.
We will also say that a vertex u sees another vertex v if v is at distance at most 2 from u.

Useful observations and lemmata

Here we show some colorable and non-colorable configurations, that is graphs together with lists of available colors for each vertex. These observations will be extensively used in Section 2.

Lemma 1. The graphs depicted in Figures 1i to 1xv are 2-distance colorable.

Proof. In the proofs of this section, whenever the size of a list |L(v)| ≥ k we assume that |L(v)| = k by arbitrarily removing the extra colors from the list. One can easily observe that these proofs will hold for the case when

|L(v)| > k.
We will give the proofs for each figure in order:

Proof of Figure 1i. If v 1 and v 4 can be colored with the same color, then finish by coloring v 2 , v 3 in this order. Otherwise, since L(v 1 ) ∩ L(v 4 ) = ∅ we have |L(v 1 ) ∪ L(v 4 )| ≥ 4, so one can apply Hall's Theorem.

Proof of Figure 1ii.

If L(v 4 ) = L(v 5
), then color v 5 with x / ∈ L(v 4 ) and get Figure 1i, so we are done. Otherwise, color v 3 with a color y / ∈ L(v 5 ) ∪ L(v 4 ). Then color v 1 , v 2 , v 4 , v 5 , in this order.

Proof of Figure 1iii. If L(v 1 ) = L(v 3 ), then we color v 1 with x / ∈ L(v 3 ) and get Figure 1ii. Otherwise, color v 2 with a color y / ∈ L(v 3 ) ∪ L(v 1 ), then color v 3 , v 4 , v 5 , v 6 using Figure 1i and finish by coloring vertex v 1 .

Proof of Figure 1iv. Observe that L(v 3 ) = L(v 4 ) because if not we color v 4 with x / ∈ L(v 3 ) and we get Figure 1i. Thus color v ′ 3 with y / ∈ L(v 3 ) and get Figure 1i again. Figure 1v. Finally, we finish by coloring v 2 and v 1 in this order.

Proof of Figure 1xi. 1v and finish with v 2 and v 1 . Proof of Figure 1xii. Observe that L(v 1 ) = L(v 2 ) since otherwise one could color v 1 with x / ∈ L(v 2 ) and get Figure 1vi. Therefore, we restrict the list of colors of v 3 to L(v 3 ) \ L(v 2 ). We color then v 3 , v 4 , v ′ 4 , v 5 , v 6 by Figure 1v and finish with v 2 and v 1 .

If L(v 2 ) = L(v 1 ), then color v 2 with x / ∈ L(v 1 ), color vertices v ′ 4 , v 4 , v 5 , v 6 by Figure 1i and finish with v 3 and v 1 . If L(v 2 ) = L(v 1 ), then by restricting the list of colors of v 3 to L(v 3 ) \ L(v 2 ), we color vertices v 3 , v 4 , v ′ 4 , v 5 , v 6 by Figure
Proof of Figure 1xiii. If L(v 5 ) = L(v 6 ), then by coloring v 6 with x / ∈ L(v 5 ), one could finish by Figure 1ii. Thus L(v 5 ) = L(v 6 ) and we restrict the list of colors of v 4 to L(v 4 ) \ L(v 5 ), color vertices v 1 , v 2 , v 3 , v 4 by Figure 1i and finish with v 5 and v 6 .

Proof of Figure 1xiv. Observe that L(v 1 ) = L(v 2 ) as otherwise by coloring v 2 with x / ∈ L(v 1 ), one could color v 3 , v 4 , v 5 , v 6 , v 7 by Figure 1ii and finish by coloring v 1 . Therefore, color v 3 with y / ∈ L(v 2 ) ∪ L(v 1 ), color v 4 , v 5 , v 6 , v 7 by Figure 1i and finish by coloring v 2 , v 1 in this order.

Proof of Figure 1xv. Note that L(v 6 ) = L(v 7 ) as otherwise by coloring v 7 with x / ∈ L(v 6 ) one could finish by Figure 1xiii. Hence color v 5 with y / ∈ L(v 7 ) ∪ L(v 6 ), then color v 1 , v 2 , v 3 , v 4 by Figure 1i and finish with v 6 , v 7 .

Proof of Figure 1xvi. If it is possible to color v 1 and v 5 with the same color, then after coloring v 6 , we get Figure 1x. Hence L(v 1 ) ∩ L(v 5 ) = ∅. If it is possible to color v 5 and v ′ 2 with a common color, then after coloring v 6 , we get again Figure 1x. Hence

L(v ′ 2 ) ∩ L(v 5 ) = ∅. Symmetrically, we have L(v ′′ 3 ) ∩ L(v 5 ) = ∅ and L(v ′′′ 3 ) ∩ L(v 5 ) = ∅.
Now, since we are considering a 6-coloring, we restrict the list of colors of v 3 to L(v 3 ) = L(v 5 ) and color vertices v 3 , v 4 , v ′ 4 , v 5 , v 6 by Figure 1v. We finish by coloring the remaining vertices in the following order:

v 1 , v 2 , v ′ 2 , v ′ 3 , v ′′ 3 , v ′′′ 3 . v 1 v 2 v 3 v 4 2 3 2 2 (i) v 1 v 2 v 3 v 4 v 5 2 3 3 2 2 (ii) v 1 v 2 v 3 v 4 v 5 v 6 2 3 2 3 3 2 (iii) v 1 v 2 v 3 v 4 2 4 2 v ′ 3 3 2 (iv) v 1 v 2 v 3 v 4 2 2 4 v ′ 3 3 2 (v) v 1 v 2 v 3 v 4 v 5 2 2 4 v ′ 3 3 3 2 (vi) v 1 v 2 v v 4 2 4 v ′ 2 3 3 v ′ 3 2 (vii) v 1 v 2 v 3 v 4 v 5 2 4 v ′ 2 3 4 v ′ 3 3 2 2 (viii) v 1 v 2 v 3 v 4 v 5 v 6 2 3 4 v ′ 3 3 4 v ′ 4 3 2 2
(ix)

v 1 v 2 v 3 v v 5 2 3 5 v ′ 3 2 v ′′ 3 2 4 v ′ 3 2 (x) v 1 v 2 v 3 v 4 v 5 v 6 2 2 5 4 v ′ 4 2 2 2 (xi) v 1 v 2 v 3 v 4 v 5 v 6 2 2 4 4 v ′ 4 3 2 2 (xii) v 1 v 2 v 3 v 4 v 5 v 6 2 2 3 4 2 2 (xiii) v 1 v 2 v 3 v 4 v 5 v 6 v 7 2 2 3 3 3 3 2 (xiv) v 1 v 2 v 3 v 4 v 5 v 6 v 7 2 2 4 3 3 2 2 (xv) v 1 v 2 v 3 v 4 v 5 v 6 2 4 6 4 2 2 v ′ 2 3 v ′ 4 3 v ′ 3 4 v ′′ 3 2 v ′′′ 3 3 (xvi) Figure 1: Useful 2-distance colorable configurations (Lemma 1)
In Figures 2 to 5 we provide several useful non-colorable configurations. The important fact is that the non-colorable configurations can force the lists of colors on some vertices.

Lemma 2. The graphs depicted in Figures 2 to 5 are 2-distance colorable unless their lists of available colors are exactly as indicated.

v 1 v 2 v 3 1 2 2 v 1 v 2 v 3 2 1 2 (i) Initial configurations v 1 v 2 v 3 L(v 1 ) ⊆ {a, b} {a, b} {a, b} v 1 v 2 v 3 {a, b} L(v 2 ) ⊆ {a, b} {a, b} (
v 2 v 3 v 4 v 1 2 3 2 3 (i) Initial configuration v 2 v 3 v 4 v 1 L(v 1 ) ⊆ {a, b, c} {a, b, c} L(v 3 ) ⊆ {a, b, c} {a, b, c} (ii) Forced lists of colors Figure 3: A non-colorable graph v 2 v 3 v 4 v 5 v 1 2 3 3 2 2 (i) Initial configuration v 2 v 3 v 4 v 5 v 1 L(v 1 ) ⊆ {a, b, c} {a, b, c} {a, b, c} L(v 4 ) ⊆ {a, b, c} (ii) Forced lists of colors Figure 4: A non-colorable graph v 1 v 2 v 3 v 4 v 5 2 2 4 2 2 (i) Initial configuration v 1 v 2 v 3 v 4 v 5 {a, b} {a, b} {a, b, c, d} {c, d} {c, d} (ii) Forced lists of colors Figure 5: A non-colorable graph Proof of Figure 2. By Hall's Theorem, if |L(v 1 ) ∪ L(v 2 ) ∪ L(v 3 )| ≥ 3, then the graph is 2-distance colorable.
Hence the forced lists in Figure 2ii follow.

Proof of Figure 3. By Hall's Theorem, if We will show that if v 1 , v 2 , v 3 , v 4 are colorable, then the whole configuration is colorable (v 5 included). Thus, they cannot be colored and by Figure 3 (since all four vertices see each other at distance two), we obtain Figure 4ii.

|L(v 1 ) ∪ L(v 2 ) ∪ L(v 3 ) ∪ L(v 4 )| ≥ 4,
So, let us assume that v 1 , v 2 , v 3 , v 4 are colorable, in which case, |L(v 1 ) ∪ L(v 2 ) ∪ L(v 3 ) ∪ L(v 4 )| ≥ 4 and |L(v 5 )| = 2. If L(v 5 ) ⊆ L(v 4 ), then we restrict L(v 3 ) to L(v 3 ) \ L(v 5 ) and observe that |L(v 1 ) ∪ L(v 2 ) ∪ (L(v 3 ) \ L(v 5 )) ∪ L(v 4 )| = |L(v 1 ) ∪ L(v 2 ) ∪ L(v 3 ) ∪ L(v 4 )| ≥ 4 since L(v 5 ) ⊆ L(v 4 ). So, we can color v 1 , v 2 , v 3 , v 4 and finish by coloring v 5 . If L(v 5 ) ⊆ L(v 4 ), then we restrict L(v 4 ) to L(v 4 ) \ L(v 5 ). If |L(v 1 ) ∪ L(v 2 ) ∪ L(v 3 ) ∪ (L(v 4 ) \ L(v 5 ))| ≥ 4, then we can color v 1 , v 2 , v 3 , v 4 and finish with v 5 . Thus, |L(v 1 ) ∪ L(v 2 ) ∪ L(v 3 ) ∪ (L(v 4 ) \ L(v 5 ))| = 3 and we can assume w.l.o.g. that L(v 1 ) ⊆ L(v 2 ) = L(v 3 ) = {a, b, c} and d ∈ L(v 4 ) ∩ L(v 5
). Now, it suffices to color v 4 with d, then color v 5 , v 1 , v 3 , v 2 in this order.

Proof of Figure 5. First, observe that if |L(v 1 )| ≥ 3, then we can color the other vertices by Figure 1i and color v 1 last. If |L(v 2 )| ≥ 3, then we obtain Figure 1ii. Symmetrically, the same holds for L(v 4 ) and

L(v 5 ). If |L(v 3 )| ≥ 5, we can color v 1 , v 2 , v 4 , v 5 , v 3 in this order.
Now, let us try to color the configuration. If L(v 1 ) = L(v 2 ), then color v 1 with a / ∈ L(v 2 ) and get Figure 1i. Therefore we have L(v 1 ) = L(v 2 ) and symmetrically

L(v 4 ) = L(v 5 ). Finally, if L(v 1 ) ∪ L(v 5 ) = L(v 3 ), then one could color v 3 with b / ∈ L(v 1 ) ∪ L(v 5
) and finish by coloring v 1 , v 2 , v 4 , v 5 in this order. Hence the lists in Figure 5ii follow. Lemma 3. If there exists a coloring φ of the configuration from Figure 5i where φ(v 1 ) = φ(v 5 ), then there exists a coloring φ ′ such that φ(v 1 ) = φ ′ (v 1 ) or φ(v 5 ) = φ ′ (v 5 ).

Proof. Suppose that the configuration from Figure 5i is colorable with φ where φ(v 1 ) = a, φ(v 5 ) = b and a = b. Suppose by contradiction that for every coloring φ ′ of Figure 5i, φ ′ (v 1 ) = a and φ ′ (v 5 ) = b.

Let L(v 1 ) = {a, x}. We color v 1 with x. Since there exists no valid coloring φ ′ where φ ′ (v 1 ) = x, the remaining configuration must not be colorable. So x ∈ L(v 2 ), otherwise, we can color v 2 , v 3 , v 4 , v 5 by Figure 1i. Let L(v 2 ) = {x, y}. Moreover, x, y ∈ L(v 3 ). Otherwise, we color v 1 with x, v 2 with y and finish by coloring v 4 , v 5 , v 3 in this order.

Symmetrically, the same holds for v 5 . Let L(v 5 ) = {b, x ′ }, then we must have L(v 4 ) = {x ′ , y ′ } and x ′ , y ′ ∈ L(v 3 ).

Observe that when we color v 1 with x and v 2 with y, the remaining configuration is not colorable so by Figure 2, we must have L(v 3 ) = {x, y, b, x ′ }. Symmetrically, if instead we color v 5 with x ′ and v 4 with y ′ , then we must have L(v 3 ) = {x ′ , y ′ , a, x}. We conclude that {x, x ′ , b, y} = {x, x ′ , a, y ′ }. In other words, a = y and b = y ′ . Thus, we have L(v 1 ) = L(v 2 ) = {a, x}, L(v 4 ) = L(v 5 ) = {b, x ′ } and L(v 3 ) = {a, x, b, x ′ }. By Figure 2, we know that this configuration is not colorable, which is a contradiction as there exists a valid coloring φ.

Structural properties of a minimal counterexample

Let G be a counterexample to Theorem 2 with the minimum number of vertices. We show some properties of G.

Lemma 4. Graph G is connected.
Proof. If G is not connected, then we consider one of its connected component that is not 2-distance colorable (which exists since G is a counterexample to Theorem 2). This component is also a planar subcubic graph with girth at least 8 that is a counterexample to Theorem 2, which contradicts G's minimality. Proof. If G has a 0-vertex, since G is connected, it is a single vertex which is colorable. Assume by contradiction that G has a 1-vertex v. We remove such vertex and 2-distance color the resulting graph which is possible due to the minimality of G. Then, we add the vertex back then choose a color for v different from all of its 2-distance neighbors' as v has at most 3 neighbors at distance 2 and we have 6 colors.

By Lemma 4 and Lemma 5, the graph G has only 2-vertices and 3-vertices. Lemma 6. Graph G has no k-path with k ≥ 2.

Proof. Assume by contradiction that G has a k-path with k ≥ 2. We remove the 2-vertices of this path and color the resulting graph. One can easily see that such coloring is greedily extendable to the removed 2-vertices.

In what follows we show a set of subgraphs of G that are reducible, that is none of these subgraphs can appear in G as otherwise it would contradict the choice of G. All these configurations are depicted in Figure 6, Figure 8 and Figure 24. In order to simplify the reading of the paper, the captions of the corresponding configurations of these figures will be explained later in Section 3.2 as they are not used in this section. In each of the sub-figures, we define S as the set of all vertices labeled v i , v ′ i , v ′′ i or v ′′′ i , where i is a positive integer. The degree of these vertices are given by their incident edges. In order to prove the reducibility of S we consider a 2-distance coloring φ of G -S (by induction hypothesis) and show how to extend φ to G leading to a contradiction. In each figure, the number drawn next to a vertex of S in the figure corresponds to the number of available colors in the precoloring extension of G -S.

Since G has girth g ≥ 8, one can easily observe that G[S] 2 = G 2 [S] for each configuration in Figure 6. In other words, there are no extra conflicts between vertices in S than the conflicts in G[S]. Unlike the configurations of Figure 6, in those of Figure 8, some pair of vertices may see each other in G while they are at distance at least 3 in the subgraph induced by S, that is sometimes

G[S] 2 = G 2 [S].
Lemma 7. Graph G does not contain the configurations depicted in Figure 6.

Proof. We will give the proofs for each figure in order: Proof of Figure 6i Lemma 8. Graph G does not contain the configurations depicted in Figure 7.

v 1 , v 2 , v 3 , v ′ 2 , v ′′ 2 , v ′′′ 2 by
1 v 2 v 3 v 4 v 5 3 4 5 2 2 v ′ 2 3 (i) 1c1a1, 1c1c v 1 v 2 v 3 v 4 v 5 3 4 4 v ′ 3 3 2 2 v ′ 2 3 (ii) 1c0c0a1, 1c0c0c, 1a0b1, 1b0c v 1 v 2 v 3 v 4 3 4 4 v ′ 3 3 3 v ′ 2 3 (iii) 1c0c1, 1b1 v 1 v 2 v 3 v 4 v 5 v 6 2 2 4 3 3 3 v ′ 5 3 (iv) 1a1a0c1, c1a0c1, 1a1b, c1b v 1 v 2 v 3 v 4 v 5 v 6 2 2 5 4 2 2 v ′ 4 3 (v) 1a1c0a1, c1c0a1, 1a1c0c, c1c0c v 1 v 2 v 3 v 4 v 5 3 5 5 2 2 v ′ 2 4 v ′′ 2 3 v ′′′ 2 3 v ′ 3 4 v ′′ 3 3 v ′′′ 3 3 (vi) 1b0b0a1, 1b0b0c, 1c0c0b0a1, 1c0c0b0c v 1 v 2 v 3 v 4 v 5 3 4 6 4 3 v ′ 2 3 v ′ 4 3 v ′ 3 4 v ′′ 3 3 v ′′′ 3 3 (vii) 1c0b0c1 v 1 v 2 v 3 v 4 v 5 v 6 3 4 6 4 2 2 v ′ 2 3 v ′ 4 3 v ′ 3 4 v ′′ 3 3 v ′′′ 3 3 (viii) 1c0b0c0a1, 1c0b0c0c
Proof. Proof of Figure 7i. Here, we redefine

S = {v 0 , v 1 , v 2 , v 3 , v 4 }. By Figure 5, L(v 0 ) = L(v 1 ) = {a, b}, L(v 3 ) = L(v 4 ) = {c, d} and L(v 2 ) = {a, b, c, d}.
Therefore, we can assume w.l.o.g that v 6 is colored e. Since |L(v 0 )| = 2, all of the colored vertices that v 0 sees must be colored differently. The same holds for v 4 . However, it means that v 2 does not see the color e, which is impossible since

L(v 2 ) = {a, b, c, d}. Proof of Figure 7ii. Note that G[S] 2 = G 2 [S]
. We first prove three important observations.

• L(v 7 ) = L(v ′ 6 ). Suppose the contrary and color v 7 , v 6 , v ′ 6 , v 5 , v ′ 5 , v 4 , v 3 by Figure 1viii. Now if v 0 , v 1
and v 2 are colorable, then we are done. Thus according to Figure 2, we can assume that

L(v 1 ) ⊂ L(v 0 ) = L(v 2 ).
But then since by our assumption L(v 7 ) = L(v ′ 6 ), we permute the colors of v ′ 6 and v 7 so that L(v 0 ) = L(v 2 ) and we are done.

• L(v 3 ) ⊂ L(v 2 ) ⊃ L(v 4 ). If not, color v 3 and v 4 such that |L(v 2 )| ≥ 3. Recall that L(v 7 ) = L(v ′ 6 ). Hence we color v ′ 5 , v 5 , v 6 , v ′ 6 , v 7 by Figure 4. We finish by coloring v 1 , v 0 , v 2 in this order. • L(v 1 ) ∩ L(v 4 ) = ∅. By contradiction, suppose a ∈ L(v 1 ) ∩ L(v 4
). We will show the following observations.

-a / ∈ L(v ′ 6 ). If a ∈ L(v ′ 6
), we color v 1 , v 4 and v ′ 6 with a. Then, we color v 3 . After that, we color v ′ 5 , v 5 , v 6 , v 7 by Figure 1i and we finish by coloring v 0 and v 2 in this order.

a ∈ L(v 7 ). If a / ∈ L(v 7 ), we color v 1 and v 4 with a. Then, we color v 3 . After that, we color

v ′ 5 , v 5 , v 6 , v ′ 6 , v 7 by Figure 4 (recall that L(v ′ 6 ) = L(v 7 )
) and finish by coloring v 0 and v 2 in this order.

-a ∈ L(v ′ 5 ). If a / ∈ L(v ′ 5)
, we color v 4 and v 7 with a. Then, we color v 3 . Finally, we finish by coloring

v 1 , v 2 , v 0 , v 6 , v 5 , v ′ 6 , v ′ 5 in this order. -|L(v 3 ) \ {a}| = 1.
Otherwise, we color v 4 and v 7 with a. Then, we color v 5 in such a way that v 3 has at least 2 colors left. After that, we color v ′ 5 , v 5 , v 6 , v 7 in this order. Finally, we finish by coloring v 3 , v 2 , v 1 , v 0 by Figure 1i. Thus, we color v ′ 5 , v 3 and v 7 with a, then we color the remaining vertices in the following order: 1viii and finish by coloring v 0 and v 2 in this order.

v 4 , v 2 , v 1 , v 0 , v 6 , v 5 , v ′ 6 . Since L(v 1 ) ∩ L(v 4 ) = ∅, we assume w.l.o.g. that L(v 4 ) ⊆ {a, b, c} and L(v 1 ) = {d, e, f }. As L(v 3 ) ⊂ L(v 2 ) ⊃ L(v 4 ), there exists a color, say d, in L(v 1 ) such that after coloring v 1 with d, we have |L(v 2 )| ≥ 4 and |L(v 3 )|, |L(v 3 )| ≥ 2. In conclusion, we color v 1 with d, v 7 , v 6 , v ′ 6 , v 5 , v ′ 5, v 4 , v 3 by Figure
Proof of Figure 7iii. If v ′ 2 sees v ′ 6
, then the are at distance exactly 2 and share a common neighbor, say 1vii and finish by coloring v 3 and v ′ 2 in this order. Proof of Figure 7iv. If v ′′ 5 sees v 1 by sharing a common neighbor, say v 8 , then vertices

v 8 . Then vertices v ′ 6 , v 8 , v ′ 2 , v 2 , v 3 , v 4 , v 5 , v 6 correspond to the reducible configuration of Figure 7i. Therefore, we can assume that G[S] 2 = G 2 [S]. Color v 2 with x / ∈ L(v ′ 2 ) and color greedily v 1 . Then color vertices v 4 , v 5 , v ′ 5 , v 6 , v ′ 6 , v 7 , v 0 by Figure
v ′′′ 5 , v ′ 5 , v ′′ 5 , v 8 , v 1 , v 2 , v 0 form the reducible configuration of Figure 6iv. The case when v ′′′ 5 sees v 1 is symmetric. Therefore, we can suppose that G[S] 2 = G 2 [S]. First we show that L(v 1 ) ∩ L(v 7 ) = ∅.
Suppose the contrary and color v 1 and v 7 with a same color. Then restrict 1iv. Then we color v ′′′ 5 and v ′′ 5 in this order. Observe the remaining uncolored vertices are v ′ 7 , v 7 , v 0 , v 1 and v 2 . If the lists of available colors of these vertices, do not correspond to Figure 5, then we are done. And it is indeed the case, since the only colored vertex seen by both v 0 and v ′ 7 is v 6 , and since initially

L(v 5 ) to L(v 5 ) \ L(v ′′ 5 ) and color vertices v 6 , v 5 , v 4 , v ′ 4 , v 3 by Figure 1v. Finish by coloring vertices v ′ 5 , v ′′′ 5 , v ′′ 5 , v 7 , v 2 , v 0 in this order. Observe that L(v 1 ) ⊂ L(v 0 ). Therefore, since L(v 1 ) ∩ L(v 7 ) = ∅ and since we are doing a 6-coloring, we conclude that L(v ′ 7 ) ⊂ L(v 0 ). We color v ′ 5 with x / ∈ L(v ′′ 5 ) and v 6 , v 5 , v 4 , v ′ 4 , v 3 by Figure
L(v ′ 7 ) ⊂ L(v 0 ). Proof of Figure 7v. We have G[S] 2 = G 2 [S].
Color vertices v 0 and v 4 with the same color by pigeonhole principle and then v 3 , v 1 and v 2 in this order. The remaining vertices can be colored by Figure 1x.

Proof of Figure 7vi. If v ′ 3 sees v ′ 7
, then they must be at distance exactly 2 since G has girth 8.

Say v 8 is their common neighbor, then v 0 , v 7 , v ′ 7 , v 8 , v ′ 3 , v 3 , v 2 and v 1 form the reducible configuration from Figure 7i. Thus, we have G[S] 2 = G 2 [S]. First, observe that |L(v ′ 7 )| = |L(v ′ 5 )| = |L(v ′ 6
)| = 3 and we will prove the following: andv ′ 3 by Figure 1xiii. Finish by coloring v 7 , v 0 , and v ′ 7 in this order.

• L(v 6 ) = L(v ′ 7 ). Otherwise, color v 6 differently from L(v ′ 7 ), then color v 1 and v 2 in this order. Color v ′ 5 , v 5 , v 4 , v 3 ,
• L(v 6 ) = L(v ′ 5 ). Otherwise, color v 6 differently from L(v ′ 5 ), then color v ′ 7 , v 7 , v 0 , v 1 , and v 2 by Figure 1ii. Finish by coloring v ′ 3 , v 3 , v 5 , v 4 , and v ′ 5 in this order. • L(v 1 ) ∩ L(v ′ 7 ) = ∅. Otherwise, color v 1 and v ′ 7 with x ∈ L(v 1 ) ∩ L(v ′ 7 )
. Then, color v 2 and v 6 . Color v ′ 5 , v 5 , v 4 , v 3 , and v ′ 3 by Figure 1xiii. Finish by coloring v 7 and v 0 in this order. Using the equalities above, we have the following. Color v 7 differently from L(v 6 ) and L(v ′ 7 ). Now, color v 1 and v 4 with the same color, which is possible since v 4 has all six colors available. Observe that, since

L(v 1 ) ∩ L(v ′ 7 ) = ∅ and L(v ′ 7 ) = L(v 6 ) = L(v ′ 5
), v 6 and v 5 still have the same amount of available colors remaining. Finish by

coloring v 2 , v ′ 3 , v 3 , v 5 , v 6 , v ′ 5 , v 0 , and v ′ 7 in this order. Proof of Figure 7vii. Note that G[S] 2 = G 2 [S].
Here, we redefine and e = φ(v 6 ). Observe that L(v ′ 6 ) = L(v 7 ), otherwise, we can permute the colors of v ′ 6 and v 7 in φ and extend φ to G as L(v 0 ) would no longer be {a, b, c}. Symmetrically,

S = {v 0 , v 1 , v ′ 1 , v 2 }. Consider φ a coloring of G -S. Note that if φ is extendable to G, then we have a contradiction. Thus, L(v 0 ) = L(v 1 ) = L(v ′ 1 ) = L(v 2 ) = {a, b, c} by Figure 3. Now, we uncolor v 3 , v 4 , v ′ 4 , v 5 , v 6 , v ′ 6 , v
L(v 3 ) = L(v ′ 4 ). If d / ∈ L(v ′ 6 ), then we can color v 7 with d, v 6 with x = e, v 5 , then v 3 , v 4 , v ′ 4 by Figure 2 since L(v 3 ) = L(v ′ 4), and finish by coloring v ′ 6 . As L(v 0 ) = {a, b, c}, φ is extendable to G. Now, d ∈ L(v ′ 6
). In which case, there exists y ∈ L(v 7 ) \ L(v ′ 6) so we color v 7 with y, v 6 with z = d, v 5 , then v 3 , v 4 , v ′ 4 and finish by coloring v ′ 6 . Finally, φ is extendable to G because L(v 0 ) = {a, b, c}.

Lemma 9. Graph G does not contain the configurations depicted in Figure 8.

Proof. Proof of Figure 8i. If v 1 does not see v 7 . Then the proof is a direct implication of Figure 1xv. If v 1 sees v 7 , then they must be at distance exactly 2 since G has girth at least 8 and therefore |L(v 1 )| ≥ 3 and |L(v 7 )| ≥ 3. We color v 1 such that v 2 has at least 2 colors left. We then obtain Figure 1xiii.

Proof of Figure 8ii. If v 1 sees v ′ 6 , then they must be at distance exactly 2 since G has girth at least 8. Say v 0 is their common neighbor, then v ′ 6 , v 0 , v 1 , . . . , v 6 form the reducible configuration from Figure 7i. If v 1 sees v 7 , then they share a common neighbor v 0 and

v 1 , v 2 , v 3 , v 4 , v 5 , v ′ 5 , v 6 , v ′ 6 , v 7 , v 8 , v 0 form the reducible configuration from Figure 7ii. If v 2 sees v 8 , then they share a common neighbor v ′ 2 and v 8 , v ′ 2 , v 2 , v 1 , v 3 , v 4 , v 5 , v ′ 5 , v 6 , v ′ 6 , v 7 form the reducible configuration from Figure 7iii.
If v 1 sees v 8 , they must be at distance exactly 2 since both are 2-vertices and there are no 2-paths due to Lemma 6. Thus, 1viii and finish by coloring v 3 and v 1 in this order. Therefore, 1viii, and finish by coloring v 3 and v 1 in this order. Therefore, Lemma 10. Graph G does not contain the 8-faces depicted in Figure 24 in the Appendix.

3 ≤ |L(v 1 )|, |L(v 8 )| ≤ 4. If we can color v 2 such that v 1 has at least 3 colors left, then we can color v 4 , v 5 , v ′ 5 , v 6 , v ′ 6 , v 7 , v 8 by Figure
|L(v 1 )| = 3 and L(v 2 ) ⊆ L(v 1 ). We color v 3 with x / ∈ L(v 1 ). Then, we color v 4 , v 5 , v ′ 5 , v 6 , v ′ 6 , v 7 by Figure 1vii and finish by coloring v 8 , v 2 and v 1 in this order. Now, G[S] 2 = G 2 [S]. If we can color v 2 such that v 1 has at least 2 colors left, then we can color v 4 , v 5 , v ′ 5 , v 6 , v ′ 6 , v 7 , v 8 by Figure
L(v 1 ) = L(v 2 ) and |L(v 1 )| = 2. We restrict L(v 3 ) to L(v 3 ) \ L(v 1 ). Then, we color v 3 , v 4 , v 5 , v ′ 5 , v 6 , v ′ 6 , v 7 ,
(v 5 ) to L(v 5 ) \ L(v ′ 6 ) and L(v 4 ) to L(v 4 ) \ L(v ′′ 4 ). We color vertices v 5 , v 4 , v 3 , v 2 , v 1 , v ′ 3 , v ′′ 3 , v ′′′ 3 by Figure 1x. Then finish by coloring v ′ 5 , v ′ 4 , v ′′′ 4 , v ′′ 4 , v 6 , v 7 , v ′ 6 in this order. v 1 v 2 v 3 v 4 v 5 v 6 v 7 2 2 4 3 4 2 2 (i) 1a1a1c, 1a1a1a1, c1a1c v 1 v 2 v 3 v 4 v 5 v 6 v 7 v 8 2 2 4 3 4 4 2 2 v ′ 5 3 v ′ 6 3 (ii) c1a0c0c0c v 1 v 2 v 3 v 4 v 5 v 6 v 7 2 2 5 6 5 4 3 v ′ 3 4 v ′′ 3 3 v ′′′ 3 3 v ′ 4 4 v ′′ 4 3 v ′′′ 4 3 v ′ 5 3 v ′ 6 3 (iii) 1a0b0b0c0c1, 1a0b0b0b1, c0b0b0b1, c0b0b0c0c1
The proof of Lemma 10 is also in the Appendix. It follows the same scheme as Lemma 8 and uses Section 1 as well as the previous lemma. There are a lot of configurations and their proofs are quite tedious and do not contribute extra value to what we already know, even though they are necessary.

We have started out by coloring these configurations by computer (by testing all precoloring of the set of vertices separating our configuration from the rest of the graph) but this proves to be very time consuming. Moreover, there are tricks that can be done manually (restricting the considered set of vertices in the configurations, uncoloring then recoloring part of the configuration) that can hardly be replicated by computer. Concretely, it means that not all precoloring is a possible precoloring of a proper subgraph of G and we cannot know which precoloring to test, which not to with our naive approach.

Lemma 11. Consider the configuration in Figure 9. If v 3 , v 4 , v 5 , v 6 , and v 7 are colorable, but the configuration as a whole is not, then ) and uncolor v 3 , v 4 , v 5 , v 6 , and v 7 . Due to our previous observations, we can assume w.l.o.g. that v 3 and v 7 must have been colored d and e respectively. Moreover, due to Lemma 3, since we know that v 3 , v 4 , v 5 , v 6 , and v 7 are colorable, there exists another coloring of these vertices where v 3 is not colored d or v 7 is not colored e. As v 0 , v 1 , v ′ 1 , and v 2 must remain uncolorable, we know that v 3 must have been colored e and v 7 colored d. So, we know that {d, e} ⊆ L(v 3 ) and {d, e} ⊆ L(v 7 ). In addition, when v 3 was colored d (e), d (e) must be in L(v 2 ) or we would have had |L(v 2 )| ≥ 4 after the coloring of v 3 , v 4 , v 5 , v 6 , and v 7 . In other words, L(v 2 ) = {a, b, c, d, e}. Symmetrically, the same holds for L(v 0 ). Knowing that L(v 2 ) = {a, b, c, d, e}, when v 3 was colored d (e), v 4 must have been colored e (d). So we get {d, e} ⊆ L(v 4 ). Similarly, the same holds for L(v 6 ). Finally, if any of v 3 , v 4 , v 6 , or v 7 has another available color than d and e, we could have colored them with one vertex not colored d, nor e, and finish coloring the rest of the configuration due to Figure 5 and Figure 3, which is impossible. Consequently, we have

L(v 3 ) = L(v 4 ) = L(v 6 ) = L(v 7 ) = L(v 1 ) \ L(v ′ 1 ) and |L(v 3 )| = 2. v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 5
L(v 3 ) = L(v 4 ) = L(v 6 ) = L(v 7 ) = L(v 1 ) \ L(v ′ 1 ) = {d, e}.
Lemma 12. The configurations in Figure 10 are colorable.

v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 5 5 6 v ′ 1 3 5 3 4 4 3 v ′ 4 3 v ′′ 4 u ′′ 4 3 4 v 8 u 8 3 5 v ′′ 6 u ′′ 6 3 4 v ′ 6 3 (i) v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 5 5 6 v ′ 1 3 5 3 4 4 3 v ′ 4 2 v ′′ 4 2 v 8 4 v ′′ 6 2 v ′ 6 2 (ii) v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 5 5 5 v ′ 1 3 5 3 4 2 2 v ′ 4 v ′′ 4 2 2 (iii)
, v ′ 1 (= u 8 ), v 0 , v 2 , and v 1 in this order. • If L(v 3 ) ∩ L(v 7 ) = ∅, then it suffices to show that we can color v 3 , v 4 , v 5 , v 6 , v 7 , v ′ 4 , v ′′ 4 , u ′′ 4 , v 8 , v ′ 6 , v ′′ 6
, and u ′′ 6 . Indeed, say they are colorable with φ, then after coloring

v ′ 4 , v ′′ 4 , u ′′ 4 , v 8 , v ′ 6 , v ′′ 6
, and u ′′ 6 with φ, we obtain the configuration from Figure 7vii where v 3 , v 4 , v 5 , v 6 , and v 7 are colorable (with φ) but L(v 3 )∩L(v 7 ) = ∅, so the whole configuration can be colored.

It remains to show that there exists such a coloring φ. Start by coloring v ′′ 4 such that u ′′ 4 still has 3 colors remaining. Similarly, color v 6 such that v 7 still has 3 colors remaining. Finish by coloring v

′ 4 , v 4 , v 3 , v 5 , v ′ 6 , v 7 , v ′′ 6 , u ′′ 6 , v 8
, and u ′′ 4 in this order. Now, observe that v ′ 1 might see u ′′ 4 and if it does, then they must be at distance exactly 2 since G has no 2 + -paths due to Lemma 6. Symmetrically, the same holds if v ′ 1 sees u ′′ 6 . The following colorings will still work when v ′ 1 sees u ′′ 4 or u ′′ 6 . Consider the two following cases: 1viii. Observe that we obtain the configuration from Figure 7vii where v 3 , v 4 , v 5 , v 6 , and v 7 are colorable by Figure 5 since L(v 3 ) and L(v 7 ) will have at least one color in common. Moreover, we will have either to obtain a non-negative amount of charge on faces. Thus, we will get a non-negative total of charge, which is a contradiction to Equation (1). In our proof, we have to consider a large number of non-reducible 8-faces.

• If |L(v 3 )∩L(v 7 )| ≥ 2, say {d, e} ⊂ L(v 3 )∩L(v 7 ), then let x ∈ L(v 3 )\{d, e}. We restrict L(v ′ 4 ) to L(v ′ 4 )
To handle this, we will provide a computer procedure that checks the remaining charge on each non-reducible 8-face. In order to define this procedure, we will present an encoding of the 8-faces, the reducible configurations, and the discharging rules.

First round: vertices to vertices

We define the following discharging rules on the vertices of G : R0 A 3-vertex gives 1 to a 2-neighbor.

R1 A 3-vertex gives 1 2 to a (1,1,0)-neighbor.

R2 A 3-vertex gives 1 2 to a (1,1,1)-vertex at distance 2. We will now calculate the exact amount µ * (v) of charges that v ends up with after applying R0, R1 and

R2. If d(v) = 2: Recall that the initial charge for v is µ(v) = 7 2 d(v) -9 = -2.
By Lemma 6, v can only have 3-neighbors. According to the discharging rules, v receives 1 from each of its neighbor by R0 and does not give any charge away. Thus, v ends up with

µ * (v) = -2 + 2 • 1 = 0. If d(v) = 3: Recall that the initial charge is µ(v) = 7 2 d(v) -9 = 3 2 . • If v is a (1, 1, 1)-vertex.
Every neighbor of v is a 2-vertex so only R0 and R2 may apply. However, due to Figure 6i, there is no (1, 1, 0 + )-vertex at distance 2 from v. So, v does not give away any charge to 3-vertices but only receive instead. Thus, by R0 and R2, we have

µ * (v) = 3 2 -3 • 1 + 3 • 1 2 = 0. • If v is a (1, 1, 0)-vertex.
Due to Figure 6i, there is no (1, 1, 1)-vertex at distance 2 from v so R2 does not apply. Due to Figure 6iii, v cannot have a (1, 1, 0)-neighbor. So, v does not give away any charge to 3-vertices but only receive by R1 instead. Thus, by R0 and R1, we have

µ * (v) = 3 2 -2 • 1 + 1 2 = 0. • If v is a (1, 0, 0)-vertex.
-If v has a (1, 1, 0)-neighbor, v cannot have another (1, 0 + , 0)-neighbor due to Figure 6ii. By Figure 6iv, v cannot share a common 2-neighbor with a (1, 1, 0 + )-vertex at distance 2 so R2 does not apply. Hence, by R0 and R1, we have

µ * (v) = 3 2 -1 - 1 2 = 0.
-If v see a (1, 1, 1)-vertex at distance 2, v can only see exactly one such vertex. By Figure 6iv, v cannot have (1, 1, 0)-neighbor so R1 does not apply. Thus, by R0 and R2, we have

µ * (v) = 3 2 -1 - 1 2 = 0.
-If v does not have a (1, 1, 0)-neighbor and does not see a (1, 1, 1)-vertex at distance 2, then only R0 applies and we have

µ * (v) = 3 2 -1 = 1 2 .
• If v is a (0, 0, 0)-vertex.

Observe that R0 and R2 cannot apply since v does not have any 2-neighbor and cannot see a (1, 1, 1)vertex at distance 2. So, only R1 can apply and by Figure 6vii, v cannot have three (1, 1, 0)-neighbors. Consequently,

if v has exactly two (1, 1, 0)-neighbors, then we have

µ * (v) = 3 2 -2 • 1 2 = 1 2 .
if v has exactly one (1, 1, 0)-neighbor, then we have

µ * (v) = 3 2 - 1 2 = 1.
if v has no (1, 1, 0)-neighbor, then we have

µ * (v) = 3 2 .
Below, we recapitulate the remaining charges of each type of 3-vertex v (as 2-vertices are at 0) after applying R0, R1, and R2. In Figures 11 to 17, the 2-vertices will be filled while the 3-vertices will not be.

w 1 v w 2 w 3 Figure 11: (1,1,1). w 1 , w 2 , w 3 = (1, 1, 0 + ). µ * (v) = 0. u 1 v w 2 w 3 Figure 12: (1,1,0). u 1 = (1, 1, 0) and w 2 , w 3 = (1, 1, 1). µ * (v) = 0. w 1 v u 2 u 3 Figure 13: (1,0,0). w 1 = (1, 1, 1) and u 2 , u 3 = (1, 1, 0). µ * (v) = 1 2 . w 1 v u 2 w ′′ 2 u 3 w ′ 2 (i) w 1 = (1, 1, 0 + ) and u 3 = (1, 0 + , 0). w 1 v u 2 u 3 w ′ 1 w ′′ 1 (ii) u 2 , u 3 = (1, 1, 0). Figure 14: (1,0,0). µ * (v) = 0. u 1 v u 2 u 3 Figure 15: (0,0,0). u 1 , u 2 , u 3 = (1, 1, 0). µ * (v) = 3 2 . u 1 v u 2 w ′′ 2 u 3 w ′ 2 Figure 16: (0,0,0). u 1 , u 3 = (1, 1, 0). µ * (v) = 1. u 1 v u 2 w ′′ 2 u 3 w ′ 2 w ′′ 3 w ′ 2 Figure 17: (0,0,0). u 1 = (1, 1, 0). µ * (v) = 1 2 .

Second round: vertices to faces

Recall that µ * (v) is the remaining charges of v after applying rules R0-R2. We define the following discharging rules between the vertices and 8-faces of G: R3 If a 3-vertex v is not a (1, 0, 0)-vertex, then it gives µ * (v) n1 to each incident 8-face, where n 1 is the number of incident 8-faces.

v µ * (v) 3 2 1 1 2 0 (1,
R4 For a (1, 0, 0)-vertex v, let n 2 be the number of 8-faces incident to v and to its 2-neighbor. Vertex v gives µ * (v) n2 to each of these n 2 8-faces. Recall that, given a face f , the initial amount of charge µ(f ) = d(f ) -9 so all k-faces with k ≥ 9 have a positive charge. Moreover, after applying R3-R4, every 3-vertex v will have a remaining charge of at least

µ * (v) -n i • µ * (v) ni = 0 for 1 ≤ i ≤ 2.
As a result, it remains to verify that every 8-face f will receive at least charge 1 so that its final charge will be µ * (f ) ≥ µ(f ) -9 + 1 = 8 -8 = 0.

To generate every possible 8-face efficiently, we introduce the following encoding of a configuration around an 8-face.

Encoding a face f :

• For every pair of consecutive 3-vertices in clockwise order, count the number of 2-vertices in between. We obtain a circular sequence of integers in clockwise order of length equal to the number of 3-vertices of f . Since G has no 2 + -paths by Lemma 6, each integer is in {0, 1}. Observe that there are at most as many ways to write this sequence of integers as the number of 3-vertices of f . Indeed, we can choose any 3-vertex v as a starting point and start counting the number of 2-vertices between v and the next 3-vertex in clockwise order. We choose as representative the first one in the lexicographic order where 1 precedes 0 and call it the number-word of f . Examples:

v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 1 1 0 0 0 0 (i) 110000 v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 1 0 0 1 0 0 (ii) 100100
-Take the 8-face in Figure 18i as an example. We consider the 3-vertices in clockwise order starting at any 3-vertex, say v 1 . We get v 1 , v 3 , v 4 , v 5 , v 6 , v 7 . Now, we count the number of 2-vertices between two consecutives vertices in that sequence. More precisely, there is one 2-vertex (v 2 ) in between v 1 and v 3 , then none between v 3 and v 4 , and so on. This gives us the sequence of numbers 100001. Had we chosen another starting 3-vertex (say v 3 ) we would have obtained another sequence (000011). Among all of these different sequences, we choose the one that comes first in the lexicographic order where 1 comes before 0. And that sequence is 110000, the number-word of f , which corresponds to the starting 3-vertex v 7 .

-We can do the same with the 8-face in Figure 18ii. The number-word for f is 100100. Observe that this sequence can be obtained by taking, in clockwise order, either v 7 or v 3 as a starting point.

• Due to our discharging rules, we are interested in configurations around 3-vertices. So, given a 3-vertex v on f , we choose the following letters to encode the neighborhood outside f of v:

c means that v has a 2-neighbor outside f .

b means that v has a (1, 1, 0)-neighbor outside f .

a represents the rest of the possible neighbors of v. In other words, the neighbor of v outside f is a 3-vertex that is not a (1, 1, 0)-vertex.

Observe that there may be multiple starting 3-vertices that give the same number-word for f . Given one possible starting 3-vertex of the number-word nw, we insert between each pair of consecutive integers of nw the letter encoding of the neighborhood outside f of the corresponding 3-vertex. We obtain an alternating sequence f w of integers and letters for each starting 3-vertex.

Among the possible alternating sequences f ws, we choose the one where the subsequence of letters is the smallest in alphabetical order. We call this alternating sequence the full-word of f and the corresponding subsequence of letters the letter-word of f . Examples:

v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 v ′ 4 v ′′ 4 v ′′′ 4 v ′ 5 v ′ 7 1 1 0 0 0 0 a a b c a c (i) 1a1a0b0c0a0c v 0 v 1 v 2 v 3 v 4 v 5 v 6 v 7 v ′ 3 v ′ 5 v ′ 7 1 a 0 a 0 c 1 c 0 a 0 a (ii) 1a0a0c1c0a0a
-Take the 8-face f in Figure 19i as an example. It is the same face as in Figure 18i, this time with more information about the neighborhood of the 3-vertices outside of f . Observe that when we do not have extra information about the neighborhood of a 3-vertex outside of f (it could be a, b, or c), we will denote it a for now and explain it later on. We consider the neighborhood of each 3-vertex, starting with the one that comes right after the first number, which is the 3-vertex v 1 . In order, they corresponds to the letters a, a, b, c, a, c, which give us the letter-word aabcac. Finally, we combine these the number-word and the letter-word into the full-word 1a1a0b0c0a0c.

-We can do the same with the 8-face in Figure 19ii, which is the face in Figure 18ii with extra information. When we choose the letter-word for f , we need to consider two encodings, one that starts with the 3-vertex that comes right after v 7 in clockwise order, namely v 1 , or the one after v 3 , namely v 5 . These give us two sequence of letters aaccaa and caaaac respectively. For our letterword, we choose the first one in alphabetical order, which is aaccaa. Finally, we get the full-word 1a0a0c1c0a0a.

Observation 1. Each face has a unique encoding full-word and each full-word uniquely defines a face.

Under each 8-cycle of Figures 7,9 and 24, you have the corresponding encoding of the reducible configuration if it were an 8-face.

In what follows we explain the generation of all possible 8-faces, how to check which ones are reducible and which ones will obtain enough charge from its incident 3-vertices by R3 and R4. The corresponding pseucode is summarized in Algorithm 1.

Algorithm 1: Filtering forbidden and dischargeable full-words corresponding to faces with a given size.

Data: forbidden_subwords, dictionary_of_charges, number_words, alphabet, target_charge.

Result: The list of full-words that are not forbidden nor dischargeable. Since G has no 2 + -paths and f has length 8, there can be at most four 2-vertices on f . On the other hand, given a number-word nw of f , the number of 2-vertices of f is given by the number of 1s in nw. Therefore, one can easily check the following observation: Observation 2. The only possible number-words for 8-faces in G are 1111, 11100, 11010, 110000, 101000, 100100, 1000000, and 00000000.

Since the process of generating these number-words is done naively and it is not the main focus of the algorithm, we will not go into technical details.

However, the script is available at https://gite.lirmm.fr/discharging/planar-graphs. For this case, the set of number-words is small enough that it can even be checked manually. Now, for each number-word nw, we can generate all possible sequences of letters in {a, b, c} with the same length as nw that we will then interlace with nw to create an alternating sequence corresponding to a full-word (line 5 of Algorithm 1). Observe that during this process of generation, we may obtain several words representing the same face and only one of them is the unique full-word encoding f . This has no influence on the correctness of our algorithm, only the time complexity, as some faces might be checked multiple times. Here, it is possible to identify the symmetries in the generated words in order to keep the unique full-words. However, in practice, at least for our case, this subroutine adds complications with minimal time gain.

The list of full-words described above corresponds to all possible neighborhoods at distance at most 2 of an 8-face. We filter out every neighborhood that either contains a reducible configuration of Lemmas 7 to 10 (line 6 of Algorithm 1), or has enough charge available for its 8-face by R3 and R4 (line 8 of Algorithm 1).

In order to check that the corresponding subgraph of a full-word contains a reducible configuration, we encode the latter using similar conventions as for the neighborhood of the 8-faces. Indeed, the considered configuration is encoded as seen from an incident face. Thus, one configuration may have multiple different encodings (depending on the incident faces) and we call these encodings forbidden subwords. A full-word that contains a forbidden subword is forbidden.

Since we always consider the worst case scenario, if a forbidden subword contains a letter a, then one can always build two other ("weaker") forbidden subwords by replacing this a by b or c. Therefore, whenever we consider a forbidden subword containing a, we also implicitly consider the other "weaker" subwords. See Figures 6 to 8 and 24 where the captions contain all possible forbidden ("strong") subwords of each reducible configuration. In a general case, one can define a different symbol (another letter, say d for example) that can be rewritten as multiple different letters (here a, b, and c). Our choice was a for simplicity.

In the code implementation of Algorithm 1, we define a forbidden subword as a regular expression and rewriting rule (formal grammar) in which a can be rewritten as b or c. Observation 3. In a forbidden subword, a can mean a, b, or c in a real encoding. Now, recall that a full-word is actually circular and is read in clockwise order. Thus, in order to check whether it is forbidden, one has to check if it contains a forbidden subword or its mirror. Once we removed the forbidden subword, we are ready to move to the next step of the algorithm. The next step (lines 7-8 of Algorithm 1) is to check, for every full-word f w, whether the 3-vertices of the corresponding subgraph give enough charge to f according to R3 and R4 (at least a total charge 1). If it is the case, we say that f w is dischargeable. Similar to the encoding of the reducible configurations, we can also encode into a dictionary the configurations from Figures 11 to 17 for R4 (Figures 13 and14). To work with integers, we multiply by 12 the charge of each vertex and each face of G. In Table 2, we detail the dictionary entries for each configuration. Table 2: The dictionary of charges. Each entry is written as "<encoding> : <charge>". Every value was multiplied by 12 to get an integer.

Observe that, in our case, every encoding in a dictionary entry starts and ends with a number. Thus, we have the following observation.

Observation 4. The encoding in a dictionary entry always has odd length.

As a consequence, the 3-vertex v that holds the charge in the encoding of a dictionary entry corresponds to either • the letter in the middle when it has length 3 or 7,

• or the letter in second position when it has length 5.

Once again, each encoding can be read from left to right or right to left. Note that one has to be mindful of the position of v when reading an encoding of length 5 from right to left.

In order to count the total amount of charge that an 8-face will receive from its 3-vertices, the algorithm consists of sliding a window of odd length across the circular full-word. We start with the window of the largest possible length (7 according to our dictionary) in order to have the most information about the neighborhood of v. At each step, it searches for the corresponding encoding (or its mirror) in the dictionary and if it exists, it marks the position as "discharged" and adds the corresponding amount of charge to its total amount. For a given window size, if the corresponding subword is not in the dictionary, then it means that the dictionary entry corresponding to v must have an encoding of smaller length (recall that the dictionary entries are exhaustive). Then, it suffices to verify that the total amount is at least 12 (target_charge) since we multiplied every charge by 12. In such a case, we know that our 8-face will end up with a non-negative amount of charge.

Third round: faces to faces

We ran Algorithm 1 to compute the outcome of the second round of discharging. The only remaining type of face which was output by the algorithm (full-word: 1c1a0a1a0a) corresponds to the face f in Figure 20. We define another discharging rule R5 to take care of this last case.

R5 Let f and f ′ be as depicted in Figure 20. If f ′ is an 8-face, then f ′ gives 1 2 to f . one edge removed: it has mad = 14 5 and it needs 8 colors, while all subcubic planar graphs are 7-colorable [START_REF] Hartke | The chromatic number of the square of subcubic planar graphs[END_REF][START_REF] Thomassen | The square of a planar cubic graph is 7-colorable[END_REF]. Observe that the class of graphs with mad ≤ 14 5 does not even contain all planar graphs with girth 6. For girth 8, the corresponding graphs with bounded mad verify mad < 8 3 . If Theorem 2 is generalizable to graphs with mad < 8 3 , then it would be optimal in terms of mad as the Petersen graph with one vertex removed has mad = 8 3 and it needs 7 colors. On the other hand, it is unclear whether there exists a planar graph with girth 7 needing 7 colors.

A 5-cycle with a subdivided chord, which has mad = 7 3 , shows that a generalization of Theorem 2 to graphs with mad < 8 3 would also be optimal in terms of number of colors. Once again, it does not mean that there exists a planar graph with girth 8 that needs 6 colors.

In what follows, we provide a planar subcubic construction, with relatively high girth that needs 6 colors. Precisely, we provide a construction of a planar subcubic graph having girth 6 and χ 2 ≥ 6.

We call our 5 colors a, b, c, d, and e.

Lemma 13. The graph G ′ (u 1 , u 2 , v 1 , v 2 ) in Figure 21i has the following properties:

• G ′ (u 1 , u 2 , v 1 , v 2
) is planar and subcubic.

• G ′ (u 1 , u 2 , v 1 , v 2 ) has girth 6.

• The distance in G ′ (u 1 , u 2 , v 1 , v 2 ) between u 1 and v 1 is 5.

• For every 5-coloring φ of G ′ (u 1 , u 2 , v 1 , v 2 ), if φ(u 1 ) = φ(v 1 ), then φ(u 2 ) = φ(v 2 ). u 1 u 2 u 3 u 4 w 1 w 2 x 1 x 2 y 1 y 2 v 1 v 2 v 3 v 4 (i) The gadget G ′ (u 1 , u 2 , v 1 , v 2 ) in Lemma 13. u 1 u 2 G ′ v 2 v 1 (ii) Simplified drawing of G ′ (u 1 , u 2 , v 1 , v 2 ).

Figure 21

Proof. One can verify that G ′ (u 1 , u 2 , v 1 , v 2 ) is planar, subcubic, has girth 6, and that the distance between u 1 and v 1 is 5 thanks to Figure 21i. It remains to prove that if φ(u 1 ) = φ(v 1 ), then φ(u 2 ) = φ(v 2 ) for every

5-coloring φ of G ′ (u 1 , u 2 , v 1 , v 2 ).
Suppose by contradiction that there exists a 5-coloring

φ of G ′ (u 1 , u 2 , v 1 , v 2 ) such that φ(u 1 ) = φ(v 1 ) = a, but b = φ(u 2 ) = φ(v 2 ) = c.
We can assume w.l.o.g. that φ(u 3 ) = d and φ(u 4 ) = e. As a result, we have φ(v 3 ) = e and φ(v 4 ) = d. Since w 1 sees u 2 , u 3 , and v 3 , φ(w 1 ) ∈ {a, c}. Since x 2 sees u 2 , u 4 , and v 4 , φ(x 2 ) ∈ {a, c}. Since y 2 sees v 2 , v 3 , and u 3 , φ(y 2 ) ∈ {a, b}. Since w 2 sees v 2 , v 4 , and u 4 , φ(w 2 ) ∈ {a, b}.

• If φ(x 2 ) = c, then φ(w 1 ) = a, φ(w 2 ) = b, and φ(y 2 ) = a. However, x 1 sees u 3 , w 1 , w 2 , x 2 , and u 4 which are colored d, a, b, c, and e respectively. So, x 1 is not colorable.

• If φ(x 2 ) = a, then φ(w 1 ) = c.

-If φ(w 2 ) = b, then x 1 is not colorable since it sees u 3 , w 1 , w 2 , x 2 , and u 4 which are colored d, c, b, a, and e respectively.

-If φ(w 2 ) = a, then φ(y 2 ) = b and y 1 is not colorable since it sees w 1 , w 2 , v 4 , y 2 , and v 3 which are colored c, a, d, b, and e respectively.

Lemma 14. The graph G = (u 1 , u 2 , v 1 , v 2 ) in Figure 22i has the following properties:

• G = (u 1 , u 2 , v 1 , v 2
) is planar and subcubic.

• G = (u 1 , u 2 , v 1 , v 2 ) has girth 6.
• The distance in G = (u 1 , u 2 , v 1 , v 2 ) between u 1 and v 1 is 5.

• Every 5-coloring φ of G = (u 1 , u 2 , v 1 , v 2 ) satisfies φ(u 1 ) = φ(v 1 ) and φ(u 2 ) = φ(v 2 ). u 1 u 2 u 3 u 4 w 1 w 2 x 1 x 2 y 1 y 2 z 1 z 2 s 1 t 1 v 1 v 2 v 3 v 4 G ′ G ′ (i) The gadget G = (u 1 , u 2 , v 1 , v 2 ) in Lemma 14. u 1 u 2 G = v 2 v 1 (ii) Simplified drawing of G = (u 1 , u 2 , v 1 , v 2 ).

Figure 22

Proof. One can verify that G = (u 1 , u 2 , v 1 , v 2 ) is planar, subcubic, has girth 6, and that the distance between u 1 and v 1 is 5 thanks to Figure 21i. Now, let φ be a 2-distance 5-coloring of

G = (u 1 , u 2 , v 1 , v 2 ).
First, observe the following:

Claim 1. We have {φ(w 1 ), φ(s 1 ), φ(t 1 ), φ(u 3 ), φ(v 3 )} = {a, b, c, d, e} and {φ(y 1 ), φ(s 1 ), φ(t 1 ), φ(u 4 ), φ(v 4 )} = {a, b, c, d, e}.

Proof. By symmetry, we can suppose by contradiction that {φ(w 1 ), φ(s 1 ), φ(t 1 ), φ(u 3 ), φ(v 3 )} = {a, b, c, d, e}. Since φ(x 1 ) / ∈ {φ(s 1 ), φ(t 1 ), φ(u 3 ), φ(v 3 )}, we get φ(w 1 ) = φ(x 1 ), in which case φ(w 2 ) = φ(x 2 ) by Lemma 13 due to G ′ (w 1 , w 2 , x 1 , x 2 ). However, φ(w 2 ) / ∈ {φ(w 1 ), φ(s 1 ), φ(u 3 )} and φ(x 2 ) / ∈ {φ(x 1 ), φ(t 1 ), φ(v 3 )}, which is impossible since {φ(w 1 ), φ(s 1 ), φ(t 1 ), φ(u 3 ), φ(v 3 )} = {a, b, c, d, e}.

We can assume w.l.o.g. that φ(u 1 ) = a, φ(u 2 ) = b, φ(u 3 ) = c, and φ(u 4 ) = d. We claim the following. Claim 2. We must have {φ(v 3 ), φ(v 4 )} = {c, d}.

Proof. If {φ(v 3 ), φ(v 4 )} = {c, d}, then φ(v 3 ) = d and φ(v 4 ) = c. Observe that φ(w 1 ), φ(s 1 ), and φ(t 1 ) must all be distinct and they are also different from {c, d}. As a result, we get {φ(w 1 ), φ(s 1 ), φ(t 1 ), φ(u 3 ), φ(v 3 )} = {a, b, c, d, e}, which is impossible by Claim 1.

Claim 3. If φ(v 4 ) = c, then d / ∈ {φ(w 1 ), φ(x 1 ), φ(x 2 )}. Symmetrically, if φ(v 3 ) = d, then c / ∈ {φ(y 1 ), φ(z 1 ), φ(z 2 )}.
Proof. If φ(v 4 ) = c, then suppose by contradiction that d ∈ {φ(w 1 ), φ(x 1 ), φ(x 2 )}. Observe that φ(y 1 ), φ(s 1 ), and φ(t 1 ) must all be distinct and they are also different from {c, d}. As a result, we get {φ(y 1 ), φ(s 1 ), φ(t 1 ), φ(u 4 ), φ(v 4 )} = {a, b, c, d, e}, which is impossible by Claim 1.

By symmetry, the same arguments hold for c / ∈ {φ(y 1 ), φ(z 1 ), φ(z 2 )} when φ(v 3 ) = d. Now, suppose by contradiction that we have the following cases.

Case 1: φ(u 1 ) = φ(v 1 ). In this case, φ(v 1 ) = φ(u 1 ) = a. Note that φ(v 2 ) / ∈ {φ(v 1 ), φ(u 3 ), φ(u 4 )} = {a, c, d}. Moreover, if φ(v 2 ) = e, then we necessarily have φ(v 3 ) = d and φ(v 4 ) = c which is impossible due to Claim 2. As a result, φ(v 2 ) = b.

By Claim 2 and by symmetry, we can assume that φ(v 3 ) = e and as a consequence, φ(v 4 ) = c. By Claim 3, d / ∈ {φ(w 1 ), φ(x 1 ), φ(x 2 )}. Consequently, φ(w 1 ) = a and φ(x 1 ) = a, which in turn implies that φ(w 2 ) = φ(x 2 ) = b by Lemma 13 and G ′ (w 1 , w 2 , x 1 , x 2 ). Hence, φ(s 1 ) = e and we get a contradiction since φ(y 1 ) / ∈ {φ(w 1 ), φ(s 1 ), φ(u 2 ), φ(u 4 ), φ(v 4 )} = {a, e, b, d, c}.

Case 2: φ(u 2 ) = φ(v 2 ). Since φ(v 2 ) / ∈ {φ(u 2 ), φ(u 3 ), φ(u 4 )} = {b, c, d}, we have φ(v 2 ) ∈ {a, e}. By Claim 2 and by symmetry, we can assume that φ(v 3 ) ∈ {a, e}. As a consequence, {φ(v 2 ), φ(v 3 )} = {a, e} and φ(v 4 ) = c. By Claim 3, d / ∈ {φ(w 1 ), φ(x 1 ), φ(x 2 )}. Consequently, φ(w 1 ) = φ(v 2 ) and φ(x 1 ) = b. Hence, φ(s 1 ) = φ(v 3 ) and we get a contradiction since φ(y 1 ) / ∈ {φ(w 1 ), φ(s 1 ), φ(u 2 ), φ(u 4 ), φ(v 4 )} = {a, e, b, d, c}.

Lemma 15. The graph in Figure 23 is a planar subcubic graph of girth 6 with 2-distance chromatic number at least 6.

w 1 u 1 u 2 G = v 2 v 1 x 1 w 2 G = x 2 w ′ 2 G = x ′ 2
Figure 23: A non-5-colorable planar subcubic graph of girth 6.

Proof. One can easily verify that the graph G in Figure 23 is planar, subcubic, and has girth 6. Suppose by contradiction that there exists a 2-distance 5-coloring φ of G. Suppose w.l.o.g. that φ(w 1 ) = a, φ(u 1 ) = b, φ(u 2 ) = c, and

φ(v 1 ) = d. By Lemma 14, φ(v 2 ) = φ(u 2 ) = c due to G = (u 1 , u 2 , v 1 , v 2 ) and φ(x 1 ) = φ(w 1 ) due to G = (w 1 , w 2 , x 1 , x 2 ). Moreover, since φ(x 1 ) / ∈ {φ(v 1 ), φ(v 2 ), φ(u 1 )} = {d, c, b}.
We must have φ(x 1 ) = e. By Lemma 14, we also have φ(w

2 ) = φ(x 2 ) due to G = (w 1 , w 2 , x 1 , x 2 ). Since φ(w 2 ) / ∈ {φ(w 1 ), φ(u 1 )} = {a, b} and φ(x 2 ) / ∈ {φ(v 1 ), φ(x 1 )} = {d, e}, we get φ(w 2 ) = φ(x 2 ) = c. By symmetry, we also get φ(w ′ 2 ) = φ(x ′ 2 ) = c, which is impossible since w 2 sees w ′ 2 .

Generalization of the vertices-to-faces discharging verification algorithm

In Section 3.2, we presented an algorithm (Algorithm 1) that automates the discharging procedure with a given set of reducible configurations. This becomes extremely helpful for proofs where the discharging procedure involve a large case analysis. For the input we efficiently encode a face, the set of reducible configurations, as well as the amount of charge of a vertex depending on its neighborhood. The corresponding computer program was written in Python. The source code and its documentation is publically available on https://gite.lirmm.fr/discharging/planar-graphs. In the case of Theorem 2, the execution time takes few seconds on a standard machine. On the public repository, we also provide another example where we proved the 2-distance 8-choosability of planar graphs with maximum degree 4 and girth at least 7, a result by Cranston et al. in [START_REF] Cranston | Choosability of the square of a planar graph with maximum degree four[END_REF], using a small amount configurations that can be easily reduced (by hand or by computer) and very naive discharging rules. The idea is to move towards a computer automation of proofs using the discharging method.

Our approach can be applied to other problems on planar graphs by concentrating charges on the vertices of the graph when the distribution of charges is made (according to the Euler formula). First, one has to obtain a non-negative sum of charges on the vertices (by realizing an easy discharging procedure for example). This concentrates the difficulty of the problem on the second round of discharging. In this round, one has to redistribute the remaining charge of the vertices to the faces with negative charge and that is where our algorithm can come in handy. Note that the way our algorithm is designed, a vertex can also take charge from a face by giving it a negative charge.

The encoding of a face with a number-word and a letter-word can be done in the same way. In our case, since G has no 2 + -paths, the number-word of a face is composed of integers in {0, 1}. But this alphabet can be extended to {0, 1, . . . , k -1} if G has no k + -paths. Observe that one can partition a face into i-paths (0 ≤ i ≤ k) and consider that each path contains only one endvertex. Therefore, in order to obtain the starting number-words for a face of size d(f ), it suffices to decompose d(f ) into sums where each term corresponds to the number of vertices in an i-path.

As for the letter-words, it suffices to choose a letter for each different neighborhood of interest outside the considered face. In our case, three letters are sufficient but one can always work with a larger alphabet to suit the considered problems. Once the convention for the encoding of a face is fixed, the reducible configurations and entries of the dictionary of charges can be done in the same way.

There are a few details to note about the entries of the dictionary. First, the position of the vertex v holding the charge must be in the center of the entry (or just left of the center). Second, the encoding has to start and end with a number. These properties can be guaranteed by extending the encoding with every possible sequence up to a certain length. Finally, one has to be mindful that v is in the center when the length of the encoding is congruent to 3 modulo 4, and left of the center when it is congruent to 1 modulo 4.

Moreover, we would like to note that, when a discharging procedure along with the given reducible configurations does not prove the desired result, Algorithm 1 returns a sufficient set of missing configurations (to be reduced). This helps to pinpoint the possible difficulty of the proof using discharging. In practice, we started out with a simple discharging procedure. Then, we proceed by reducing the missing configurations returned by Algorithm 1. When there are non-reducible configurations, we further refine our discharging procedure and repeat the process until we reach a sufficient set of discharging rules and reducible configurations. This is how we obtained the configurations in Lemmas 7 to 10. In that sense, Algorithm 1 is not only a tool to verify a proof but also a tool to assist the research process.

We also wanted to prove that subcubic planar graphs with girth at least 11 are 2-distance 5-colorable (which would have improved the non-list version of the result in [START_REF] Borodin | List 2-facial 5-colorability of plane graphs with girth at least 12[END_REF] by Borodin and Ivanova). The computer program returned the problematic configurations which made us realize the difficulty of finding the right discharging rules and reducible configurations. ). Otherwise, we can simply switch the colors of v 3 and v ′ 4 in φ and we can extend this coloring to S by Figure 5 as the remaining colors for v 1 and v 2 would no longer be {c, d} while the remaining colors for v ′ 7 , v 7 , and v 0 stay the same. Thanks to the observations above, we can color these vertices as follow. First, we restrict L(v 5 ) to L(v 5 ) \ {a, b}. Since |L(v 4 )| ≥ 3, we color v 4 with a color different from x and y. Now, we color v 5 , v 6 , v ′ 6 , v ′′ 6 , and v ′′ 6 by Figure 1v. Vertices v 3 and v ′ 4 are colorable since L(v ′ 4 ) = L(v 3 ). If v 3 is not colored c, d, or x, then the number of colors remaining for v ′ 7 , v 7 , v 0 , v 1 , and v 2 are at least 2, 2, 4, 3, and 2 respectively since L(v 1 ) = {c, d, x}. So, S is colorable thanks to Figure 5.

If v 3 is colored c, d, or x, then neither v 3 nor v 4 is colored y. In other words, v 2 has y as an available color while v 1 does not. Thus, v ′ 7 , v 7 , v 0 , v 1 , and v 2 can be colored by Figure 5 as they have at least 2, 2, 4, 2, and 2 remaining colors respectively.

Figure 2 :

 2 Figure 2: A non-colorable path on 3 vertices

  then the graph is 2-distance colorable. Hence the forced lists in Figure3iifollow.Proof ofFigure 4. First, observe that if |L(v 1 )| ≥ 4 or |L(v 2 )| ≥ 4, we can color the other vertices by Figure 1i and finish with v 1 or v 2 respectively. If L(v 4 ) ≥ 4, then we obtain Figure 1iv. Similarly, if |L(v 3 )| ≥ 4, then we obtain Figure 1v. Also note that if |L(v 5 )| ≥ 3, then either v 1 , v 2 , v 3 , v 4 can be colored and we color v 5 last. Or they cannot be colored and by Figure 3ii, we have Figure 4ii.

Lemma 5 .

 5 Graph G has minimum degree at least 2.

.

  Color arbitrarily vertex v ′ 2 and then get Figure 1ii. Proof of Figure 6ii. Direct implication of Figure 1viii. Proof of Figure 6iii. Direct implication of Figure 1vii. Proof of Figure 6iv. To prove this configuration, we redefine the set S to be {v 1 , v 2 , v 3 }. Consider a 2-distance coloring φ of G -S. If φ is extendable to G, then we are done. Thus the available colors of vertices in S correspond to Figure 2. More precisely, L(v 2 ) ⊆ L(v 1 ) = L(v 3 ) = {a, b}. Now, uncolor vertices v 4 , v 5 , v 6 and v ′5 and observe that the numbers of available colors of the non-colored vertices of G are the ones depicted in Figure6iv.Without loss of generality we may assume that φ(v 4 ) = c and φ(v 5 ) = d. Consequently, after the uncoloring of vertices v 4 , v 5 , v 6 and v ′ 5 , we have L(v 3 ) = {a, b, c, d} and L(v 1 ) = {a, b}. If we can choose a color x / ∈ {c, d} for v 4 and color vertices v 5 , v 6 and v ′ 5 , then due to Figure2, we can finish the coloring of v 1 , v 2 and v 3 . Thus, |L(v 5 )| = 3 and the available colors for v 5 , v 6 and v ′ 5 are {x, y, z} ∈ {a, b, c, d, e, f } (again due to Figure2). Note that φ(v 4 ) = c / ∈ {x, y, z}, otherwise φ would not be a valid coloring of G -S. We can assume w.l.o.g that x = d and we color v 4 , v 5 , v 6 , v ′ 5 with c, x, y, z respectively. Finally, due to Figure2we can finish by coloring v 1 , v 2 , v 3 since the lists of available colors for v 1 and v 3 are not the same anymore. Proof of Figure 6v. Direct implication of Figure 1xi. Proof of Figure 6vi. Color v ′ 3 with a color a / ∈ L(v ′′ 3 ), and color v 4 , v 5 in order. Then color vertices

  Figure 1vii and finish by coloring v ′′′ 3 and v ′′ 3 in this order. Proof of Figure 6vii and Figure 6viii. Direct implication of Figure 1xvi for Figure 6viii. As for Figure 6vii, it suffices to see that by adding an imaginary vertex v 6 adjacent to v 5 with any list of colors that verifies |L(v 6 )| ≥ 2, Figure 1xvi gives us a valid coloring for vertices of Figure 6vii.

  v

Figure 6 :

 6 Figure 6: Reducible configurations (Lemma 7).

Figure 7 :

 7 Figure 7: Reducible configuration in Lemma 8

  [START_REF] Hartke | The chromatic number of the square of subcubic planar graphs[END_REF] and note that the number of available colors correspond to what is depicted in Figure7vii. We assume w.l.o.g. that L(v 0 ) = {a, b, c, d, e} where d = φ(v 7 )

Figure 8 :

 8 Figure 8: Reducible configurations in Lemma 9.

Figure 9 :

 9 Figure 9: 1c1a0a1a0a

Figure 10 :

 10 Figure 10: Reducible configurations in Lemma 12.

Figure 18 :

 18 Figure 18: Examples of number-words on 8-faces.

Figure 19 :

 19 Figure 19: Examples of full-words on 8-faces.

  . The encoding of each entry of the dictionary corresponds to a possible neighborhood of a 3-vertex, along with µ * (v) 3 for the worst case scenario in R3 (Figures 11, 12 and 15 to 17) and µ * (v) 2

  fig. 11 fig. 12 fig. 13 fig. 14i fig. 14ii fig. 15 fig. 16 fig. 17 1c1 : 0 1a1 : 0 1a0 : 3 1b0 : 0 0a1c1 : 0 0a0 : 6 0b0 : 4 0b0c1 : 2 1c0 : 0 0c0 : 0 1a0c1 : 0 0a0c1 : 4 1c0a0c1 : 2

Figure 24 :

 24 Figure 24: Reducible cycles.

  v 8 by Figure1ixand finish by coloring v 2 and v 1 in this order. Proof of Figure 8iii. If v ′′ 3 sees v 7 , then they must be at distance exactly 2 since G has girth 8. Say v 8 is their common neighbor, then v ′′ 3 , v ′ 3 , v ′′′ 3 , v 8 , v 7 , v 6 , v ′ 6 form the reducible configuration from Figure 8i. Note that the cases when v ′′′ 3 sees v 7 , or v ′′ 3 sees v ′ 6 , or v ′′ 3 sees v 7 are symmetric. Observe that since v 1 cannot see both v ′ 6 and v 7 , we can assume that v 1 does not see v ′ 6 . Note that in this case |L(v ′

6 )| = 3. Thus we restrict L

Table 1 :

 1 Available amount of charges for each type of 3-vertex after applying R0-R2

	1,1)	fig. 11
	(1,1,0)	fig. 12
	(1,0,0)	fig. 13 fig. 14
	(0,0,0)	fig. 15 fig. 16 fig. 17

Acknowledgements

We would like to thank Mickael Montassier and Alexandre Pinlou for the helpful discussions on earlier versions of this paper. The second author was supported by the French ANR project DISTANCIA: ANR-17-CE40-0015.

L(v 7 ) = {d, e} and x ∈ L(v 3 )\{d, e}, or |L(v 7 )| ≥ 3, both of which means that the remaining configuration is colorable by Lemma 11. • If |L(v 3 ) ∩ L(v 7 )| ≤ 1, then it suffices to show that we can color v 3 , v 4 , v 5 , v 6 , v 7 , v ′ 4 , v ′′ 4 , u ′′ 4 , v 8 , u 8 , v ′ 6 , v ′′ 6 , and u ′′ 6 . Indeed, say they are colorable with φ, then after coloring v ′ 4 , v ′′ 4 , u ′′ 4 , v 8 , u 8 , v ′ 6 , v ′′ 6 , and u ′′ 6 with φ, we obtain the configuration from Figure 7vii where v 3 , v 4 , v 5 , v 6 , and v 7 are colorable (with φ) but |L(v 3 ) ∩ L(v 7 )| ≤ 1, so the whole configuration can be colored.

It remains to show that there exists such a coloring φ. Start by coloring v ′′ 4 such that u ′′ 4 still has 3 colors remaining. Similarly, color v 6 such that v 7 still has 3 colors remaining. Then, color v ′ 6 . Color u ′′ 6 , v ′′ 6 , v 8 , and u 8 by Figure 1i. Finish by coloring v ′ 4 , u ′′ 4 , v 4 , v 3 , v 5 , and v 7 in this order.

Proof of Figure 10ii. If v ′ 1 sees v ′′ 4 , then they must be at distance exactly 2 since G has girth 8. Say v 8 is their common neighbor, then ′′ 4 , and v 8 form the reducible configuration from Figure 7vii. Symmetrically, the same holds if v ′ 1 sees v ′′ 6 . So we have

We redefine S = {v 0 , v 1 , v ′ 1 , v 2 } and let φ be the coloring of the rest of the graph. Now we uncolor the rest of the configuration and we have the corresponding list of colors as in Figure 10ii.

After coloring v ′ 4 , v ′′ 4 , v 8 , v ′′ 6 , and v ′ 6 with φ, the remaining colors for v 3 , v 4 , v 6 , v 7 must be the same two colors, say {d, e} (determined by L(v 1 ) \ L(v ′ 1 )), or the whole configuration would be colorable by Lemma 11. We can also deduce that L(v 3 ) = {d, e, φ(v ′ 4 )}. Similarly, L(v 7 ) = {d, e, φ(v ′ 6 )}. Now, thanks to Lemma 3, we know there exists another coloring φ ′ of v ′ 4 , v ′′ 4 , v 8 , v ′′ 6 , and

). As a result, v 3 , v 4 , v 5 , v 6 , and v 7 is colorable by Figure 5 and L(v 3 ) = {d, e} so the configuration is colorable by Lemma 11.

Proof of Figure 10iii. If v ′

1 sees v ′′ 4 , then they must be at distance exactly 2 since G has girth 8. Say v 8 is their common neighbor, then We redefine S = {v 0 , v 1 , v ′ 1 , v 2 } and let φ be the coloring of the rest of the graph. Now we uncolor v 3 , v 4 , v ′ 4 , v ′′ 4 , v 5 , v 6 , and v 7 and we have the corresponding list of colors as in Figure 10iii. Let {d, e} ⊆ L(v 6 ). If {d, e} ⊆ L(v 3 ), then we color v ′ 4 differently from L(v 3 ) \ {d, e} and color v ′′ 4 . As a result, v 3 , v 4 , v 5 , v 6 , and v 7 are colorable by Figure 5 and L(v 3 ) = {d, e} ⊆ L(v 6 ) so the configuration is colorable by Lemma 11. If {d, e} ⊆ L(v 3 ), then since v 3 , v 4 , v ′ 4 , v ′′ 4 , v 5 , v 6 , and v 7 was colorable with φ, we recolor v ′ 4 and v ′′ 4 with φ(v ′ 4 ) and φ(v ′′ 4 ) respectively. Now, observe that v 3 , v 4 , v 5 , v 6 , and v 7 are colorable but L(v 3 ) = L(v 6 ) so the configuration is colorable by Lemma 11.

Discharging procedure

Charge distribution: For a plane graph G = (V, E, F ), Euler formula |V | -|E| + |F | = 2 can be rewritten as [START_REF] Appel | Every planar map is four colorable. part I. discharging[END_REF] v∈V (G)

We assign to each vertex v the charge µ(v) = 7 2 d(v) -9 and to each face f the charge µ(f ) = d(f ) -9. To prove the non-existence of G, we will redistribute the charges preserving their sum and obtaining a non-negative total charge, which will contradict Equation [START_REF] Appel | Every planar map is four colorable. part I. discharging[END_REF].

To do so, we will divide the discharging procedure into two rounds. In the first round, we will redistribute the charges only between the vertices of G, resulting in a non-negative amount of charge on each vertex using the properties proved in Lemmas 7 and 9. For the second round, first observe that µ(f ) = d(f ) -9 ≥ 0 for every face of size at least 9. Therefore, since g(G) ≥ 8 and µ(f ) = -1 for every 8-face, we will redistribute the remaining charges on each vertex over the non-reducible 8-faces (every reducible cycle is shown inLemma 10)

We show that after applying R5, we get µ * (f ) ≥ 0 and µ * (f ′ ) ≥ 0. Recall that 8-faces have starting charge -1.

First of all, by Figure 13 and R4, if f ′ is not an 8-face, then v 4 and v 6 each give 1 2 to f . So,

If f ′ is an 8-face, then v 4 and v 6 each give 1 4 to f by Figure 13 and R4, and f ′ gives f 1 2 by R5. Thus,

By Figure 10iii, v ′′ 4 cannot be a 2-vertex so it must be a 3-vertex. Symmetrically, v ′′ 6 must also be a 3-vertex. By Figure 10ii, v 8 must also be a

• If u ′′ 4 and u ′′ 6 are 2-vertices, then u 8 must be a 3-vertex by Figure 10i. In that case, v 8 gives at least

To conclude, we started with a negative total amount of charge on the vertices and faces of G by Equation (1) and after our discharging procedures, which preserve the total amount of charge, we ended up with a non-negative amount of charge on each vertex and face of G. This is a contradiction, so G does not exists and this ends the proof of Theorem 2.

Discussion on Theorem 2

The discharging method is commonly used on planar graphs, very often because of their sparseness. Sometimes, the planarity of the graph is not needed, in which case the proofs hold for more general classes of sparse graphs (for example, graphs with bounded maximum average degree mad(G) = max H⊆G

2|E(H)|

|V (H)| ). This was the case for the proof of Theorem 1 for example. However, when we increase the density of the graph by decreasing the girth of the planar graph or by increasing the maximum average degree, the result might hold for one case but not the other. In particular, the smallest class of graphs of bounded mad that contains planar graphs with girth at least g has mad < 2g g-2

, and v ′′′ 6 in this order.

Proof of Figure 24iv. If v ′ 7 sees v ′ 3 , then they must be at distance exactly 2 since G has girth 8.

, and v ′ 3 form the reducible configuration from Figure 8i. Similarly, the same holds when v

, then they must be at distance exactly 2 since G has girth 8. Say v 8 is their common neighbor,

, and v ′ 7 form the reducible configuration from Figure 8i. Similarly, the same holds when

, then they must be at distance exactly 2 since G has girth 8.

, and v ′′ 6 form the reducible configuration from Figure 7v. Similarly, the same holds when v

, and v ′′′ 6 form the reducible configuration from Figure 7vi. Similarly, the same holds when

. By the pigeonhole principle, we can color v 1 and v ′ 7 with the same color since we have six colors in total. We finish by coloring

, then they must be at distance exactly 2 since G has girth 8.

, and v ′ 6 form the reducible configuration from Figure 7i. By symmetry the same holds when v ′ 3 sees v ′′′ 6 . Thus, we have

), and afterwards color v 5 with y / ∈ L(v ′ 5 ). We finish by coloring the remaining vertices in the following order: 1vii and finish by coloring v 3 and v ′ 4 in this order.

Proof of Figure 24vii.

Here, we redefine

2 ) or we could have switched their colors in φ and d would be an available color for v 4 and we could extend φ to G. Now, we color v 2 and v 6 with colors not in {d, e}. Then, we color v ′ 7 , v 7 , v 0 , v 1 by Figure 1i. Color v ′ 2 and v 3 greedily, which is possible since L(v ′

2 ) = L(v 3 ). Finally, since at least d or e is available for v 4 and d, e / ∈ L(v ′ 5 ), by Figure 2, we can color v 4 , v 5 , v ′ 5 .

Proof of Figure 24viii.

. Observe that it is always possible to color v 1 , v 2 and v 7 such that afterwards v 0 has at least two available colors. Indeed, either v 2 and v 7 can be colored with the same color, or 1ix and finish by coloring v 0 . Proof of Figure 24ix.

. We prove first the following observations.

• L(v 3 ) = {a, b, c} and L(v 7 ) = {d, e, f }. Suppose to the contrary that we can color v 3 and v 7 with the same color. Then color v 0 with x such that

by Figure 1x and finish by coloring v 2 , v 1 in this order.

• Observe that vertices v 3 and v 7 are symmetric and thus by pigeonhole principle w.l.o.g. we have {a, b} ⊂ L(v 1 ). 1x and finish by coloring 1xvi. Finish by coloring v 2 , v 0 in this order.

By the last item, w.l.o.g. we can assume that |L(v 0 ) \ {d, e}| ≥ 4. Thus we restrict L(v 7 ) to {d, e}.

then the are at distance exactly 2 and share a common neighbor, say v 8 .

, then they must be at distance exactly 2 since G has girth 8.

5 and v 6 form the reducible configuration from Figure 7ii. The same holds when 1viii and finish by coloring v ′ 4 . Proof of Figure 24xiii. If v ′ 1 sees v ′ 5 , then they must be at distance exactly 2 since G has girth 8.

, then they must be at distance exactly 2 since G has girth 8 and say v 8 is their common neighbor. Then

Without loss of generality φ(v 3 ) = d and φ(v 7 ) = e. Now observe that the color of v 3 was chosen arbitrarily, thus there exists a similar coloring φ ′ where φ ′ (v 3 ) = d. Moreover, using again Figure 3, φ ′ (v 3 ) = e. Thus we deduce that

With all the remarks of the previous paragraphs, we give a coloring of the configuration: restrict L(v 6 ) to L(v 6 ) \ {d, e} and restrict L(v 5 ) to L(v 5 ) \ {d, e}. Then color v ′′ 6 , v ′ 6 , v ′′′ 6 , v 7 , v 5 by Figure 1vii and color v ′ 5 , v 4 , v 3 in this order. Recall that v 6 was colored x / ∈ {d, e}. Thus the list of remaining available colors for v 0 is not {a, b, c} = L(v ′ 1 ) and hence by Figure 3 we are done. Proof of Figure 24xiv. If v ′′ 4 sees v ′ 1 , then they must be at distance exactly 2 since G has girth 8.

and take a coloring φ of G -S. By Figure 3 we

= {a, b, c} and the colors of v ′ 6 and v 7 cannot be interchanged. Having that said, we uncolor vertices

6 and v 7 and the number of available colors for each vertex correspond to the numbers depicted on Figure 24xiv. We know now that L(v 0 ) = {a, b, c, φ(v 6 ), φ(v 7 )} and furthermore L(v ′ 6 ) = L(v 7 ). We color v 6 with x / ∈ {phi(v 6 ), φ(v 7 )} and v ′′ 4 , v ′ 4 , v ′′′ 4 , v 4 , v 3 , v 5 by Figure 1v. Then we color v ′ 6 and v 7 since

) and thus by Figure 3 we are done. Proof of Figure 24xv.

Suppose v ′′ 5 sees v ′ 1 . By Lemma 6 they are at distance exactly two and therefore

By pigeonhole principle we color vertices v 0 and v 4 with the same color x and show the following:

If not then we color v ′ 6 with x as well and finish by coloring

If not then we color v ′ 6 arbitrarily and finish by coloring

If not then we color v ′ 6 arbitrarily and finish by coloring

We recolor the whole configuration as follows. Color v 3 and v 6 with x, then color v 4 . Color v 5 such that vertex v 7 has at least two available colors left.

Take a coloring φ of G -S. If vertices of S are colorable, then we are done. Hence by using Figure 3 we uncolor vertices v 3 , v 4 , v 5 , v ′ 5 , v ′′ 5 , v ′′′ 5 , v 6 , v ′ 6 , v 7 and conclude that after uncoloring

as their color could be permuted and φ could be extended to S.

Without loss of generality φ(v 6 ) = d and φ(v 7 ) = e. Now one could restrict L(v 6 ) to L(v 6 ) \ {d}, and give another coloring φ ′ of G -S where first vertices v ′′ 5 , v ′ 5 , v ′′′ 5 , v 5 , v 6 , v 3 , v 4 are colored using Figure 1viii and then since L(v ′ 6 ) = L(v 7 ), vertices v ′ 6 and v 7 are colored greedily. Note that since φ ′ (v 6 ) = d, using again Figure 3, we necessarily have φ ′ (v 6 ) = e. Thus we deduce

With all the remarks of the previous paragraphs, we give a coloring of the configuration: restrict

) and that v 5 and v 4 were colored with colors other than x and y. Therefore we color vertices v 6 , v ′ 6 , v 7 in this order. Recall that v 6 was colored say x / ∈ {d, e}. Thus the list of remaining available colors for v 0 is not {a, b, c} = L(v ′ 1 ) and hence by Figure 3 we are done.

3 in this order. Note that this coloring procedure works even when v ′′ 3 (resp.

, then they must be at distance exactly 2 since G has girth 8.

, then they must be at distance exactly 2 since G has girth 8. Say v 8 is their common neighbor,

7 in this order. Note that this coloring procedure works even when v 0 sees v ′′ 4 or v ′′′ 4 . Proof of Figure 24xviii. If v ′ 3 sees v ′ 7 , then they must be at distance exactly 2 since G has girth 8.

5 by Figure 1viii and finish by coloring v ′ 7 . Note that this coloring procedure works even when v

, then they must be at distance exactly 2 since G has girth 8.

5 by Figure 1viii and finish by coloring v ′ 7 . Note that this coloring procedure works even when v ′ 2 (resp. v ′ 3 ) sees v ′′ 6 or v ′′′ 6 at distance 2 since there are no 2-paths due to Lemma 6 (resp. since G has girth at least 8). Proof of Figure 24xix. If v ′′ 2 sees v ′ 7 , then they must be at distance exactly 2 since G has girth 8.

, then they must be at distance exactly 2 since G has girth 8. Say v 8 is their common neighbor,

6 in this order. Note that this coloring procedure works even when v ′ 3 sees v ′ 7 . Proof of Figure 24xx. Between v ′′ 3 and v ′′′ 3 , there always exists one vertex that does not see v

2 ), then, by pigeonhole principle, color v 2 and v 6 with the same color. Restrict L(v 3 ) to

2 ). Finish by coloring v 7 , v ′ 7 and v 0 in this order. Note that this coloring procedure works even when v ′′′ 3 sees v ′ 7 (at distance 2 since there are no 2-paths by Lemma 6).

Proof of Figure 24xxi. Between v ′′ 7 and v ′′′ 7 , there always exists on vertex that does not see v ′ 3 , say v ′′ 7 . Color v ′ 7 with a color not in v ′′ 7 . Color v 2 with a color such that v ′ 3 still retains three available colors. Color v 0 such that v 6 still retain two available colors. Color v 1 and v ′ 2 greedily. Color 1viii. Finish by coloring v ′ 3 , v ′′′ 7 and v ′′ 7 in this order. Note that this coloring procedure works even when v ′′ 7 (resp.

4 and v ′′′ 4 , there always exists one vertex that does not see v 1vii. Finish by coloring v ′′′ 4 , v ′′ 4 , v 0 and v ′ 7 in this order. Note that this coloring procedure works even when v ′′′ 4 sees v ′ 7 (at distance 2 since G has girth at least 8).

in this order. Note that this coloring procedure works even when v ′′ 3 (resp. v ′′′ 3 ) sees v ′ 6 or v 7 , and when v ′ 2 sees v ′ 6 . Proof of Figure 24xxiv. Note that there always exists x ∈ L(v ′′ 4 ) ∩ L(v ′ 4 ). We start by showing the following observations: 4 or φ would be extendable to G. We uncolor ). Now, observe that v 6 must still be colored d or by Figure 4, we can extend this coloring. However, we know that v 1 and v 5 are not colored e, thus e is still an available color for v 7 . By Figure 4, S is colorable.

Proof of Figure 24xxvii. If v ′′

5 sees v ′ 2 , then they must be at distance exactly 2 since G has girth 8.

form the reducible configuration from Figure 7i. Symmetrically, the same holds when v ′′′ 5 sees v ′ 2 . Between v ′′ 5 and v ′′′ 5 , there always exists one vertex that does not see v 1 , say v ′′ 5 . We restrict L(v 5 ) to L(v 5 ) \ L(v ′′ 5 ). There exists a color x ∈ L(v 2 ) \ L(v ′ 2 ), we restrict L(v 4 ) to L(v 4 ) \ {x}. We color v 4 , v 5 , v 6 , v ′ 6 , v 7 by Figure 1v. Then, we color v ′ 5 , v ′′′ 5 , v ′′ 5 in this order. Now, observe that by Figure 4, we can color v 0 , v 1 , v 2 , v ′ 2 , v 3 since x is an available color for v 2 but not v ′ 2 . Note that this coloring procedure works even when v ′′′ 5 sees v 1 .

Proof of Figure 24xxviii. If v ′′ 6 sees v ′ 2 , then they must be at distance exactly two since there are no 2-path by Lemma 6. We restrict

in this order. Symmetrically, the same holds when v ′′′ 6 sees v ′ 2 . There exists a color

). We color v 7 , v 6 , v 5 , v ′ 5 , v 4 by Figure 1v. Then, we color v ′ 6 , v ′′′ 6 , v ′′ 6 in this order. Now, observe that by Figure 4, we can color v

form the reducible configuration from Figure 24vi. Symmetrically, the same holds when v

and consider φ a coloring of G -S. Note that the lists of available colors of vertices of S correspond to Figure 4 as otherwise φ would be extendable to G. We uncolor sees v ′′ 6 , then they share a common neighbor v 8 and v ′′ 6 , v 8 , v ′ 3 , v 3 , v 4 , v 5 , v 6 , v ′ 6 form the reducible configuration from Figure 7i. Symmetrically, the same holds when v ′ 3 sees v ′′′ 6 . If v 2 sees v ′′ 6 , then they must be at distance exactly 2. Note that, in this case, |L(v 2 )| ≥ 3 so we can color v 2 then v 3 such that v 1 retains at least 2 available colors. We color v ′ 6 with x / ∈ L(v ′′ 6 ). Then, we color v ′ 3 , v 5 , v 4 in this order. Afterwards, we color v 1 , v 0 , v 7 , v ′ 7 and v 6 by Figure 1iv. Finish by coloring v ′′′ 6 then v ′′ 6 in this order. Symmetrically, the same holds when v 2 sees v ′′′ 6 . So we have G[S] 2 = G 2 [S]. Observe that in the previous case, it suffices to color v 2 such that v 1 still retain at least 2 available colors to be able to extend the coloring to G. Thus, L(v 2 ) = L(v 1 ) = {a, b}. Now, if a ∈ L(v ′ 3 ), then we color v ′ 3 and v 1 with a. Restrict L(v 6 ) to L = L(v 6 ) \ L(v ′′ 6 ). Color v ′ 7 with v / ∈ L. Then, we color v 0 , v 7 , v 6 , v 5 , v 4 , v 3 with Figure 1iii. and finish by coloring v ′ 6 , v ′′′ 6 and v ′′ 6 in this order. If a / ∈ L(v ′ 3), color v 2 with a. By pigeonhole principle, we color v ′ 6 and v ′ 7 with the same color. Then, we color v ′′ 6 and v ′′′ 6 greedily. Afterwards, we color v 5 , v 6 , v 7 , v 0 by Figure 1i. We finish by coloring v 3 , v 4 , v ′ 3 in this order.