math-research/papers/face_monochromatic_pairs/paper.tex

%% 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'$.

The following labelling of vertices in a properly $3$-edge-coloured cubic
plane graph will be useful in Section~\ref{sec:toward-4ct}.

\begin{definition}[Heawood number of a vertex]
\label{def:heawood-number}
Let $H$ be a cubic plane graph with a fixed planar embedding, and let
$\varphi \colon E(H) \to \{1, 2, 3\}$ be a proper $3$-edge-colouring. At
each vertex $v \in V(H)$, the three incident edges receive three distinct
colours; reading them in clockwise order around $v$ gives a cyclic
permutation of $(1, 2, 3)$. The \emph{Heawood number} of $v$ is
\[
  h_\varphi(v) :=
  \begin{cases}
    +1 & \text{if the clockwise cyclic colour order at $v$ is }(1, 2, 3), \\
    -1 & \text{if it is }(1, 3, 2).
  \end{cases}
\]
Equivalently, $h_\varphi(v) = +1$ when the clockwise colour order at $v$ is
an even cyclic permutation of $(1, 2, 3)$ and $-1$ when it is an odd one.
The labels are due to Heawood~\cite{Heawood1898}, who introduced them as
part of his analysis of $3$-edge-colourings of cubic plane graphs.
\end{definition}

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{lemma}[A Heawood-constant Kempe cycle does not admit the clause-(3) arc]
\label{lem:kempe-heawood-constant}
Let $G$ be a minimal counterexample to the Four Colour Theorem, fix a
reduced dual $\widehat{G}'_{v,i}$ of $G' = \mathrm{dual}(G)$, and let
$\varphi$ be a proper $3$-edge-colouring of $\widehat{G}'_{v,i}$. Set
$a := \varphi(\mathrm{merged})$ and let $K$ be the $\{a, b\}$-Kempe
cycle of $\varphi$ through the merged edge for some
$b \in \{1, 2, 3\} \setminus \{a\}$. If $h_\varphi$ is constant on
$V(K)$, then no edge $e \in E(K)$ admits a face $F$ of
$\widehat{G}'_{v,i}$ and two non-incident edges
$e_1, e_2 \in \partial F$ such that
$\varphi(e_1) = \varphi(e_2)$ and $e$ is the unique edge of
$\partial F$ between $e_1$ and $e_2$ along one of the two arcs of
$\partial F$ --- that is, no edge of $K$ admits the clause-(3) arc of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
with $e_1, e_2$ at its two endpoints.
\end{lemma}

\begin{proof}
Let $c$ be the third colour. Fix any edge $e \in E(K)$ joining
$v_0, v_1 \in V(K)$. By hypothesis $h_\varphi(v_0) = h_\varphi(v_1)$;
after possibly relabelling we may take
$h_\varphi(v_0) = h_\varphi(v_1) = +1$, so by
Definition~\ref{def:heawood-number} the clockwise cyclic colour order
at $v_0$ and at $v_1$ is the same even cyclic class $(a, b, c)$.

Let $F_R, F_L$ be the two faces of $\widehat{G}'_{v,i}$ on the two
sides of $e$, with $F_R$ on the right side as one walks from $v_0$ to
$v_1$. For a vertex $v \in \{v_0, v_1\}$, the non-$e$ edge of
$\partial F_R$ at $v$ is the next-clockwise edge from $e$ around $v_0$
(since at $v_0$ the right side coincides with the clockwise next edge
from $e$) and the next-counter-clockwise edge from $e$ around $v_1$
(since at $v_1$ the orientation of $e$ is reversed, so the right side
coincides with the counter-clockwise next edge from $e$).

\emph{Case~A: $\varphi(e) = a$.} In the CW order $(a, b, c)$ at $v_0$
the next-CW edge from $e$ has colour $b$; in the same CW order
$(a, b, c)$ at $v_1$ the next-CCW edge from $e$ has colour $c$ (since
CCW-next from $a$ in cyclic order $(a, b, c)$ is $c$). Hence the
non-$e$ edge of $\partial F_R$ at $v_0$ has colour $b$, while the
non-$e$ edge of $\partial F_R$ at $v_1$ has colour $c$ --- these
differ. Symmetrically, the non-$e$ edges of $\partial F_L$ at $v_0$
and $v_1$ have colours $c$ and $b$ respectively, again different.
Hence the colour-$b$ edges at $v_0$ and $v_1$ lie on opposite faces
of $e$, and the same for the colour-$c$ edges; no face of
$\widehat{G}'_{v,i}$ contains two same-coloured non-$e$ edges at
$\{v_0, v_1\}$.

\emph{Case~B: $\varphi(e) = b$.} By the analogous reasoning, the
non-$e$ edges of $\partial F_R$ at $v_0$ and $v_1$ have colours $c$
and $a$ respectively, and those of $\partial F_L$ have colours $a$
and $c$. The colour-$a$ edges at $v_0, v_1$ thus lie on opposite
faces of $e$, and so do the colour-$c$ edges.

In either case, no face $F$ of $\widehat{G}'_{v,i}$ has two same-coloured
non-$e$ edges at $\{v_0, v_1\}$ on $\partial F$, so the clause-(3) arc
(with $e$ as the unique $\partial F$-edge between $e_1$ and $e_2$ at the
endpoints of $e$) cannot be realised.
\end{proof}

\begin{figure}[h]
\centering
\includegraphics[width=0.98\textwidth]{fig_lemma_kempe_heawood.png}
\caption{The two cases in the proof of
Lemma~\ref{lem:kempe-heawood-constant}. Vertices $v_0, v_1$ are
consecutive on the $\{a, b\}$-Kempe cycle $K$, joined by an edge $e$,
with the lemma's hypothesis $h_\varphi(v_0) = h_\varphi(v_1) = +1$ ---
so both vertices share the clockwise colour order $(a, b, c)$.
\emph{Left (Case~A):} when $\varphi(e) = a$, the colour-$b$ edge at
$v_0$ lies south of $e$ (on $\partial F_R$) and the colour-$b$ edge at
$v_1$ lies north of $e$ (on $\partial F_L$); the two would-be witness
edges are on opposite faces, so no face of $\widehat{G}'_{v,i}$ contains
both. \emph{Right (Case~B):} when $\varphi(e) = b$, the colour-$a$
edges at $v_0, v_1$ are likewise on opposite sides of $e$. In either
case the clause-$(3)$ arc of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
cannot be realised at $e$.}
\label{fig:lemma-kempe-heawood}
\end{figure}

\begin{lemma}[If Conjecture 5.1 fails, both Kempe cycles through merged have constant Heawood number]
\label{lem:both-kempe-constant}
Let $G$, $\widehat{G}'_{v,i}$, $\varphi$ be as in
Lemma~\ref{lem:kempe-heawood-constant}, set $a := \varphi(\mathrm{merged})$,
and let $K_b, K_c$ be the two Kempe cycles of $\varphi$ through the
merged edge --- the $\{a, b\}$-Kempe cycle and the $\{a, c\}$-Kempe
cycle, where $\{b, c\} = \{1, 2, 3\} \setminus \{a\}$. If no triple
$(F, e_1, e_2)$ satisfies clauses~(1)--(3) of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} on
$(G, \widehat{G}'_{v,i}, \varphi)$, then $h_\varphi$ is constant on
$V(K_b)$ and on $V(K_c)$, and the two constants agree (so all of
$V(K_b) \cup V(K_c)$ shares a common Heawood number).
\end{lemma}

\begin{proof}
We prove the contrapositive: if $h_\varphi$ is non-constant on
$V(K_b)$ (the argument for $K_c$ is identical), then a triple
$(F, e_1, e_2)$ realising clauses~(1)--(3) of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
exists. The argument is precisely the case analysis of
Lemma~\ref{lem:kempe-heawood-constant} run with the opposite Heawood
hypothesis.

Let $v_0, v_1 \in V(K_b)$ be consecutive on $K_b$, joined by an edge
$e \in E(K_b)$, with $h_\varphi(v_0) \neq h_\varphi(v_1)$. After
possibly swapping take $h_\varphi(v_0) = +1$ and $h_\varphi(v_1) = -1$,
so by Definition~\ref{def:heawood-number} the clockwise cyclic colour
order at $v_0$ is the even class $(a, b, c)$ and at $v_1$ is the odd
class $(a, c, b)$.

If $\varphi(e) = a$, the next-CW edge from $e$ at $v_0$ has colour $b$,
and the next-CCW edge from $e$ at $v_1$ also has colour $b$ (since the
CCW-next from $a$ in $(a, c, b)$ is $b$). Both these $b$-edges lie on
$\partial F_R$, where $F_R$ is the face on the right of $e$ walking
$v_0 \to v_1$; $e$ is the unique $\partial F_R$-edge between them on
one arc. Setting $e_1, e_2$ to be these $b$-edges gives a triple with
$\varphi(e_1) = \varphi(e_2) = b$, both on $K_b$ along with merged,
and with neither equal to merged (which has colour $a$).

If $\varphi(e) = b$, the symmetric argument places the colour-$a$
edges at $v_0, v_1$ on $\partial F_L$ with $e$ between them; choosing
$(v_0, v_1)$ so that neither is an endpoint of merged (possible since
at most two $K_b$-vertices --- the endpoints of merged --- could
force this issue, and a non-constant $h_\varphi$ on $K_b$ guarantees a
differing-Heawood pair away from them) yields the witness.

Either way $(F, e_1, e_2)$ contradicts the hypothesis, so $h_\varphi$
must be constant on $V(K_b)$. The same argument with $K_c$ in place of
$K_b$ gives constancy on $V(K_c)$. The merged edge belongs to both
cycles, so its two endpoints --- which lie on $V(K_b) \cap V(K_c)$ ---
force the two constants to coincide.
\end{proof}

\begin{corollary}[Per-cycle form]
\label{cor:single-cycle-non-constancy}
Let $G$, $\widehat{G}'_{v,i}$, $\varphi$ be as in
Lemma~\ref{lem:both-kempe-constant}, and let $K$ be either of the two
Kempe cycles of $\varphi$ through the merged edge. If $h_\varphi$ is not
constant on $V(K)$, then a triple $(F, e_1, e_2)$ satisfying
clauses~(1)--(3) of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} on
$(G, \widehat{G}'_{v,i}, \varphi)$ exists.
\end{corollary}

\begin{proof}
This is precisely the case analysis used to prove
Lemma~\ref{lem:both-kempe-constant}: applied to any consecutive pair of
vertices on $K$ with differing Heawood numbers, the construction in
that proof produces a clauses-(1)--(3) witness without ever needing to
inspect the other Kempe cycle.
\end{proof}

\begin{conjecture}[Constant Heawood on two edge-sharing Kempe cycles --- \textbf{FALSE}]
\label{conj:no-two-constant-kempe-cycles}
Let $H$ be a cubic plane graph with a proper $3$-edge-colouring
$\varphi$, fix a colour $a \in \{1, 2, 3\}$, and let $\{b, c\} =
\{1, 2, 3\} \setminus \{a\}$. Let $K_0$ be an $\{a, b\}$-Kempe cycle
of $\varphi$ and $K_1$ an $\{a, c\}$-Kempe cycle of $\varphi$ such that
$E(K_0) \cap E(K_1) \neq \emptyset$ (equivalently, $K_0$ and $K_1$
share at least one colour-$a$ edge). If $h_\varphi$ is constant on
$V(K_0)$, then $h_\varphi$ is \emph{not} constant on $V(K_1)$.
\end{conjecture}

\begin{remark}[Disproof of
Conjecture~\ref{conj:no-two-constant-kempe-cycles}]
\label{rem:no-two-constant-kempe-cycles-counterexample}
Conjecture~\ref{conj:no-two-constant-kempe-cycles} is \emph{false}:
there exists a cubic plane graph $H$ with a proper $3$-edge-colouring
$\varphi$ admitting an $\{a, b\}$-Kempe cycle $K_0$ and an
$\{a, c\}$-Kempe cycle $K_1$ which share a colour-$a$ edge and on which
$h_\varphi$ is simultaneously constant on $V(K_0)$ and on $V(K_1)$. A
concrete counterexample is recorded in
Figure~\ref{fig:no-two-constant-kempe-counterexample}.

The (partial) proof attempt below establishes the constraint
$|E(K_0) \cap E(K_1)| \geq 2$ (Step~2) and closes the sub-case where
two shared a-edges are consecutive on \emph{both} cycles
(``Case~A''/Step~4), but the general claim fails because in the
counterexample no pair of shared a-edges is consecutive on both
cycles --- the $K_1$-arc between two $K_0$-consecutive shared a-edges
itself passes through other shared a-edges, breaking the lune-face
assumption.
\end{remark}

\begin{figure}[h]
\centering
% TODO: replace placeholder with the actual counterexample drawing
% (e.g., the whiteboard photo or a TikZ rendering).
\fbox{\parbox{0.7\textwidth}{\centering
\emph{Placeholder for the counterexample figure.}\\[2pt]
A cubic plane graph $H$ with three edge colours
(red, blue, teal) showing two Kempe cycles sharing a colour edge,
on which $h_\varphi$ is simultaneously constant on both cycles.\\
See \texttt{figures/no-two-constant-kempe-counterexample.\{png,pdf\}}
once the image is committed to the repo.}}
\caption{Counterexample to
Conjecture~\ref{conj:no-two-constant-kempe-cycles}.}
\label{fig:no-two-constant-kempe-counterexample}
\end{figure}

\begin{proof}[Partial proof attempt (now superseded by
Remark~\ref{rem:no-two-constant-kempe-cycles-counterexample})]
\textbf{Note.}
Conjecture~\ref{conj:no-two-constant-kempe-cycles} is false (see the
counterexample in
Remark~\ref{rem:no-two-constant-kempe-cycles-counterexample} /
Figure~\ref{fig:no-two-constant-kempe-counterexample}). The argument
below is preserved as partial progress: Steps~1--2 are unconditional
and Step~4 closes the sub-case where some pair of shared a-edges is
consecutive on both $K_0$ and $K_1$.

Suppose for contradiction that $h_\varphi$ is constant on both
$V(K_0)$ and $V(K_1)$, and that $K_0, K_1$ share a colour-$a$ edge
$e = (u, w)$. Then $u, w \in V(K_0) \cap V(K_1)$ are consecutive on
both cycles. Since the two constants agree at the shared vertex $u$,
they agree everywhere on $V(K_0) \cup V(K_1)$; WLOG
$h_\varphi \equiv +1$ on $V(K_0) \cup V(K_1)$, so the CW edge order at
every such vertex is $(a, b, c)$.

Orient both cycles so that they leave $u$ along $e$: write the $K_0$
walk as $u = v_0 \xrightarrow{e} w = v_1 \to v_2 \to \cdots \to
v_{L_0 - 1} \to v_0$, and the $K_1$ walk as $u = u_0 \xrightarrow{e}
w = u_1 \to u_2 \to \cdots \to u_{L_1 - 1} \to u_0$. Let
$F_R(e), F_L(e)$ be the two faces of $H$ incident to $e$, with $F_R$
on the right and $F_L$ on the left of the $u \to w$ traversal.

\textbf{Step 1 (local sides at $u, w$).} The CW-order $(a, b, c)$ at
$u$ and $w$ partitions the faces of $H$ at each endpoint into three
wedges. Direct inspection (cf.\ the proof of
Lemma~\ref{lem:kempe-heawood-constant}) gives
\[
F_R(e) = F_{ab}^u = F_{ca}^w, \qquad F_L(e) = F_{ca}^u = F_{ab}^w,
\]
where $F_{\alpha\beta}^v$ is the face of $H$ at $v$ in the CW wedge
between the colour-$\alpha$ and colour-$\beta$ edges. Consequently:
\begin{itemize}
\item $e_c^u$ lies between $F_{bc}^u$ and $F_{ca}^u = F_L(e)$, so $e_c^u$
is on the side of $K_0$ containing $F_L(e)$ near $u$; call this side
$\mathrm{In}(K_0)$.
\item $e_c^w$ lies between $F_{bc}^w$ and $F_{ca}^w = F_R(e)$, so
$e_c^w$ is on the side $\mathrm{Out}(K_0)$ containing $F_R(e)$ near $w$.
\item Symmetrically, $e_b^u$ is on the side of $K_1$ containing
$F_R(e)$, call this $\mathrm{Out}(K_1)$, and $e_b^w$ is on the side
$\mathrm{In}(K_1)$ containing $F_L(e)$.
\end{itemize}
This recovers exactly the conclusion of
Lemma~\ref{lem:kempe-heawood-constant} applied to $(u, w)$ on each
cycle.

\textbf{Step 2 (forced crossings).} Consider $K_1 \setminus e$, the
path from $u$ to $w$ obtained by removing the open edge $e$ from
$K_1$. By Step~1, this path leaves $u$ on the $\mathrm{In}(K_0)$ side
and arrives at $w$ on the $\mathrm{Out}(K_0)$ side. Since $K_0$
separates the plane into its two sides and $K_1 \setminus e$ is a
continuous arc, the path must intersect $V(K_0)$ at an odd number of
points strictly between $u$ and $w$ along the $K_1$-walk.

At any such intersection $x \in V(K_0) \cap V(K_1) \setminus \{u, w\}$,
$K_1$ uses the colour-$a$ edge at $x$ (since $K_1$ uses only colours
$a, c$ and only colour-$a$ edges can lie on $K_0$). That colour-$a$
edge is therefore a shared edge $e^* \in E(K_0) \cap E(K_1)$ with
$e^* \neq e$; both endpoints of $e^*$ lie in $V(K_0) \cap V(K_1)$.

So $|E(K_0) \cap E(K_1)| - 1$ equals the (odd) number of crossings,
giving
\[
|E(K_0) \cap E(K_1)| \text{ is even, and } \geq 2.
\]
The symmetric argument applied to $K_0 \setminus e$ crossing $K_1$
yields the same conclusion.

\textbf{Step 3 (Heawood face-sum on each face of $K_0 \cup K_1$).}
View $K_0 \cup K_1$ as a planar subgraph of $H$ and consider any face
$\Phi$ of this subgraph. Let $F_\Phi$ be the set of $H$-faces lying
inside (the closed region of) $\Phi$. Applying Heawood's classical
face-sum identity
$\sum_{v \in \partial f} h_\varphi(v) \equiv 0 \pmod 3$
\cite{Heawood1898}
to every $f \in F_\Phi$ and summing gives
\[
\sum_{f \in F_\Phi} \sum_{v \in \partial f} h_\varphi(v) \;=\;
\sum_{v} \mathrm{mult}_\Phi(v)\, h_\varphi(v) \;\equiv\; 0 \pmod 3,
\]
where $\mathrm{mult}_\Phi(v)$ counts the number of $H$-faces in
$F_\Phi$ whose boundary contains $v$.

A direct case-check on the cubic vertex structure gives:
\begin{itemize}
\item $\mathrm{mult}_\Phi(v) = 3$ if $v$ is strictly interior to $\Phi$
(all three $H$-faces at $v$ lie in $F_\Phi$);
\item $\mathrm{mult}_\Phi(v) = 1$ if $v$ is a degree-$3$
(shared, branching) vertex of $K_0 \cup K_1$ on $\partial\Phi$ (only
one of $v$'s three wedges lies in $\Phi$);
\item $\mathrm{mult}_\Phi(v) = 2$ if $v$ is a degree-$2$ (non-shared)
vertex of $K_0 \cup K_1$ on $\partial\Phi$ \emph{and} $v$'s third edge
points into $\Phi$ (the third edge subdivides $v$'s wedge in $\Phi$
into two $H$-faces);
\item $\mathrm{mult}_\Phi(v) = 1$ if $v$ is a degree-$2$ non-shared
boundary vertex with its third edge pointing into the opposite face.
\end{itemize}

Under the contradiction hypothesis $h_\varphi \equiv +1$ on
$V(K_0) \cup V(K_1) \supseteq \partial\Phi$, the boundary contribution
collapses to
\[
\sigma_\Phi + \nu_{1,\Phi} + 2\,\nu_{2,\Phi}
\;=\; \ell_\Phi + \nu_{2,\Phi}
\;\equiv\; 0 \pmod 3,
\]
where $\sigma_\Phi$ counts shared boundary vertices of $\Phi$,
$\nu_{1,\Phi}$ and $\nu_{2,\Phi}$ count non-shared boundary vertices
with third edge pointing out of / into $\Phi$ respectively, and
$\ell_\Phi$ is the boundary length of $\Phi$. (The interior
contribution is a multiple of $3$ and drops out.) Hence
\begin{equation}
\label{eq:face-sum-mod3}
\nu_{2,\Phi} \;\equiv\; -\ell_\Phi \pmod 3
\quad\text{for every face } \Phi \text{ of } K_0 \cup K_1.
\end{equation}

\textbf{Step 4 (lune-face contradiction, ``Case A'' sub-case).}
Suppose there exist two shared a-edges $e_1 = (p, p')$ and
$e_2 = (q, q')$ which are consecutive on \emph{both} the $K_0$-walk
\emph{and} the $K_1$-walk (so the $K_0$-arc from $p'$ to $q$ and the
$K_1$-arc from $p'$ to $q$ both have all-non-shared interior). In
particular, when $|E(K_0) \cap E(K_1)| = 2$ this is automatic, but in
general it is an extra hypothesis. Let $A_1$ be the $K_0$-arc from
$p'$ to $q$ of length $m$. The arc begins with the colour-$b$ edge at
$p'$ and ends with the colour-$b$ edge at $q$, so $m$ is odd. Two
cases for the cyclic order in which $K_1$ visits $\{p, p', q, q'\}$:

\begin{description}
\item[Case A.] $K_1$ visits them in the same cyclic order
$p, p', q, q'$ as $K_0$. Then $K_1$ has a $K_1$-arc $B_1$ from $p'$
to $q$ (between $e_1$ and $e_2$ on the $K_1$-walk), of odd length
$n$, whose intermediate vertices are all non-shared.
\item[Case B.] $K_1$ visits them in the opposite order
$p, p', q', q$. Then $K_1$'s arcs between $e_1, e_2$ go from $p'$ to
$q'$ and from $q$ to $p$; they do not share endpoints with $A_1$.
\end{description}

\emph{Case A is impossible.} The arcs $A_1$ and $B_1$ share both
endpoints $p', q$ and meet only at those endpoints, so they bound a
``lune'' face $\Phi^*$ of $K_0 \cup K_1$ whose boundary has exactly
two corners (both of wedge type $(b, c)$) and length $m + n$. Now
\begin{itemize}
\item Every intermediate vertex of $B_1$ is a non-shared $K_1$-vertex,
hence not on $K_0$, hence lies in one of the two open regions of
$\mathbb{R}^2 \setminus K_0$. Since $B_1$ is a connected path joining
$p', q \in V(K_0)$ and never visits $V(K_0)$ in its interior,
$B_1 \setminus \{p', q\}$ lies entirely on \emph{one} side of $K_0$.
In particular the colour-$c$ edges at $p'$ and at $q$ (the first
and last edges of $B_1$) point into the \emph{same} side of $K_0$.
\item By Lemma~\ref{lem:kempe-heawood-constant} applied along the
$K_0$-arc from $p'$ to $q$, consecutive colour-$c$ non-cycle edges
alternate sides. After $m$ steps with $m$ odd, the colour-$c$ edges
at $p'$ and at $q$ lie on \emph{opposite} sides of $K_0$.
\end{itemize}
These two conclusions are incompatible, contradicting the assumption
that both $K_0$ and $K_1$ have constant $h_\varphi$ in Case A.

\textbf{Step 5 (Case B --- TBD).} In Case B, the four faces of
$K_0 \cup K_1$ are each three-corner ``triangles'' bounded by one
$K_0$-arc, one $K_1$-arc, and one shared a-edge (one corner each of
types $(a,b)$, $(b,c)$, $(c,a)$). For such a face the
Step~4 lune argument does not apply: $A_1$ and the corresponding
$K_1$-arc $B_1$ no longer share both endpoints, and both
Lemma~\ref{lem:kempe-heawood-constant} alternations and the mod-$3$
constraint~\eqref{eq:face-sum-mod3} can be checked to be
consistent on the parity counts. The contradiction in this case is
\emph{open}.

\emph{Empirical note.} The theorem's hypothesis is never observed:
across the $142{,}812$ chord-apex+Kempe colourings of reduced duals
with $|V(G)| \le 20$, ``$h_\varphi$ constant on $V(K_b)$'' fails on
every colouring (see \texttt{experiments/check\_constancy\_obstruction.py}
and Remark~\ref{rem:heawood-empirical}).
\end{proof}

\begin{remark}[Empirical near-proof of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} via Corollary~\ref{cor:single-cycle-non-constancy}]
\label{rem:heawood-empirical}
\sloppy
By Corollary~\ref{cor:single-cycle-non-constancy},
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
follows from the (a~priori weaker) structural claim:
\emph{for every chord-apex+Kempe colouring $\varphi$ of every reduced
dual $\widehat{G}'_{v,i}$, $h_\varphi$ is not constant on $V(K_b)$
(equivalently, not constant on $V(K_c)$).} We have verified this claim
computationally on all chord-apex+Kempe colourings of reduced duals
with $|V(G)| \le 20$ (including the six Holton--McKay duals at
$n = 21$ as a special case); see
\texttt{experiments/check\_heawood\_on\_kempe.py} and
\texttt{experiments/check\_constancy\_obstruction.py}.
\begin{center}
\small
\renewcommand{\arraystretch}{1.15}
\begin{tabular}{r|r|r|r|l}
$n$ & \#col.\ tested
    & \#non-const. on $V(K_b)$
    & \#non-const. on $V(K_c)$ & status \\
\hline
$14$ & $216$       & $216$       & $216$       & all non-constant \\
$16$ & $864$       & $864$       & $864$       & all non-constant \\
$17$ & $4{,}650$   & $4{,}650$   & $4{,}650$   & all non-constant \\
$18$ & $8{,}070$   & $8{,}070$   & $8{,}070$   & all non-constant \\
$19$ & $21{,}138$  & $21{,}138$  & $21{,}138$  & all non-constant \\
$20$ & $107{,}874$ & $107{,}874$ & $107{,}874$ & all non-constant \\
\hline
total ($n \le 20$) & $142{,}812$ & $142{,}812$ & $142{,}812$ & \\
\end{tabular}
\end{center}
\noindent In particular, $h_\varphi$ is non-constant on $V(K_b)$ alone
in every tested colouring (and likewise on $V(K_c)$); by
Corollary~\ref{cor:single-cycle-non-constancy} each such colouring
admits a Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
witness. This gives an empirical near-proof of the conjecture for
$|V(G)| \le 20$ independent of (and consistent with) the direct
witness-search check of Remark~\ref{rem:conj-3-6-empirical}. A
structural proof of non-constancy on $V(K_b)$ (or on $V(K_c)$) would
convert this into a proof of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
proper.
\end{remark}

\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{Heawood1898}
P.~J.~Heawood,
\emph{On the four-colour map theorem},
Quart. J.~Pure Appl. Math. \textbf{29} (1898), 270--285.

\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}