# Five Color Theorem

This article needs to be linked to other articles.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{MissingLinks}}` from the code. |

## Theorem

A planar graph $G$ can be assigned a proper vertex $k$-coloring such that $k \le 5$.

## Proof

The proof proceeds by the Principle of Mathematical Induction on the number of vertices.

For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:

- $G_n$ can be assigned a proper vertex $k$-coloring such that $k \le 5$.

### Basis for the Induction

$\map P r$ is trivially true for $1 \le r \le 5$, as there are no more than $5$ vertices to be colored.

This is our basis for the induction.

### Induction Hypothesis

Now we need to show that, if $\map P r$ is true, where $r \ge 5$, then it logically follows that $\map P {r + 1}$ is true.

So this is our induction hypothesis:

- $G_r$ can be assigned a proper vertex $k$-coloring such that $k \le 5$.

Then we need to show:

- $G_{r + 1}$ can be assigned a proper vertex $k$-coloring such that $k \le 5$.

### Induction Step

This is our induction step:

According to the Minimum Degree Bound for Simple Planar Graph, $G_{r + 1}$ has at least one vertex with at most $5$ edges.

- Let this vertex be labeled $x$.

Remove vertex $x$ from $G_{r + 1}$ to create another graph, $G'_r$.

By the induction hypothesis, $G'_r$ is five-colorable.

Suppose all five colors were not connected to $x$.

Then we can give $x$ the missing color and thus five-color $G_{r + 1}$.

Suppose all five colors are connected to $x$.

Then examine the five vertices $x$ was adjacent to.

Call them $y_1, y_2, y_3, y_4$ and $y_5$ in clockwise order around $x$.

Let $y_1, y_2, y_3, y_4$ and $y_5$ be colored respectively by colors $c_1, c_2, c_3, c_4$ and $c_5$.

Let us denote $H_{i, j}$ a subgraph of $G'_r$ induced by the vertices colored with $c_i$ and $c_j$.

Consider $H_{1, 3}$.

Suppose there exists no path between $y_1$ and $y_3$ in $H_{1, 3}$.

Thus, $H_{1, 3}$ is disconnected into two components.

We can, then, interchange the colors $c_1$ and $c_3$ in the component that is connected to $y_1$.

Thus $x$ is no longer adjacent to a vertex of color $c_1$, so $x$ can be colored $c_1$.

Suppose there exists a path between $y_1$ and $y_3$ in $H_{1, 3}$.

Including the vertex $x$ in this path we get a circuit $C$.

Since we indexed the vertices $y_1, y_2, y_3, y_4$ and $y_5$ clockwise, exactly one of the vertices $y_2$ and $y_4$ is inside $C$.

Hence, $y_2$ and $y_4$ are in different connected components of $H_{2, 4}$

Then we can switch colors $c_2$ and $c_4$ in the component of $H_{2, 4}$ that is connected to $y_2$.

Now $x$ is no longer adjacent to a vertex of color $c_2$, so we can color it $c_2$.

This graph illustrates the case in which the path from $y_1$ to $y_3$ can be completed.

- $\text{Blue} = c_1, \text{Yellow} = c_2, \text{Red} = c_3, \text{Green} = c_4, \text{Turquoise} = c_5$.

The dotted lines represent edges and vertices that might exist, as this is simply a fairly minimal example graph that matches the conditions.

So $\map P r \implies \map P {r + 1}$ and the result follows by the Principle of Mathematical Induction.

Therefore:

- For all $n \in \N_{>0}$, $G_n$ can be assigned a proper vertex $k$-coloring such that $k \le 5$.

## Also known as

This theorem is also known as **Heawoodâ€™s Theorem**, for Percy John Heawood, although **The Five-Color Theorem** is more widely used.

The British English spelling of this proof is **five colour theorem**.

## Also see

This page has been identified as a candidate for refactoring of medium complexity.In particular: It would be good to extract that algorithm into its own page, and then link to it from here.Until this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

- The proof gives a simple (recursive) algorithm for $5$-coloring a planar graph, the so-called
**Heawood's Algorithm.**

## Historical Note

The Five Color Theorem is not the strongest result possible.

It was proved by Percy John Heawood in $1890$.

In the same year he showed a flaw in Alfred Bray Kempe's supposed $1879$ proof of the Four Color Theorem which was not mended for almost another $100$ years.

It was not until $1976$ that Kenneth Ira Appel and Wolfgang Haken demonstrated that four colors suffice.

Their proof relies heavily on computers and for the moment is not to be found on $\mathsf{Pr} \infty \mathsf{fWiki}$.