%% filename: amsart-template.tex
%% American Mathematical Society
%% AMS-LaTeX v.2 template for use with amsart
%% ====================================================================

\documentclass{amsart}

\usepackage{amssymb}
\usepackage{graphicx}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{algorithm}[theorem]{Algorithm}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\numberwithin{equation}{section}

\begin{document}

\title{Face-Monochromatic Pairs and the Four Colour Theorem}

%    author one information
\author{Eric Bauerfeld}
\address{}
\curraddr{}
\email{}
\thanks{}

\subjclass[2010]{Primary }

\keywords{four colour theorem, plane triangulation, dual graph, cubic planar
graph, edge connectivity, cyclic edge cut, Tait colouring, $3$-edge-colouring}

\date{}

\dedicatory{}

\begin{abstract}
We propose the \emph{face-monochromatic-pair conjecture}, a structural
property of proper $3$-edge-colourings of cubic plane graphs that, if
true, implies the Four Colour Theorem. Working in the planar dual $G'$ of
a hypothetical minimal counterexample $G$ to 4CT, we delete a single
pentagonal face of $G'$ and rewire its five external vertices around a
new apex vertex and a chord; the resulting \emph{reduced dual}
$\widehat{G}'_{v,i}$ is a smaller cubic plane graph whose proper
$3$-edge-colourings, by the minimality of $G$, are constrained by a
chord-apex condition and a pair of Kempe-cycle conditions. The
face-monochromatic-pair conjecture, in its strengthened form, asserts the
existence in every such colouring of a face $F$ and two non-incident
same-coloured edges $e_1, e_2 \in \partial F$ whose subdivision-and-%
bridging produces a $4$-face $f_n$ whose boundary colouring places it
under the hypothesis of a $4$-face edge-suppression theorem; we use this
theorem to derive a proper $3$-edge-colouring of $G'$, contradicting
minimality. We verify the conjecture computationally on all
chord-apex+Kempe colourings of reduced duals with $|V(G)| \leq 20$
($142{,}812$ colourings, all pass); the weaker form is verified up to
$|V(G)| \leq 21$ ($535{,}182$ colourings, all pass).
\end{abstract}

\maketitle

\section{Introduction}
\label{sec:intro}

The Four Colour Theorem (4CT) --- that every loopless plane graph admits a
proper $4$-vertex-colouring --- has, since the late 1970s, only been proved
by computer-assisted case analysis on a discharging argument over a finite
set of unavoidable reducible configurations. Appel and Haken's original
proof~\cite{AH77a, AHK77}, the Robertson--Sanders--Seymour--Thomas
reworking~\cite{RSST97}, and Gonthier's machine-checked
version~\cite{Gonthier08} all share that structure.

This paper takes a different approach: rather than discharge over
configurations in the triangulation $G$, we work in its planar dual $G'$,
a cubic plane graph whose proper $3$-edge-colourings correspond by Tait's
theorem to proper $4$-vertex-colourings of $G$. Assuming $G$ is a minimal
counterexample to 4CT, we delete a single pentagonal face of $G'$ and
rewire its five external vertices, obtaining a smaller cubic plane graph
$\widehat{G}'_{v,i}$ --- the \emph{reduced dual} --- which by minimality
\emph{is} properly $3$-edge-colourable. Two structural lemmas constrain
every such colouring: a \emph{chord-apex} condition (Lemma~\ref{lem:chord-apex})
forcing two named edges to share a colour, and a pair of
\emph{Kempe-cycle} conditions (Lemma~\ref{lem:kempe-spike}) placing four
of the rewired edges on common bichromatic Kempe cycles. These constraints
are the starting point of the present development.

The main contribution of the paper is the
\emph{face-monochromatic-pair conjecture}
(Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}) and
its strengthening
(Conjecture~\ref{conj:face-monochromatic-pair-strengthened}), which we
show together imply the Four Colour Theorem. The supporting ingredients
are the chord-apex and Kempe-cycle lemmas on reduced-dual colourings, the
classical operation of \emph{edge suppression} (delete the edge and smooth
its two degree-$2$ endpoints; equivalently, simple-graph contraction in
the dual triangulation; recalled in Section~\ref{sec:edge-suppression}),
and an observation that suppression preserves $3$-edge-colourability when
applied across a $4$-face whose two opposite boundary edges carry
different colours (Theorem~\ref{thm:edge-suppression-4face}).

The strategy is to construct, from a putative minimal counterexample's
reduced-dual colouring, a $4$-face $f_n$ in a slightly modified graph
$\widehat{G}'^{+}$ to which the suppression theorem applies; the
suppression then produces a properly $3$-edge-coloured graph from which a
$3$-edge-colouring of $G'$ can be recovered, contradicting the
non-$4$-colourability of $G$. The face-monochromatic-pair conjecture
asserts the existence of the structural data ($F, e_1, e_2$) needed to
build $f_n$; the strengthening guarantees that $f_n$'s boundary colouring
falls under the suppression theorem's hypothesis. Both conjectures have
been verified computationally on all chord-apex+Kempe colourings of
reduced duals up to $|V(G)| \leq 20$, with the weaker form going up to
$|V(G)| \leq 21$.

\paragraph{Organization.} Section~\ref{sec:minimal} fixes the
minimal-counterexample framework: $G$ is a triangulation,
$\delta(G) \geq 5$, and every triangulation on fewer vertices is properly
$4$-colourable. Section~\ref{sec:reduced-dual} introduces the reduced dual
$\widehat{G}'_{v,i}$ and proves the chord-apex and Kempe-cycle lemmas.
Section~\ref{sec:edge-suppression} defines edge suppression and proves
its $4$-face $3$-edge-colourability theorem.
Section~\ref{sec:toward-4ct} states the two conjectures, reports the
empirical verification, and gives the implication to 4CT.

\paragraph{Companion paper.} An iterated version of the reduced-dual
construction --- producing a sequence $H_1, H_2, \dots$ of progressively
smaller cubic plane graphs and tracking an accumulating ``protected'' edge
set --- is the subject of a companion paper. The present paper does not
use that iteration.

\section{The minimal counterexample}
\label{sec:minimal}

Throughout, a \emph{triangulation} is a simple plane graph, with a fixed
embedding, in which every face --- including the outer face --- is bounded by a
triangle. We first reduce to triangulations, then record the degree properties a
smallest counterexample must have.

\begin{lemma}[Reduction to triangulations]
\label{lem:triangulate}
If every triangulation is properly $4$-vertex-colourable, then so is every plane
graph.
\end{lemma}

\begin{proof}
Let $H$ be a plane graph. Add edges to $H$, maintaining planarity, until no
further edge can be added; the result is a triangulation $H^{+}$ on the same
vertex set with $E(H) \subseteq E(H^{+})$. A proper $4$-colouring of $H^{+}$
restricts to a proper $4$-colouring of $H$, since every edge of $H$ is an edge of
$H^{+}$.
\end{proof}

By Lemma~\ref{lem:triangulate}, if the Four Colour Theorem fails then it fails for
some triangulation. We may therefore make the following assumption.

\begin{definition}[Minimal counterexample]
\label{def:minimal}
Let $G$ be a triangulation on the fewest vertices that admits no proper
$4$-vertex-colouring. We call $G$ a \emph{minimal counterexample}. By minimality,
every triangulation on fewer than $|V(G)|$ vertices is properly
$4$-colourable.
\end{definition}

\begin{remark}
Since every triangulation on at most four vertices is properly $4$-colourable
(the largest being $K_4$), a minimal counterexample has $|V(G)| \ge 5$; the degree
bound below sharpens this to $|V(G)| \ge 12$.
\end{remark}

\begin{lemma}[Minimum degree]
\label{lem:mindeg}
A minimal counterexample $G$ has minimum degree $\delta(G) \ge 5$.
\end{lemma}

\begin{proof}
Suppose some vertex $v$ has $\deg(v) = d \le 4$.

If $d \le 3$, let $G' = G - v$. Then $G'$ is a plane graph on fewer vertices, so
by Definition~\ref{def:minimal} and Lemma~\ref{lem:triangulate} it has a proper
$4$-colouring. The at most three neighbours of $v$ use at most three colours, so
a fourth colour is free for $v$, extending the colouring to $G$ --- a
contradiction.

If $d = 4$, again $4$-colour $G - v$. If the four neighbours of $v$ use at most
three colours we extend as before, so assume they receive all four colours; let
$v_1, v_2, v_3, v_4$ be the neighbours in cyclic order around $v$, coloured
$1,2,3,4$. Consider the subgraph induced by the colour classes $1$ and $3$, and
let $K$ be its connected component containing $v_1$. If $v_3 \notin K$, swap
colours $1$ and $3$ on $K$; now no neighbour of $v$ is coloured $1$, freeing it
for $v$. If $v_3 \in K$, then a $1$--$3$ Kempe chain joins $v_1$ to $v_3$, and
this chain together with $v$ encloses exactly one of $v_2, v_4$; hence the
$2$--$4$ component containing $v_2$ cannot also reach $v_4$, and swapping colours
$2$ and $4$ on it frees colour $2$ for $v$. Either way the colouring extends to
$G$, a contradiction.

Hence $\delta(G) \ge 5$.
\end{proof}

\section{The reduced dual}
\label{sec:reduced-dual}

Write $G'$ for the dual of $G$: since $G$ is a triangulation, $G'$ is a cubic
plane graph in which each vertex of $G$ corresponds to a face of $G'$, each face
of $G$ to a vertex of $G'$, and each edge to a dual edge. A vertex of $G$ of
degree $k$ corresponds to a $k$-gonal face of $G'$.

By Lemma~\ref{lem:mindeg}, $\delta(G) \ge 5$, and Euler's formula gives
$\sum_{u \in V(G)}(6 - \deg u) = 12$, so $G$ has a vertex of degree exactly $5$
(indeed at least twelve). Fix such a vertex $v$. Its dual face $F_v$ is a
pentagon, bounded by the five dual vertices corresponding to the five faces of
$G$ incident to $v$.

\begin{definition}[Reduced dual]
\label{def:reduced-dual}
Let $v$ be a degree-$5$ vertex of $G$ with pentagonal dual face $F_v$, and fix an
index $i \in \{0,1,2,3,4\}$. The \emph{reduced dual} $\widehat{G}'_{v,i}$ is the
plane graph obtained from $G'$ as follows.
\begin{enumerate}
  \item Delete the five dual vertices on the boundary of $F_v$, together with all
        edges incident to them. Each deleted vertex is cubic, with two edges on
        $\partial F_v$ and one edge leaving $F_v$; deleting the five boundary
        vertices therefore removes the five external edges as well, dropping their
        five outer endpoints from degree $3$ to degree $2$. These five degree-$2$
        vertices lie on the boundary of a single face $F$ of the resulting graph.
  \item List the five degree-$2$ vertices in clockwise order around $F$ as
        $A = (A_0, A_1, A_2, A_3, A_4)$.
  \item Add a new vertex $v_n$ and join it to $A_i$, $A_{i+1}$, and $A_{i+2}$
        (indices mod $5$) by three new edges.
  \item Add a new edge between $A_{i+3}$ and $A_{i+4}$ (indices mod $5$).
\end{enumerate}
\end{definition}

\begin{remark}
Steps (3) and (4) restore cubicity: $A_i, A_{i+1}, A_{i+2}$ each gain one edge to
$v_n$ and $A_{i+3}, A_{i+4}$ each gain the new edge, so all five return to degree
$3$, and $v_n$ has degree $3$. Since $A_i,\dots,A_{i+2}$ and $A_{i+3}, A_{i+4}$
are each consecutive along $\partial F$, the new vertex and edge can be drawn
inside $F$ without crossings, so $\widehat{G}'_{v,i}$ is again a cubic plane
graph. The construction depends on the choice of $i$ up to the rotational
symmetry of $A$.
\end{remark}

\begin{figure}[h]
\centering
\includegraphics[width=0.48\textwidth]{fig_reduced_dual_step1.png}\hfill
\includegraphics[width=0.48\textwidth]{fig_reduced_dual_step2.png}\\[0.5em]
\includegraphics[width=0.48\textwidth]{fig_reduced_dual_step3.png}\hfill
\includegraphics[width=0.48\textwidth]{fig_reduced_dual_step4.png}
\caption{The four steps of Definition~\ref{def:reduced-dual}, illustrated on
$G' = $ the dodecahedron (dual of the icosahedron) with $F_v$ the inner
pentagon and $i = 0$. Top left: delete the five boundary vertices of $F_v$,
leaving five degree-$2$ vertices on a new face $F$. Top right: order them
clockwise as $A_0,\dots,A_4$. Bottom left: add $v_n$ joined to $A_0, A_1, A_2$.
Bottom right: add the chord $A_3 A_4$, giving the cubic plane graph
$\widehat{G}'_{v,0}$.}
\label{fig:reduced-dual-steps}
\end{figure}

\begin{definition}[Edges of the reduced dual]
\label{def:edge-names}
The four edges added in steps (3) and (4) of Definition~\ref{def:reduced-dual}
are named as follows. The chord $A_{i+3}A_{i+4}$ is the \emph{merged edge};
the edge $A_{i+1}v_n$ is the \emph{spike edge}; the edge $A_iv_n$ is the
\emph{side-$0$ edge}; and the edge $A_{i+2}v_n$ is the \emph{side-$1$ edge}.
In the $i = 0$ case of Figure~\ref{fig:reduced-dual-steps} these are
$\{A_3, A_4\}$, $\{A_1, v_n\}$, $\{A_0, v_n\}$, and $\{A_2, v_n\}$
respectively.
\end{definition}

We will use the following structural fact about proper $3$-edge-colourings near
a pentagonal face of a cubic plane graph; it is stated for a generic such graph
$H$, not specifically for the reduced dual.

\begin{lemma}[Pentagonal externals]
\label{lem:pentagonal-externals}
Let $H$ be a cubic plane graph and $F$ a pentagonal face of $H$, with
$\partial F$ traversed clockwise as $u_0, u_1, u_2, u_3, u_4$. For each $i$
let $f_i$ be the unique edge of $H$ incident to $u_i$ that does not lie on
$\partial F$. An assignment $\varphi$ of colours from $\{1, 2, 3\}$ to the ten
edges incident to $\{u_0, \dots, u_4\}$ is proper at every $u_i$ if and only if
there is some index $j$ such that
\[
  \varphi(f_j) = \varphi(f_{j+1}) = \varphi(f_{j+2})
  \quad\text{and}\quad
  \{\varphi(f_{j+3}), \varphi(f_{j+4})\}
    = \{1, 2, 3\} \setminus \{\varphi(f_j)\},
\]
indices mod $5$.
\end{lemma}

\begin{proof}
Write $e_i = u_i u_{i+1}$ for the boundary edges of $\partial F$ (indices mod
$5$). A colouring $\varphi$ is proper at every $u_i$ if and only if at each
$u_i$ the three incident edges $e_{i-1}, e_i, f_i$ receive three distinct
colours; whenever this holds, $\varphi(f_i)$ is forced to be the unique colour
in $\{1, 2, 3\} \setminus \{\varphi(e_{i-1}), \varphi(e_i)\}$, and $\varphi$
restricts to a proper $3$-edge-colouring of the cycle $\partial F$.

\textbf{($\Rightarrow$)} The line graph of $\partial F$ is $C_5$, whose
maximum independent set has size $2$, so no colour appears more than twice on
$\partial F$; and since $\partial F$ is an odd cycle, all three colours appear.
The colour multiset on $(\varphi(e_0), \dots, \varphi(e_4))$ is therefore
$(2, 2, 1)$, with the singleton at a unique position. Cyclically shifting
indices we may place this position at $0$; let $c$ be the singleton colour.
The remaining four edges form the path $e_1 e_2 e_3 e_4$, which by propriety
alternates between the other two colours, so for some labelling
$\{a, b, c\} = \{1, 2, 3\}$,
\[
  (\varphi(e_0), \varphi(e_1), \varphi(e_2), \varphi(e_3), \varphi(e_4))
  = (c, a, b, a, b).
\]
Reading off the forced values of $\varphi(f_i)$,
\[
  \varphi(f_0) = a, \quad
  \varphi(f_1) = b, \quad
  \varphi(f_2) = \varphi(f_3) = \varphi(f_4) = c,
\]
which is the lemma's pattern at $j = 2$ (the cyclic shift maps this back to
the corresponding $j$ in the original indexing). This case is the unique
proper $3$-edge-colouring of $\partial F$ up to cyclic shift and permutation of
$\{1, 2, 3\}$ (since $5 \cdot 3! = 30 = P(C_5, 3)$, the chromatic polynomial of
$C_5$ at $3$), so it exhausts every proper $\varphi$.

\textbf{($\Leftarrow$)} The lemma's hypothesis is invariant under cyclic
shifts of indices and under permutations of $\{1, 2, 3\}$, so we may assume
$j = 2$, $\varphi(f_2) = \varphi(f_3) = \varphi(f_4) = c$, $\varphi(f_0) = a$,
and $\varphi(f_1) = b$, with $\{a, b, c\} = \{1, 2, 3\}$. Propriety at $u_i$
and $u_{i+1}$ requires $\varphi(e_i) \notin \{\varphi(f_i), \varphi(f_{i+1})\}$,
which gives
\[
  \varphi(e_0) = c, \quad
  \varphi(e_1) = a, \quad
  \varphi(e_2) \in \{a, b\}, \quad
  \varphi(e_3) \in \{a, b\}, \quad
  \varphi(e_4) = b.
\]
The remaining propriety condition $\varphi(e_{i-1}) \neq \varphi(e_i)$ holds
automatically at $u_0, u_1, u_4$, forces $\varphi(e_2) = b$ at $u_2$, and then
forces $\varphi(e_3) = a$ at $u_3$. The resulting triples
$(\varphi(e_{i-1}), \varphi(e_i), \varphi(f_i))$ at $u_0, u_1, u_2, u_3, u_4$
are
\[
  (b, c, a), \quad (c, a, b), \quad (a, b, c), \quad (b, a, c), \quad (a, b, c),
\]
each a permutation of $\{1, 2, 3\}$, so $\varphi$ is proper at every $u_i$.
\end{proof}

\begin{remark}
The two-element condition $\{\varphi(f_{j+3}), \varphi(f_{j+4})\}
= \{1,2,3\}\setminus\{\varphi(f_j)\}$ cannot be dropped: a 3-colouring
satisfying $\varphi(f_j) = \varphi(f_{j+1}) = \varphi(f_{j+2})$ alone need not
extend, e.g.\ $(1,1,1,1,2)$.
\end{remark}

Since $\widehat{G}'_{v,i}$ is the dual of a triangulation on fewer vertices than
$G$, it is $3$-edge-colourable by the minimality of $G$. The following lemma
constrains every such colouring.

\begin{lemma}
\label{lem:chord-apex}
Let $G$ be a minimal counterexample, and let $\widehat{G}'_{v,i}$ be a reduced
dual of its dual $G'$. Then in every proper $3$-edge-colouring of
$\widehat{G}'_{v,i}$, the merged edge and the spike edge receive the same
colour.
\end{lemma}

\begin{figure}[h]
\centering
\includegraphics[width=0.7\textwidth]{fig_chord_apex_step1.png}\\[0.4em]
\includegraphics[width=0.48\textwidth]{fig_chord_apex_step2.png}\hfill
\includegraphics[width=0.48\textwidth]{fig_chord_apex_step3.png}
\caption{The proof of Lemma~\ref{lem:chord-apex}, illustrated for $i = 0$ on
$G' = $ the dodecahedron. Top: under the assumption $W \neq Y$, propriety at
$v_n$ forces $W \in \{X, Z\}$. Bottom: in either case the lift to $G'$ has
externals satisfying the hypothesis of
Lemma~\ref{lem:pentagonal-externals}, which colours $\partial F_v$ to extend
$\psi$ to a proper $3$-edge-colouring of $G'$.}
\label{fig:chord-apex-proof}
\end{figure}

\begin{proof}
After cyclically relabelling, assume $i = 0$. Suppose for contradiction that
$\varphi$ is a proper $3$-edge-colouring of $\widehat{G}'_{v,0}$ in which the
merged edge $\{A_3, A_4\}$ and the spike edge $\{A_1, v_n\}$ receive different
colours (Figure~\ref{fig:chord-apex-proof}, top), and write
\[
  X = \varphi(\{A_0, v_n\}), \quad
  Y = \varphi(\{A_1, v_n\}), \quad
  Z = \varphi(\{A_2, v_n\}), \quad
  W = \varphi(\{A_3, A_4\}).
\]
Propriety of $\varphi$ at $v_n$ forces $\{X, Y, Z\} = \{1, 2, 3\}$, and the
assumption $W \neq Y$ leaves $W \in \{X, Z\}$.

We lift $\varphi$ to a colouring $\psi$ of $E(G')$ as follows. Let
$B_0, \dots, B_4$ be the boundary vertices of $\partial F_v$ in $G'$, indexed
so that $f_k = B_k A_k$. On every edge of $G'$ that survived the reduction,
set $\psi = \varphi$. At each $A_k$ the two surviving edges retain their
$\varphi$-colours, so the remaining edge at $A_k$ --- in $G'$ this is the
external $f_k$; in $\widehat{G}'_{v,0}$ this is a $v_n$-edge ($k \in
\{0, 1, 2\}$) or the chord ($k \in \{3, 4\}$) --- is forced to take the third
colour at $A_k$. Since the two-surviving-edge colours at $A_k$ agree in $G'$
and $\widehat{G}'_{v,0}$, the third colour does too, giving
\[
  \psi(f_0) = X, \quad \psi(f_1) = Y, \quad \psi(f_2) = Z, \quad
  \psi(f_3) = \psi(f_4) = W
\]
(the last two equalities holding because the chord is a single edge contributing
its colour at each of $A_3$ and $A_4$).

It remains to assign colours to the five boundary edges $B_k B_{k+1}$ of
$\partial F_v$. Apply Lemma~\ref{lem:pentagonal-externals} to $G'$ at the face
$F_v$ with the $B_k$'s as its boundary vertices and the same indexing. The
external vector $(\psi(f_0), \dots, \psi(f_4)) = (X, Y, Z, W, W)$ falls into
one of two cases (Figure~\ref{fig:chord-apex-proof}, bottom):
\begin{itemize}
  \item if $W = Z$, it is $(X, Y, Z, Z, Z)$: three consecutive $Z$'s at
        positions $2, 3, 4$, with $\{X, Y\} = \{1, 2, 3\} \setminus \{Z\}$;
  \item if $W = X$, it is $(X, Y, Z, X, X)$: three consecutive $X$'s at
        positions $3, 4, 0$, with $\{Y, Z\} = \{1, 2, 3\} \setminus \{X\}$.
\end{itemize}
Each case satisfies the hypothesis of Lemma~\ref{lem:pentagonal-externals};
its $(\Leftarrow)$ direction therefore assigns colours to the boundary edges
$B_k B_{k+1}$ that make $\psi$ proper at every $B_k$.

The resulting $\psi$ is a proper $3$-edge-colouring of $G'$: proper at every
$B_k$ by the lemma, at every $A_k$ by the construction, and at every other
vertex because such a vertex has the same neighbourhood in $G'$ as in
$\widehat{G}'_{v,0}$ with the same incident-edge colours. By Tait's theorem,
$G'$ is $3$-edge-colourable iff $G$ is $4$-vertex-colourable, contradicting
that $G$ is a counterexample. The assumption $W \neq Y$ is therefore false.
\end{proof}

For a pair of colours $\{a, b\} \subseteq \{1, 2, 3\}$, the subgraph of
$\widehat{G}'_{v,i}$ on the edges coloured $a$ or $b$ is $2$-regular (since at
each vertex exactly one of the three incident edges is excluded), and hence a
disjoint union of cycles. We call each such cycle a \emph{$\{a, b\}$-Kempe
cycle}, and reserve the notation for the specific cycle containing a given
edge when the context makes it clear. Swapping the two colours on a single
Kempe cycle yields another proper $3$-edge-colouring of the same graph.

\begin{lemma}[Kempe cycles through the spike]
\label{lem:kempe-spike}
Let $G$ be a minimal counterexample, fix a reduced dual $\widehat{G}'_{v,i}$ of
$G'$, and let $\varphi$ be a proper $3$-edge-colouring of $\widehat{G}'_{v,i}$.
Write $c$ for the common colour assigned by $\varphi$ to the spike and the
merged edge (Lemma~\ref{lem:chord-apex}), and $c_0, c_1$ for the colours of
the side-$0$ and side-$1$ edges respectively, so $\{c, c_0, c_1\} = \{1, 2,
3\}$. Then
\begin{enumerate}
  \item the $\{c, c_0\}$-Kempe cycle through the spike edge contains both the
        side-$0$ edge and the merged edge;
  \item the $\{c, c_1\}$-Kempe cycle through the spike edge contains both the
        side-$1$ edge and the merged edge.
\end{enumerate}
\end{lemma}

\begin{proof}
We prove (1); (2) is the same argument with $c_1$ and the side-$1$ edge in
place of $c_0$ and the side-$0$ edge.

The spike edge $\{A_{i+1}, v_n\}$ and the side-$0$ edge $\{A_i, v_n\}$ share
the vertex $v_n$ and receive the two colours $c, c_0$, so they both lie on the
$\{c, c_0\}$-Kempe cycle through $v_n$. Suppose for contradiction that the
merged edge lies on a different $\{c, c_0\}$-Kempe cycle $K$ (it lies on
\emph{some} such cycle, since it has colour $c$). Let $\varphi'$ be obtained
from $\varphi$ by swapping the colours $c$ and $c_0$ along $K$ alone: this is
a Kempe swap, so $\varphi'$ is again a proper $3$-edge-colouring of
$\widehat{G}'_{v,i}$. Under $\varphi'$ the spike edge --- which is not on $K$
--- still has colour $c$, but the merged edge --- which is on $K$ --- now has
colour $c_0$. Hence in $\varphi'$ the spike and the merged edge receive
distinct colours, contradicting Lemma~\ref{lem:chord-apex} applied to
$\varphi'$.
\end{proof}

\section{Edge suppression}
\label{sec:edge-suppression}

We recall the classical operation of \emph{edge suppression} on cubic
plane graphs: delete the edge and smooth the two resulting degree-$2$
endpoints. Under planar duality this coincides with simple-graph
contraction on the dual side. It will be the central tool in
Section~\ref{sec:toward-4ct} below, where we formulate a sufficient
condition for the Four Colour Theorem.

\begin{definition}[Edge suppression]
\label{def:edge-suppression}
Let $H$ be a cubic plane graph and $e = uv$ an edge of $H$ with $u \neq v$
and no edge of $H$ parallel to $e$. The \emph{edge suppression} of $H$ at
$e$ is the graph $H'$ obtained in two steps:
\begin{enumerate}
  \item \emph{Delete} the edge $e$; the endpoints $u$ and $v$ each drop to
        degree $2$.
  \item \emph{Smooth} each of $u$ and $v$: at $u$, replace $u$ and its two
        remaining incident edges $ua, ub$ by a single new edge $ab$; do
        the same at $v$. Both vertices $u$ and $v$ are removed, and two
        new edges are added in their place.
\end{enumerate}
Provided the smoothings do not introduce a loop or parallel edge, $H'$ is
again a cubic plane graph, with $|V(H')| = |V(H)| - 2$ and
$|E(H')| = |E(H)| - 3$.

Equivalently, $H'$ is the planar dual of $\mathrm{dual}(H) / e^{*}$,
where $e^{*}$ is the edge of $\mathrm{dual}(H)$ crossing $e$ and the
contraction on the right-hand side is simple-graph contraction (loops
removed, parallel edges absorbed). Under planar duality, contracting
$e^{*}$ in $\mathrm{dual}(H)$ merges the two triangular faces of
$\mathrm{dual}(H)$ incident to $e^{*}$, and the parallel-edge cleanup
corresponds exactly to the smoothing step on the primal side.
\end{definition}

\begin{figure}[h]
\centering
\includegraphics[width=0.95\textwidth]{fig_cubic_edge_contraction.png}
\caption{Edge suppression
(Definition~\ref{def:edge-suppression}). Left: a fragment of a cubic
plane graph with the suppressed edge $e = uv$ highlighted in red. Middle:
deleting $e$ leaves $u$ and $v$ of degree~$2$. Right: smoothing $u$ and
$v$ replaces each pair of incident edges by a single new edge, removing
$u, v$ and giving a cubic plane graph again.}
\label{fig:edge-suppression}
\end{figure}

\begin{theorem}[Edge suppression across a 4-face preserves 3-edge-colourability]
\label{thm:edge-suppression-4face}
Let $H$ be a cubic plane graph with a proper $3$-edge-colouring $\varphi$,
let $f$ be a face of $H$ with $|\partial f| = 4$, and let $e_0, e_1$ be
the two edges of $\partial f$ sharing no endpoint (the opposite pair on
the $4$-cycle $\partial f$). If $\varphi(e_0) \neq \varphi(e_1)$ and the
edge suppression of $H$ at $e_0$
(Definition~\ref{def:edge-suppression}) is well-defined (no loops or
parallel edges are created), then the suppressed graph admits a proper
$3$-edge-colouring.
\end{theorem}

\begin{proof}
Write $\partial f$ as the $4$-cycle $v_0 v_1 v_2 v_3$ with $e_0 = v_0 v_1$
and $e_1 = v_2 v_3$ (so $e_0, e_1$ are opposite); the remaining two
boundary edges of $f$ are $e_2 := v_1 v_2$ and $e_3 := v_3 v_0$. Since $H$
is cubic, each $v_i$ has exactly one edge not on $\partial f$: write $w_i$
for that edge and $u_i$ for its other endpoint, so $w_i = v_i u_i$ with
$u_i \notin \{v_0, v_1, v_2, v_3\}$, for each $i \in \{0, 1, 2, 3\}$. Put
$a := \varphi(e_0)$, $b := \varphi(e_1)$, and let $c$ be the third colour.

\emph{Forced colours on the face.} Propriety at $v_1$ and $v_2$ forces
$\varphi(e_2) \notin \{a, b\}$, so $\varphi(e_2) = c$; then
$\varphi(w_1) = b$ and $\varphi(w_2) = a$. Symmetrically $\varphi(e_3) = c$,
$\varphi(w_0) = b$, and $\varphi(w_3) = a$. In particular
$\varphi(w_0) = \varphi(w_1) = b$.

\emph{Construction of $\varphi'$.} Let $H'$ denote the edge suppression
of $H$ at $e_0$; its new edges are $e_3' := v_3 u_0$
(replacing $e_3$ and $w_0$ via the smoothing at $v_0$) and
$e_2' := v_2 u_1$ (replacing $e_2$ and $w_1$ via the smoothing at $v_1$).
Define $\varphi' \colon E(H') \to \{1, 2, 3\}$ by
\[
  \varphi'(e) :=
  \begin{cases}
    c & \text{if } e = e_1, \\
    b & \text{if } e \in \{e_2', e_3'\}, \\
    \varphi(e) & \text{otherwise.}
  \end{cases}
\]
That is: give each smoothed-in edge the colour $b$ (the colour of the two
$w_i$ it absorbs), recolour $e_1$ to $c$, and leave every other edge of
$H'$ with its $\varphi$-colour.

\emph{Propriety.} Every vertex of $H'$ other than $v_2, v_3, u_0, u_1$ has
the same incident edges and the same $\varphi'$-colours as it did under
$\varphi$, so propriety is inherited there. At the four affected vertices,
\[
\begin{array}{r|lll}
\text{vertex} & \text{edges in } H' & \text{colours under }\varphi' \\
\hline
v_2 & e_1,\; w_2,\; e_2'         & c,\; a,\; b \\
v_3 & e_1,\; w_3,\; e_3'         & c,\; a,\; b \\
u_0 & e_3',\; \alpha_0,\; \beta_0 & b,\; a,\; c \\
u_1 & e_2',\; \alpha_1,\; \beta_1 & b,\; a,\; c
\end{array}
\]
where $\alpha_i, \beta_i$ are the two edges of $H$ at $u_i$ other than
$w_i$, whose $\varphi$-colours are forced to $\{a, c\}$ by propriety at
$u_i$ (since $\varphi(w_i) = b$). Each row lists three distinct colours, so
$\varphi'$ is proper.
\end{proof}

\begin{figure}[h]
\centering
\includegraphics[width=0.98\textwidth]{fig_thm_cubic_contraction_4face.png}
\caption{The recolouring used in the proof of
Theorem~\ref{thm:edge-suppression-4face}. Left: the $4$-face $f$ of $H$
under $\varphi$, with the forced colours $\varphi(e_0) = a$,
$\varphi(e_1) = b$, $\varphi(e_2) = \varphi(e_3) = c$,
$\varphi(w_0) = \varphi(w_1) = b$, and $\varphi(w_2) = \varphi(w_3) = a$.
Right: the suppressed graph $H'$ under $\varphi'$. The smoothed-in edges
$e_2', e_3'$ inherit the colour $b$ from $w_0, w_1$, and $e_1$ is
recoloured from $b$ to $c$; every edge outside the face neighbourhood
keeps its $\varphi$-colour (dotted in red: the five edges of $H$ removed
by the suppression).}
\label{fig:thm-edge-suppression-4face}
\end{figure}

\section{The face-monochromatic-pair conjecture and the Four Colour Theorem}
\label{sec:toward-4ct}

The following conjecture identifies a structural property of every proper
$3$-edge-colouring of a reduced dual of a minimal counterexample. If true,
it implies the Four Colour Theorem via
Theorem~\ref{thm:edge-suppression-4face}.

\begin{conjecture}[Face-monochromatic-pair conjecture]
\label{conj:face-monochromatic-pair-on-merged-kempe-cycle}
Let $G$ be a minimal counterexample to the Four Colour Theorem, and let
$\widehat{G}'_{v,i}$ be a reduced dual of $G' = \mathrm{dual}(G)$. Then
for every proper $3$-edge-colouring $\varphi$ of $\widehat{G}'_{v,i}$
there exist a face $F$ of $\widehat{G}'_{v,i}$ and two distinct edges
$e_1, e_2 \in \partial F$, with neither $e_1$ nor $e_2$ equal to the
merged edge, such that:
\begin{enumerate}
  \item $\varphi(e_1) = \varphi(e_2)$. Write
        $a := \varphi(e_1) = \varphi(e_2)$.
  \item $e_1$, $e_2$, and the merged edge all lie on a common
        $\{a, b\}$-Kempe cycle of $\varphi$, for some colour $b \neq a$.
  \item Exactly one edge of $\partial F$ lies between $e_1$ and $e_2$
        along one of the two arcs of $\partial F$. Equivalently,
        subdividing $e_1, e_2$ by new vertices $X_1, X_2$ and joining
        them by a new edge $X_1 X_2$ inside $F$ creates a new face $f_n$
        bounded by exactly $4$ edges (the new edge $X_1 X_2$, the two
        subdivision halves adjacent to it, and the single
        $\partial F$-edge between $e_1$ and $e_2$).
\end{enumerate}
\end{conjecture}

\begin{remark}
\label{rem:conj-3-6-empirical}
\sloppy
The conjecture cannot be tested on actual minimal counterexamples (none
exist by the Four Colour Theorem), but its conclusion is checkable on the
structural surrogates: proper $3$-edge-colourings of reduced duals that
satisfy both the chord-apex condition (Lemma~\ref{lem:chord-apex}) and
the Kempe-cycle conditions (Lemma~\ref{lem:kempe-spike}), since a minimal
counterexample's reduced dual is forced to admit such colourings. For
every min-degree-$5$ triangulation $G$ with $|V(G)| \leq 21$, every
pentagonal face $F$ of $G'$, and every reduction index
$i \in \{0,\dots,4\}$, we enumerated all such colourings and verified the
three clauses of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} (see
\texttt{experiments/check\_conj\_face\_kempe\_scaled.py}); $n = 22$ ran
past a $1800$\,s budget after $641{,}700$ colourings (all pass) without
finishing the full set of $651$ triangulations.
\begin{center}
\small
\renewcommand{\arraystretch}{1.15}
\begin{tabular}{r|r|r|r|l}
$n$ & \#tri & \#col.\ tested & \#sat. & status \\
\hline
$12$         & $1$    & $0$         & ---         & vacuous (icosahedron) \\
$13$         & $0$    & ---         & ---         & no min-deg-$5$ tri \\
$14$         & $1$    & $216$       & $216$       & all pass \\
$15$         & $1$    & $0$         & ---         & vacuous \\
$16$         & $3$    & $864$       & $864$       & all pass \\
$17$         & $4$    & $4{,}650$   & $4{,}650$   & all pass \\
$18$         & $12$   & $8{,}070$   & $8{,}070$   & all pass \\
$19$         & $23$   & $21{,}138$  & $21{,}138$  & all pass \\
$20$         & $73$   & $107{,}874$ & $107{,}874$ & all pass \\
$21$         & $192$  & $392{,}370$ & $392{,}370$ & all pass \\
$22$ (part.) & $651$  & $641{,}700$ & $641{,}700$ & timeout \\
\hline
total ($n \le 21$) & $311$ & $535{,}182$ & $535{,}182$ & \\
\end{tabular}
\end{center}
\noindent The vacuous rows ($n = 12, 15$) are those where the relevant
reduced duals admit no chord-apex+Kempe colourings, so the conjecture
has no content there.
\end{remark}

The following strengthening adds a fourth clause that arranges the new
$4$-face $f_n$ to satisfy the hypotheses of
Theorem~\ref{thm:edge-suppression-4face}.

\begin{conjecture}[Strengthening of
  Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}]
\label{conj:face-monochromatic-pair-strengthened}
Let $G$, $\widehat{G}'_{v,i}$, $\varphi$ be as in
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}. Then
there exist $F$, $e_1$, $e_2$ satisfying clauses~(1)--(3) of that
conjecture, together with the following additional clause.
\begin{enumerate}
  \setcounter{enumi}{3}
  \item Let $\widehat{G}'^{+}$ be the modified graph obtained from
        $\widehat{G}'_{v,i}$ by the modification of clause~(3), and let
        $\varphi'$ be the proper $3$-edge-colouring of $\widehat{G}'^{+}$
        obtained from $\varphi$ by swapping the two colours along the
        (subdivided) $\{a, b\}$-Kempe cycle of clause~(2) and assigning
        the new edge $X_1 X_2$ the remaining (third) colour $c$.
        (Equivalently: $\varphi'$ agrees with $\varphi$ on every edge of
        $\widehat{G}'_{v,i}$ outside that Kempe cycle, and at $X_1, X_2$
        the two subdivision halves take the colours $\{a, b\}$ in the
        order forced by propriety.) Then either
        \begin{enumerate}
          \item[(i)] $\partial f_n$ uses all three colours under
                     $\varphi'$, or
          \item[(ii)] the $\{b, c\}$-Kempe cycle of $\varphi'$ through
                     $X_1 X_2$ is incident to exactly one edge of
                     $\partial f_n$ (namely $X_1 X_2$ itself).
        \end{enumerate}
\end{enumerate}
\end{conjecture}

\begin{remark}
\label{rem:conj-3-8-empirical}
\sloppy
The strengthened conjecture was tested on the same chord-apex+Kempe
colourings as Remark~\ref{rem:conj-3-6-empirical}; for each colouring we
sought any
Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}-witness
$(F, e_1, e_2)$ whose accompanying $f_n$ satisfies clause~(4) (see
\texttt{experiments/check\_conj\_3\_8\_scaled.py}):
\begin{center}
\small
\renewcommand{\arraystretch}{1.15}
\begin{tabular}{r|r|r|r|l}
$n$ & \#tri & \#col.\ tested & \#sat. & status \\
\hline
$14$ & $1$  & $216$       & $216$       & all pass \\
$16$ & $3$  & $864$       & $864$       & all pass \\
$17$ & $4$  & $4{,}650$   & $4{,}650$   & all pass \\
$18$ & $12$ & $8{,}070$   & $8{,}070$   & all pass \\
$19$ & $23$ & $21{,}138$  & $21{,}138$  & all pass \\
$20$ & $73$ & $107{,}874$ & $107{,}874$ & all pass \\
\hline
total ($n \le 20$) & $116$ & $142{,}812$ & $142{,}812$ & \\
\end{tabular}
\end{center}
\noindent A subtlety: only about half of the
Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}-witnesses
individually satisfy clause~(4) on each colouring, but in every case
\emph{some} witness does. Clause~(4) is therefore an existential statement
at the witness level, not a property of every witness.

\smallskip\noindent\emph{Targeted check on the Holton--McKay duals.}
The six $21$-vertex triangulations whose duals are the
non-Hamiltonian $38$-vertex cubic plane graphs of Holton and McKay
(the smallest examples falsifying Tait's conjecture) are a particularly
interesting subfamily at $n = 21$. Running the strengthened test directly
on these six (see
\texttt{experiments/check\_conj\_on\_holton\_mckay.py}) gives:

\begin{center}
\small
\renewcommand{\arraystretch}{1.15}
\begin{tabular}{r|r|r|r|l}
HM\# & \#pentagonal faces & \#col.\ tested & \#sat.\ (1)--(4) & status \\
\hline
$0$ & $10$ & $2{,}880$ & $2{,}880$ & all pass \\
$1$ & $11$ & $2{,}880$ & $2{,}880$ & all pass \\
$2$ & $10$ & $2{,}880$ & $2{,}880$ & all pass \\
$3$ & $10$ & $2{,}880$ & $2{,}880$ & all pass \\
$4$ & $11$ & $2{,}880$ & $2{,}880$ & all pass \\
$5$ & $11$ & $2{,}880$ & $2{,}880$ & all pass \\
\hline
total & --- & $17{,}280$ & $17{,}280$ & \\
\end{tabular}
\end{center}
\end{remark}

\begin{remark}[The implication to the Four Colour Theorem]
\label{rem:implication-4ct}
Clause~(4)(i) of
Conjecture~\ref{conj:face-monochromatic-pair-strengthened} says that
$\partial f_n$ uses all three colours under $\varphi'$. Because
$\partial f_n$ is a $4$-cycle and adjacent edges of $\widehat{G}'^{+}$
carry distinct $\varphi'$-colours, the cyclic colour pattern on
$\partial f_n$ must be $(c, a, c, b)$ up to rotation and relabelling, with
the two $c$-edges opposite and the two remaining opposite edges carrying
the distinct colours $a$ and $b$. Those two opposite edges therefore
satisfy the hypothesis of Theorem~\ref{thm:edge-suppression-4face}: they
lie on the $4$-face $f_n$, share no endpoint, and have different
$\varphi'$-colours. Theorem~\ref{thm:edge-suppression-4face} then produces
a proper $3$-edge-colouring of the edge suppression of
$\widehat{G}'^{+}$ at the $a$-coloured one.

Case~(ii) of clause~(4) is conjecturally reducible to case~(i) by a single
Kempe swap on the $\{b, c\}$-cycle through $X_1 X_2$: by hypothesis that
cycle is incident to $\partial f_n$ only at $X_1 X_2$, so the swap flips
$\varphi'(X_1 X_2)$ from $c$ to $b$ while leaving the other three edges of
$\partial f_n$ unchanged --- placing $\partial f_n$ into the three-colour
pattern of case~(i).

\smallskip\noindent\emph{Consequence.}
Theorem~\ref{thm:edge-suppression-4face} now produces a proper
$3$-edge-colouring of the edge suppression of $\widehat{G}'^{+}$ at the
chosen edge of $f_n$. Combined with the
chord-apex and Kempe-cycle structure of $\widehat{G}'_{v,i}$
(Lemmas~\ref{lem:chord-apex} and~\ref{lem:kempe-spike}), this yields a
proper $3$-edge-colouring of $G'$, and by Tait's correspondence a proper
$4$-vertex-colouring of $G$ --- contradicting the assumption that $G$ is a
minimal counterexample. Hence
Conjecture~\ref{conj:face-monochromatic-pair-strengthened} implies the
Four Colour Theorem.
\end{remark}

\begin{thebibliography}{9}
\bibitem{AH77a}
K.~Appel and W.~Haken,
\emph{Every planar map is four colorable. Part~I: Discharging},
Illinois J.~Math. \textbf{21} (1977), 429--490.

\bibitem{AHK77}
K.~Appel, W.~Haken, and J.~Koch,
\emph{Every planar map is four colorable. Part~II: Reducibility},
Illinois J.~Math. \textbf{21} (1977), 491--567.

\bibitem{RSST97}
N.~Robertson, D.~P.~Sanders, P.~Seymour, and R.~Thomas,
\emph{The four-colour theorem},
J.~Combin. Theory Ser.~B \textbf{70} (1997), 2--44.

\bibitem{Gonthier08}
G.~Gonthier,
\emph{Formal proof---the four-color theorem},
Notices Amer. Math. Soc. \textbf{55} (2008), no.~11, 1382--1393.
\end{thebibliography}

\end{document}
