$$\newcommand{\tsf}[1]{{\sf{#1}}} \newcommand{\lb}{\left<} \newcommand{\rb}{\right>} \newcommand{\pair}[1]{\lb #1 \rb} \newcommand{\BB}{\mathbb{B}} \newcommand{\RR}{\mathbb{R}} \newcommand{\Pow}{\tsf{Pow}} \newcommand{\List}{\tsf{List}} \newcommand{\TwoPow}[1]{2^{#1}} \renewcommand{\implies}{⇒} \newcommand{\pto}{\to_{\text{?}}}$$

5 color theorem


Sort Node - Is ℚ², i.e. we identify nodes with the points on the rational plane.
Sort Color - The set {1,2,3,4,5}
Sort Defn Coloring := PartialFn(Node, Color)
Sort Map
A planar map, i.e. an embedding of a planar graph in the plane, where the nodes of a map are elements of Node, and the edges of a map are piecewise-linear curves connecting one node to another. Whether a node has an edge to another node is determined by the function neighbours introduced below. The curves (the embeddings of edges) do not intersect (unless of course they share an endpoint, in which case they intersect at that point only). We must also assume that no three nodes are colinear, since otherwise Claim 9 can be false.


5-coloring : Coloring × Map → 𝔹
5-coloring(σ,G) holds iff σ is a 5-coloring of G, meaning that it is defined on each node of G, and if u,v are nodes of G with v ∈ neighbours(u), then σ(u) ≠ σ(v).
Defn 5-colorable : Map → 𝔹 - The nodes of the given map can be colored with 5 colors in such a way that no two adjacent nodes have the same color.
5-colorable(G) ⇔ ∃σ:Coloring. 5-coloring(σ,G)

$\tsf{Theorem}$: Every planar graph is 5-colorable
∀G:Map. 5-colorable(G)
Defn IH : ℕ → 𝔹 - IH(n) ⇔ ∀G:Map. #nodes(G) = n ⇒ 5-colorable(G)
Defn ‹extendable to a 5-coloring of› : Coloring × Map → 𝔹 - σ is extendable to a 5-coloring of G iff σ is a 5-coloring of the graph obtained by deleting a node u, and there is a color c that we can color u with to make a full 5-coloring of G, because none of the neighbours of u are colored c.
‹extendable to a 5-coloring of›(σ,G) ⇔ ∃u:Node. ∃c:Color. u ∈ nodes(G) ∧ 5-coloring(σ,G-u) ∧ c ∉ σ(neighbours(u,G))
Claim 1: IH(0) ∧ IH(1) ∧ (∀n:ℕ. n≥2 ∧ IH(n-1) ⇒ IH(n)) ⇒ $\tsf{Theorem}$
Claim 2: IH(0) ∧ IH(1)
Lemma 1: ∀n:ℕ. n≥2 ∧ IH(n-1) ⇒ IH(n)
Let n : ℕ be arbitrary
Assume n ≥ 2 ∧ IH(n-1)
Lemma 2: IH(n)
connected : {Node × Node × Map → 𝔹, Map → 𝔹}
When there are three argument: means two nodes are connected in the given map. When there is one argument: means each pair of nodes in the map is connected.
Let G : Map be arbitrary
Assume #nodes(G) = n
Claim 3: ¬connected(G) ⇒ 5-colorable(G)
Assume connected(G)
Claim 4: mindegree(G) < 5 ⇒ 5-colorable(G)
Claim 5: #edges(G) < 3 ⇒ 5-colorable(G)
Lemma 3: mindegree(G) ≥ 5 ∧ #edges(G) ≥ 3 ⇒ 5-colorable(G)
Assume mindegree(G) ≥ 5 ∧ #edges(G) ≥ 3
Lemma 4: G has a node of degree exactly 5.
∃v:Node. v ∈ nodes(G) ∧ degree(v,G) = 5
Let v : Node be a witness for the previous sentence.
Defn G' : Map - G - v
Assertion 1: 5-colorable(G') by IH(n-1)
Let σ : Coloring be a witness for the previous sentence.
Defn $C_{\text{v}}$ : FiniteSet(Color) - σ(neighbours(v,G))
Assertion 2: |$C_{\text{v}}$| < 5 ⇒ ‹extendable to a 5-coloring of›(σ,G) since then there is a color not in $C_{\text{v}}$ that we can use to color v.
Assertion 3: |$C_{\text{v}}$| < 5 ∨ |$C_{\text{v}}$| = 5 since |$C_{\text{v}}$| ≤ degree(v,G) = 5.
Lemma 5: |$C_{\text{v}}$| = 5 ⇒ 5-colorable(G)
Assume |$C_{\text{v}}$| = 5
‹clockwise around› : Node⁵ × Node → 𝔹
‹clockwise around›(u₁,u₂,u₃,u₄,u₅,v) is true iff the 6 nodes are distinct, and the 5 ordered nodes u₁,u₂,u₃,u₄,u₅ are arranged clockwise around v in the following sense. Draw 5 rays starting from v and going through each uᵢ. Then none of the rays intersect except at v. Starting at u₁ and moving clockwise around the circle centered at v and intersecting u₁, your path will intersect the rays of u₁,u₂,u₃,u₄,u₅ in that order.
‹color submap› : Map × Coloring × Color × Color ⤏ Map
‹color submap›(G, σ, c₁, c₂) is the submap obtained by deleting all nodes in G whose color according to σ is not c₁ or c₂. It is defined iff σ is defined on every node of G.
Claim 9: ∃u₁,u₂,u₃,u₄,u₅:Node. ‹clockwise around›(u₁,u₂,u₃,u₄,u₅,v) ∧ {u₁,u₂,u₃,u₄,u₅} = neighbours(v,G)
Let u₁,u₂,u₃,u₄,u₅ : Node be a witness for the previous sentence.
c₁, c₂, c₃, c₄, c₅ : Color - Define $c_i$ := σ($u_i$)
Defn $G'_{13}$ : Map - ‹color submap›(G',σ, c₁, c₃})
swap : Coloring × Color × Color × Map × Map ⤏ Coloring
swap(σ, c₁, c₂, G, G') is defined iff G' is a submap of G and σ is defined on every node of G. When defined it is the (not necessarily proper) coloring function obtained from σ by swapping c₁ and c₂ in nodes(G').
component : Node × Map → Map
component(u,G) is the empty map if u is not in nodes(G), and otherwise it is the subgraph of G obtained by deleting all the nodes not reachable from u.
Defn ‹component of› : Map × Map → 𝔹 - component(G',G) is true iff G' is one of the connected components of G, i.e. it is a maximal subgraph of G in which all the nodes are connected by paths.
‹component of›(H,G) ⇔f ∃u:Node. u ∈ nodes(G) ∧ H = component(u,G)
Kempke Chains Lemma: Let I be a Map and τ a 5-coloring of I. Let d₁,d₂ be distinct colors, and let I' be a component of ‹color submap›(I,τ,d₁,d₂). Then the coloring τ' = swap(τ, d₁, d₂, I, I') is also a 5-coloring of I.
∀I,I':Map. ∀d₁≠d₂:Color. ∀τ,τ':Coloring. 5-coloring(τ,I) ∧ ‹component of›(I',I) ∧ τ' = swap(τ, d₁, d₂, I, I') ⇒ 5-coloring(τ' ,I)
Lemma 6: ¬connected(u₁,u₃,$G'_{13}$) ⇒ 5-colorable(G)
Lemma 7: connected(u₁,u₃,$G'_{13}$) ⇒ 5-colorable(G)