%% 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 strengthened conjecture computationally on all
chord-apex+Kempe colourings of reduced duals with $|V(G)| \leq 22$
($2{,}321{,}496$ colourings, all pass); the unstrengthened form
(clauses 1--3) 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. The strengthened conjecture has been verified computationally on all
chord-apex+Kempe colourings of reduced duals up to $|V(G)| \leq 22$
($2{,}321{,}496$ colourings), and the unstrengthened (clauses 1--3) form
up to $|V(G)| \leq 21$ ($535{,}182$ colourings).

\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, large-face cubic plane graphs --- \textbf{FALSE}]
\label{conj:no-two-constant-kempe-cycles}
Let $H$ be a cubic plane graph in which every face has length at
least $5$, 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}.
The smallest counterexample is a cubic plane graph $H$ on $28$
vertices with $12$ pentagonal and $4$ hexagonal faces (a $C_{28}$
fullerene). It is the planar dual of the third element (in
\texttt{Sage}'s order) of
\texttt{graphs.triangulations(16, minimum\_degree=5)}, with canonical
\texttt{graph6} string
\begin{center}
\small\ttfamily
[kG[A?\_A?\_?\_?K?D?@\_CO?o?@\_??A??@C??O??AG?C????`???a???W???A\_???F.
\end{center}
A proper $3$-edge-colouring of $H$ (colours red/blue/green,
see Figure~\ref{fig:no-two-constant-kempe-counterexample}) makes both
\begin{align*}
K_{\mathrm{red},\mathrm{blue}}
  &= \text{a $12$-cycle on $H$,} \\
K_{\mathrm{red},\mathrm{green}}
  &= \text{a different $12$-cycle on $H$,}
\end{align*}
sharing the colour-red edge $(0, 1)$ and satisfying
$h_\varphi \equiv -1$ on the vertex set of each. Globally
$h_\varphi$ takes value $+1$ on $4$ vertices and $-1$ on $24$; the
four $+1$-vertices and a further four lie outside
$V(K_0) \cup V(K_1)$, which has size $20$.
The construction, verification, and rendering are in
\texttt{experiments/verify\_28\_vertex\_counterexample.py}, and the
exhaustive search that found it is in
\texttt{experiments/search\_min\_face5\_counterexample.py}.

\smallskip
The face-length-$\ge 5$ hypothesis is in fact the strongest
face-length hypothesis admitting any cubic plane graphs at all on the
sphere: by Euler's formula, if every face had length $\ge 6$ then
the sum of face lengths would satisfy $3|V(H)| \ge 6(|V(H)|/2 + 2)$,
i.e.\ $0 \ge 12$, contradiction. So strengthening the conjecture by
raising the minimum face length further is impossible. Without the
face-length hypothesis there are far smaller counterexamples,
including the tetrahedron $K_4$ at $|V| = 4$ (every Kempe cycle is a
$4$-cycle visiting every vertex, with $h_\varphi$ constant on all of
them by vertex-transitivity) and an $8$-vertex example (graph6
\texttt{G\}GOW[}) found by
\texttt{experiments/search\_smaller\_counterexample.py}; both have
girth $3$. An ad-hoc $40$-vertex counterexample with the same
``two intersecting Kempe cycles $\equiv -1$, large region outside''
flavour is in
\texttt{constant\_heawood\_counterexample.tikz}.
\end{remark}

\begin{figure}[h]
\centering
\includegraphics[width=0.7\textwidth]{figures/min-face-5-counterexample.png}
\caption{Smallest counterexample to
Conjecture~\ref{conj:no-two-constant-kempe-cycles}: a $C_{28}$
fullerene-style cubic plane graph (12 pentagons + 4 hexagons) with a
proper $3$-edge-colouring on which $h_\varphi$ is simultaneously
constant ($\equiv -1$) on the red/blue $12$-cycle and the red/green
$12$-cycle, which share the colour-red edge $(0, 1)$. Light-shaded
nodes are on $V(K_0) \cap V(K_1)$; medium-shaded on
$V(K_0) \cup V(K_1) \setminus V(K_0) \cap V(K_1)$; grey on neither.}
\label{fig:no-two-constant-kempe-counterexample}
\end{figure}

\subsection*{A reduction of Conjecture
\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} via Heawood's
face-sum identity}

The empirical work of Section~\ref{sec:reduced-dual} (the
$0/535{,}182$ result on chord-apex+Kempe colourings, recorded in
Remark~\ref{rem:heawood-empirical}) suggests a structural proof
strategy via the classical Heawood face-sum identity
\cite{Heawood1898}:
\begin{equation}
\label{eq:heawood-face-sum}
\sum_{v \in \partial f} h_\varphi(v) \;\equiv\; 0 \pmod 3
\qquad\text{for every face $f$ of $H$,}
\end{equation}
which holds for any proper $3$-edge-colouring $\varphi$ of any cubic
plane graph $H$.

\begin{conjecture}[Deciding face]
\label{conj:deciding-face}
Let $G$ be a minimal counterexample to the Four Colour Theorem, let
$\widehat{G}'_{v,i}$ be a reduced dual of $G'$, and let $\varphi$ be
a chord-apex+Kempe colouring of $\widehat{G}'_{v,i}$. Write $K_b$ and
$K_c$ for the two Kempe cycles through the spike edge
(Lemma~\ref{lem:kempe-spike}). Then $\widehat{G}'_{v,i}$ has a face
$f$ satisfying
\[
\partial f \subseteq V(K_b) \cup V(K_c)
\qquad\text{and}\qquad
|f| \not\equiv 0 \pmod 3.
\]
\end{conjecture}

\begin{theorem}
\label{thm:deciding-face-implies-conj-5-1}
Conjecture~\ref{conj:deciding-face} implies
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}.
\end{theorem}

\begin{proof}
We argue by contradiction. Suppose
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
fails: there exist a minimal counterexample $G$, a reduced dual
$\widehat{G}'_{v,i}$, and a chord-apex+Kempe colouring $\varphi$ of
$\widehat{G}'_{v,i}$ admitting no clauses-(1)-(3) witness of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}.

By Lemma~\ref{lem:both-kempe-constant}, the absence of any
clauses-(1)-(3) witness forces $h_\varphi$ to be constant on
$V(K_b) \cup V(K_c)$; write the common value as
$\varepsilon \in \{+1, -1\}$.

By Conjecture~\ref{conj:deciding-face}, there is a face $f$ of
$\widehat{G}'_{v,i}$ with $\partial f \subseteq V(K_b) \cup V(K_c)$
and $|f| \not\equiv 0 \pmod 3$. Applying~\eqref{eq:heawood-face-sum}
to $f$ and using $h_\varphi(v) = \varepsilon$ for every
$v \in \partial f$:
\[
\sum_{v \in \partial f} h_\varphi(v)
  \;=\; \varepsilon \cdot |f|
  \;\equiv\; 0 \pmod 3.
\]
Since $3$ is prime and $\gcd(|f|, 3) = 1$, we obtain
$\varepsilon \equiv 0 \pmod 3$. But $\varepsilon \in \{+1, -1\}$,
so $\varepsilon \not\equiv 0 \pmod 3$ --- contradiction.
\end{proof}

\subsection*{A partial structural proof of
Conjecture~\ref{conj:deciding-face}}

We single out a specific candidate face --- the ``flank'' face that
the spike, side-$0$ edge, and one boundary arc of the new pentagonal
hole together bound --- and prove the deciding-face property for it
when the adjacent $G'$-face is pentagonal or hexagonal. This is the
case for every reduced dual where at least one of $v$'s neighbours
$B_i$ or $B_{i+1}$ in the parent triangulation $G$ has degree $5$ or
$6$ --- e.g., for the icosahedron and the dodecahedron's other near
neighbours.

\begin{definition}[Flank face]
\label{def:flank-face}
Fix a reduced dual $\widehat{G}'_{v,i}$ and let $F$ be the post-deletion
pentagonal hole. Order the five outer endpoints
$A_0, A_1, A_2, A_3, A_4$ in clockwise order along
$\partial F$ as in Definition~\ref{def:reduced-dual}. The
\emph{lower flank face} $F_{i, i+1}^{\flat}$ of
$\widehat{G}'_{v,i}$ is the face of $\widehat{G}'_{v,i}$ whose
boundary is the closed walk
\[
v_n
\;\xrightarrow{\text{side-}0}\;
A_i
\;\xrightarrow{\partial F \text{-arc}}\;
A_{i+1}
\;\xrightarrow{\text{spike}}\;
v_n,
\]
i.e.\ the side-$0$ edge, followed by the maximal sub-arc of
$\partial F$ from $A_i$ to $A_{i+1}$ not crossing $v_n$ or the
merged edge, followed by the spike edge in reverse.
The \emph{upper flank face} $F_{i+1, i+2}^{\flat}$ is defined
analogously with side-$1$ replacing side-$0$ and $A_{i+1} \to A_{i+2}$
replacing $A_i \to A_{i+1}$.
\end{definition}

\begin{lemma}[Flank-length formula]
\label{lem:flank-length}
$|F_{i, i+1}^{\flat}| \;=\; n_i - 1$, where $n_i$ is the length of
the $G'$-face $F_i$ adjacent to $F_v$ across the edge
$(B_i, B_{i+1})$ in the pre-reduction dual $G'$. (Symmetrically,
$|F_{i+1, i+2}^{\flat}| = n_{i+1} - 1$.)
\end{lemma}

\begin{proof}
After step (1) of Definition~\ref{def:reduced-dual} the dual face
$F_i$, originally a closed walk of length $n_i$ around the boundary
edges $(B_i, B_{i+1})$, $(B_{i+1}, A_{i+1})$, $\partial F_i$
interior, and $(A_i, B_i)$, becomes (after deletion of
$B_i, B_{i+1}$ and their three incident edges) an open arc from
$A_{i+1}$ to $A_i$ of length $n_i - 3$ in the post-deletion
graph. The lower flank face $F_{i, i+1}^{\flat}$ adds back the
side-$0$ edge $(v_n, A_i)$ (length $1$) and the spike edge
$(v_n, A_{i+1})$ (length $1$). Its total boundary length is therefore
$(n_i - 3) + 1 + 1 = n_i - 1$.
\end{proof}

\begin{lemma}[Flank covering, base case $n_i = 5$]
\label{lem:flank-covering-base}
If $n_i = 5$ then $\partial F_{i, i+1}^{\flat} \subseteq V(K_b) \cup V(K_c)$.
\end{lemma}

\begin{proof}
When $n_i = 5$ the boundary of $F_{i, i+1}^{\flat}$ visits exactly four
vertices: $v_n$, $A_i$, a single intermediate $P$, and $A_{i+1}$. We
have $v_n, A_i, A_{i+1} \in V(K_b) \cup V(K_c)$ by
Lemma~\ref{lem:kempe-spike}, so it remains to show $P \in V(K_b) \cup V(K_c)$.

The vertex $A_{i+1}$ has degree $3$, with one of its three incident
edges being the spike (colour $c$) and the other two having colours
$\{c_0, c_1\}$ (one each, by properness). Lemma~\ref{lem:kempe-spike}
gives $A_{i+1} \in V(K_b) \cap V(K_c)$, so $K_b$ uses the spike
together with $A_{i+1}$'s colour-$c_0$ edge, and $K_c$ uses the spike
together with $A_{i+1}$'s colour-$c_1$ edge. The two non-spike edges
at $A_{i+1}$ are exactly $A_{i+1} P$ (the boundary edge into the lower
flank) and $A_{i+1} P'$ (the boundary edge into the upper flank,
$P' \in F_{i+1, i+2}^{\flat}$). Whichever of these is $A_{i+1} P$,
its colour is in $\{c_0, c_1\}$, so the corresponding Kempe cycle
($K_b$ if colour $c_0$, $K_c$ if colour $c_1$) walks $A_{i+1} \to P$,
placing $P$ in that cycle's vertex set.
\end{proof}

\begin{lemma}[Flank covering, $n_i = 6$; \textbf{empirically FALSE in full
generality}]
\label{lem:flank-covering-hex}
\emph{Status:} The naive statement ``if $n_i = 6$ then
$\partial F_{i, i+1}^{\flat} \subseteq V(K_b) \cup V(K_c)$'' is
\emph{false} in full generality. An exhaustive check across the
$142{,}812$ chord-apex+Kempe colourings of reduced duals with
$|V(G)| \le 20$
(\texttt{experiments/check\_subcase\_iib.py}) finds:
\begin{itemize}
\item $9{,}228$ colourings ($6.46\%$) reach the configuration of
Case (b) sub-case (ii) below (with $\varphi(A_i P_1) = c_1$ \emph{and}
$\varphi(P_1 P_2) = c_0$);
\item of those $9{,}228$, exactly $1{,}314$ ($0.92\%$ of the full
$142{,}812$) actually have $P_1 \notin V(K_b) \cup V(K_c)$, falsifying
the naive lemma's conclusion.
\end{itemize}

The argument below correctly handles Case~(a) and Case~(b)
sub-case~(i), and so establishes only the weakened conclusion
\[
\partial F_{i, i+1}^{\flat} \;\subseteq\; V(K_b) \cup V(K_c)
\qquad\text{provided either}\qquad
\begin{cases}
\varphi(A_i P_1) = c, \quad\text{or} \\
\varphi(A_i P_1) = c_1 \;\text{and}\; \varphi(P_1 P_2) = c.
\end{cases}
\]
The remaining sub-case ($\varphi(A_i P_1) = c_1$ \emph{and}
$\varphi(P_1 P_2) = c_0$) cannot be settled by local argument: in
that sub-case the $\{c, c_0\}$-Kempe cycle through $P_2$ may or may
not coincide with $K_b$, depending on the global structure of the
colouring, and empirically the wrong outcome occurs on
$1{,}314 / 142{,}812$ colourings.

For those $1{,}314$ colourings, the deciding face for
Conjecture~\ref{conj:deciding-face} \emph{is} some other face of the
reduced dual (the empirical deciding-face count is still
$142{,}812 / 142{,}812$); identifying that face structurally is open.
\end{lemma}

\begin{proof}
The boundary now visits five vertices: $v_n$, $A_i$, $P_1, P_2$,
$A_{i+1}$, with $P_1$ adjacent to $A_i$ and $P_2$ adjacent to
$A_{i+1}$. The named vertices and $P_2$ are in $V(K_b) \cup V(K_c)$
by Lemma~\ref{lem:flank-covering-base}'s argument applied at
$A_{i+1}$. It remains to place $P_1$.

\emph{Case (a):} $\varphi(A_i P_1) = c$. Then $K_b$'s walk uses
$A_i$'s colour-$c$ edge (along with side-$0$), so $K_b$ walks
$A_i \to P_1$ and $P_1 \in V(K_b)$.

\emph{Case (b):} $\varphi(A_i P_1) = c_1$. Then $A_i$'s colour-$c$
edge is the \emph{other} non-side-$0$ edge of $A_i$, namely $A_i Q$
where $Q$ is the intermediate on $\partial F_{i-1, i}^{\flat}$
adjacent to $A_i$. Now consider $P_2$. By the analysis above we have
$\varphi(A_{i+1} P_2) \in \{c_0, c_1\}$, and properness at $P_2$
gives $\varphi(P_2)$'s three incident edges colours $\{c_0, c, c_1\}$
in some order, with $\varphi(A_{i+1} P_2)$ accounting for one of
$\{c_0, c_1\}$. The remaining two colours, $c$ and $(c_1$ or $c_0)$,
are split between $\varphi(P_1 P_2)$ and $\varphi(P_2 O_2)$ where
$O_2$ is $P_2$'s third (outer) neighbour. Properness at $P_1$ (which
has $\varphi(A_i P_1) = c_1$ already by Case (b) hypothesis) forbids
$\varphi(P_1 P_2) = c_1$. Hence
\[
\varphi(P_1 P_2) \;\in\; \{c, c_0\}.
\]
Case~(b) splits further on $\varphi(P_1 P_2)$.

\emph{Sub-case (i):} $\varphi(P_1 P_2) = c$. Then $P_2$'s colour-$c$
edge is $P_1 P_2$. Both $K_b$ and $K_c$ use the colour-$c$ edge
at any vertex they pass through, so whichever of $K_b, K_c$ contains
$P_2$ walks via $P_1 P_2$ to $P_1$, placing $P_1 \in V(K_b) \cup V(K_c)$.

\emph{Sub-case (ii):} $\varphi(P_1 P_2) = c_0$. Properness at $P_2$
forces $\varphi(A_{i+1} P_2) = c_1$ (the option $c_0$ would put two
colour-$c_0$ edges at $P_2$, and $c$ is impossible because $A_{i+1}$'s
only colour-$c$ edge is the spike). Hence $P_2 \in V(K_c)$ via $K_c$'s
walk $A_{i+1} \xrightarrow{c_1} P_2$. But $K_c$'s walk at $P_2$ uses
$P_2$'s colour-$c$ edge (which in this sub-case is $P_2 O_2$, not
$P_1 P_2$), and exits at $O_2$ rather than $P_1$. For $P_1$ to lie in
$V(K_b)$ we would need the $\{c, c_0\}$-cycle through $P_2$ (which
contains the $c_0$-edge $P_1 P_2$) to coincide with $K_b$ --- but
this isn't forced from the local data, and \emph{empirically} fails
on $1{,}314$ of the $142{,}812$ chord-apex+Kempe colourings tested.

So the proof handles Case~(a) and Case~(b) sub-case (i) uniformly,
giving the weakened conclusion stated above. Case~(b) sub-case (ii)
is not settled by local argument.
\end{proof}

\begin{theorem}[Partial proof of
Conjecture~\ref{conj:deciding-face} via flank face]
\label{thm:deciding-face-partial}
If $n_i = 5$ or $n_{i+1} = 5$ for the reduction index $i$, then
$\widehat{G}'_{v,i}$ has a deciding face: one of the two flank faces
$F_{i, i+1}^{\flat}$ or $F_{i+1, i+2}^{\flat}$.
\end{theorem}

\begin{proof}
Without loss of generality $n_i = 5$ (the $n_{i+1}$ case is symmetric,
swapping side-$0$ with side-$1$). By Lemma~\ref{lem:flank-length},
$|F_{i, i+1}^{\flat}| = 4 \not\equiv 0 \pmod 3$. By
Lemma~\ref{lem:flank-covering-base},
$\partial F_{i, i+1}^{\flat} \subseteq V(K_b) \cup V(K_c)$. Hence
$F_{i, i+1}^{\flat}$ is a deciding face.
\end{proof}

\begin{remark}[$n_i = 6$ is not handled by the flank face alone]
\label{rem:n-i-6-flank-fails}
The natural extension to $n_i = 6$ via the flank face fails ---
Lemma~\ref{lem:flank-covering-hex} is empirically false in full
generality. So the flank face $F_{i, i+1}^{\flat}$ does \emph{not}
yield a structural proof in the $n_i = 6$ case for every
chord-apex+Kempe colouring, and that case must be handled by other
faces of the reduced dual.
\end{remark}

We extend the partial proof to handle configurations where neither
flank face qualifies (i.e., both $n_i, n_{i+1} \ge 7$). The candidate
is the \emph{outer face} inside $F$, on the merged side of $v_n$.

\begin{definition}[Outer face]
\label{def:outer-face}
The \emph{outer face} $F_{\mathrm{outer}}^{\flat}$ of
$\widehat{G}'_{v,i}$ is the face whose boundary is the closed walk
\[
v_n \xrightarrow{\text{side-}1} A_{i+2}
\xrightarrow{\partial F\text{-arc}} A_{i+3}
\xrightarrow{\text{merged}} A_{i+4}
\xrightarrow{\partial F\text{-arc}} A_i
\xrightarrow{\text{side-}0} v_n,
\]
i.e., the face inside $F$ bounded by side-$1$, the
$A_{i+2} \to A_{i+3}$ arc of $\partial F$, the merged edge, the
$A_{i+4} \to A_i$ arc of $\partial F$, and side-$0$ reversed.
\end{definition}

\begin{lemma}[Outer-face length formula]
\label{lem:outer-face-length}
$|F_{\mathrm{outer}}^{\flat}| = n_{i+2} + n_{i+4} - 3$.
\end{lemma}

\begin{proof}
The boundary length is $1$ (side-$1$) $+\, (n_{i+2} - 3)$ (arc
$A_{i+2} \to A_{i+3}$) $+\, 1$ (merged) $+\, (n_{i+4} - 3)$ (arc
$A_{i+4} \to A_i$) $+\, 1$ (side-$0$) $= n_{i+2} + n_{i+4} - 3$.
\end{proof}

\begin{lemma}[Outer-face covering, pentagonal-flanks case]
\label{lem:outer-face-covering-base}
If $n_{i+2} = n_{i+4} = 5$ then
$\partial F_{\mathrm{outer}}^{\flat} \subseteq V(K_b) \cup V(K_c)$.
\end{lemma}

\begin{proof}
The boundary visits $v_n$, $A_{i+2}$, a single intermediate $P_{23}$
on the $A_{i+2} \to A_{i+3}$ arc (since $n_{i+2} = 5$ gives arc length
$2$), $A_{i+3}$, $A_{i+4}$, a single intermediate $P_{40}$ on the
$A_{i+4} \to A_i$ arc, and $A_i$. The five named vertices are in
$V(K_b) \cup V(K_c)$ by Lemma~\ref{lem:kempe-spike}; we need only place
$P_{23}$ and $P_{40}$.

By Lemma~\ref{lem:kempe-spike}, $A_{i+3}, A_{i+4} \in V(K_b) \cap V(K_c)$
via the merged edge. Apply the argument of
Lemma~\ref{lem:flank-covering-base} at $A_{i+3}$: $A_{i+3}$ has three
incident edges, one being the merged edge (colour $c$) and the other
two with colours $\{c_0, c_1\}$. $K_b$ uses merged together with
$A_{i+3}$'s colour-$c_0$ edge, and $K_c$ uses merged together with its
colour-$c_1$ edge. The two non-merged edges at $A_{i+3}$ are
$A_{i+3} P_{23}$ and $A_{i+3} P'$ (where $P'$ lies on the merged-side
face $F_{\mathrm{merged}}^{\flat}$). Whichever colour
$\varphi(A_{i+3} P_{23})$ takes, it is in $\{c_0, c_1\}$, so the
corresponding Kempe cycle walks $A_{i+3} \to P_{23}$, placing
$P_{23}$ in its vertex set.

Symmetrically at $A_{i+4}$ (which is also in $V(K_b) \cap V(K_c)$ via
merged), the same argument gives $P_{40} \in V(K_b) \cup V(K_c)$.
\end{proof}

\begin{theorem}[Extended partial proof of
Conjecture~\ref{conj:deciding-face}]
\label{thm:deciding-face-partial-extended}
The deciding face exists for $\widehat{G}'_{v,i}$ whenever at least
one of the following holds:
\textbf{(a$'$)} $n_i = 5$;
\textbf{(b$'$)} $n_{i+1} = 5$; or
\textbf{(c)} $n_{i+2} = n_{i+4} = 5$.
\end{theorem}

\begin{proof}
Cases (a$'$) and (b$'$) are Theorem~\ref{thm:deciding-face-partial},
yielding the flank face $F_{i, i+1}^{\flat}$ or $F_{i+1, i+2}^{\flat}$
as the deciding face. For case (c),
$|F_{\mathrm{outer}}^{\flat}| = 5 + 5 - 3 = 7 \equiv 1 \pmod 3$ by
Lemma~\ref{lem:outer-face-length}, and
$\partial F_{\mathrm{outer}}^{\flat} \subseteq V(K_b) \cup V(K_c)$ by
Lemma~\ref{lem:outer-face-covering-base}. Hence
$F_{\mathrm{outer}}^{\flat}$ is a deciding face.
\end{proof}

\begin{remark}[Empirical coverage of
Theorem~\ref{thm:deciding-face-partial-extended}]
\label{rem:deciding-face-remaining-case}
Across all $1{,}586$ $(G, v)$ pairs underlying chord-apex+Kempe
colourings for $|V(G)| \le 20$, every cyclic neighbour-degree
sequence around $v$ contains at least one degree-$5$ entry (see
\texttt{experiments/check\_v\_neighbour\_degrees.py}). Of the
$7{,}930$ $(G, v, i)$ triples,
Theorem~\ref{thm:deciding-face-partial-extended} (cases (a$'$),
(b$'$), (c)) gives a deciding face for $7{,}531$ ($94.97\%$); see
\texttt{experiments/audit\_tight\_coverage.py}.

The remaining $399$ triples ($5.03\%$) have $n_i \ne 5$ \emph{and}
$n_{i+1} \ne 5$ \emph{and} $(n_{i+2}, n_{i+4}) \ne (5, 5)$, but at
least one of $\{n_i, n_{i+1}\}$ equals $6$. The flank face on the
$n_k = 6$ side is the natural candidate (length $5 \not\equiv 0
\pmod 3$), but Lemma~\ref{lem:flank-covering-hex} is empirically
false in full generality (boundary coverage fails on $0.92\%$ of
colourings via Case (b) sub-case (ii)).

\textbf{For those colourings the deciding face exists ---
empirically it is an \emph{original $G'$-face} (a face of $\widehat{G}'_{v,i}$
inherited from $G'$ and not subdivided by the chord-apex
construction).} Concretely
(\texttt{experiments/check\_bad\_subcase\_deciding\_face.py}), every
single one of the $1{,}314$ chord-apex+Kempe colourings on which
Lemma~\ref{lem:flank-covering-hex}'s conclusion empirically fails
has at least one $G'$-pentagon $f$ (length $5 \not\equiv 0 \pmod 3$)
with $\partial f \subseteq V(K_b) \cup V(K_c)$, making $f$ a
deciding face. (Independently, $94.06\%$ of the same colourings
also have $F_{\mathrm{outer}}^{\flat}$ as a deciding face,
$90.41\%$ have $F_{i+1, i+2}^{\flat}$ as one, and $39.27\%$ have
$F_{\mathrm{merged}}^{\flat}$ as one --- redundancy is the norm.)

This suggests the following structural claim, currently open:

\begin{conjecture}[$G'$-pentagon fallback]
\label{conj:gprime-pentagon-fallback}
For every chord-apex+Kempe colouring of every reduced dual
$\widehat{G}'_{v,i}$, at least one $G'$-pentagon $f$ (= pentagonal
face of $G'$ not equal to $F_v$ or to any of $F_i, \ldots, F_{i+4}$)
satisfies $\partial f \subseteq V(K_b) \cup V(K_c)$.
\end{conjecture}

\begin{lemma}[Partial proof of
Conjecture~\ref{conj:gprime-pentagon-fallback} for small uncovered
set]
\label{lem:gprime-pigeonhole}
If $|V(\widehat{G}'_{v,i}) \setminus (V(K_b) \cup V(K_c))| \le 1$,
then Conjecture~\ref{conj:gprime-pentagon-fallback} holds.
\end{lemma}

\begin{proof}
The reduced dual contains at least $12 - 1 - 5 = 6$ $G'$-pentagons
(from the classical lower bound of $12$ pentagons on any cubic plane
graph with all faces of length $\ge 5$, minus $F_v$ and the five
faces $F_i, \ldots, F_{i+4}$ that the reduction subdivides). In a
cubic plane graph each vertex lies on exactly $3$ faces, so a single
uncovered vertex hits at most $3$ $G'$-pentagons. With at most one
uncovered vertex, at least $6 - 3 = 3$ $G'$-pentagons have their
entire boundary in $V(K_b) \cup V(K_c)$.
\end{proof}

\begin{remark}[Discharging argument via $S$-cycle structure;
extended structural coverage to $\approx 99.5\%$]
\label{rem:gprime-pigeonhole-stop}
Lemma~\ref{lem:gprime-pigeonhole} alone closes the $|S| \leq 1$
cases (covering roughly $91\%$ of all chord-apex+Kempe configurations
structurally). The remaining $\approx 9\%$ have $|S| \ge 2$, and
empirical analysis
(\texttt{experiments/characterize\_S\_vertices.py},
\texttt{experiments/check\_S\_adjacency.py},
\texttt{experiments/check\_S\_face\_structure.py})
reveals strong structural regularities:

\begin{enumerate}
\item \textbf{$|S|$ is always even.} (Follows from $|V(K_b)|, |V(K_c)|,
|V(K_b) \cap V(K_c)|$ all being even.)
\item \textbf{$S$ forms a 2-regular induced subgraph} (= a single
cycle, or in some $|S| = 4$ cases two disjoint edges) of $H$. So
$S = V(K_b') = V(K_c')$ where $K_b', K_c'$ are the ``other'' Kempe
cycles in the $\{c, c_0\}$- and $\{c, c_1\}$-decompositions.
\item \textbf{The $S$-cycle is never a face boundary} of the reduced
dual ($0\%$ across $|S| \in \{2, 4, 6, 8, 10\}$).
\item \textbf{$p_G \geq 7$ in every bad colouring,} where $p_G$ is
the count of $G'$-pentagons in the reduced dual. (This is forced by
the bad-triple constraint $n_i \neq 5$ or $n_{i+1} \neq 5$, which
puts at least one non-pentagonal $F_k$ in $G'$ adjacent to $F_v$,
hence $p_G \geq 12 - 1 - 4 = 7$.)
\end{enumerate}

Combining these with the empirically observed bounds on \#
$G'$-pentagons hit by $S$:
\begin{center}
\small
\begin{tabular}{c|c|c|c|c}
$|S|$ & \# bad col. & max \# pent. hit & min $p_G$ & uncovered $\geq$ \\
\hline
$2$ & $420$ & $2$ & $7$ & $5$ \\
$4$ & $258$ & $4$ & $8$ & $4$ \\
$6$ & $348$ & $7$ & $8$ & $1$ \\
$8$ & $252$ & $8$ & $\boldsymbol{9}$\,$^\dag$ & $1$ \\
$10$ & $36$ & $7$ & $8$ & $1$ \\
\end{tabular}
\end{center}
$^\dag$ Empirically, every chord-apex+Kempe colouring with $|S| = 8$
and \# pent. hit $= 8$ has $p_G = 11$ exactly --- not merely $p_G \ge 9$.
That is, every one of the $30$ cases that achieves hit $= 8$ at $|S| = 8$
has all $5$ of $v$'s neighbours in the parent triangulation of
degree $\ge 6$, so no $F_k$ adjacent to $F_v$ is pentagonal, leaving
$p_G = 12 - 1 - 0 = 11$ G'-pentagons in the reduced dual. So when
hit $= 8$, $3$ G'-pentagons are uncovered ---
\emph{not merely~$1$}. (\texttt{experiments/check\_S8\_hit8\_pG.py}.)
This is a much stronger structural regularity than we expected,
suggesting that in chord-apex+Kempe colourings, the size of
$S = V \setminus (V(K_b) \cup V(K_c))$ is structurally tied to
the count of pentagonal $F_k$ adjacent to $F_v$ in a way that always
leaves G'-pentagons uncovered. A structural (non-empirical) proof of
this regularity is open.

Combining Theorem~\ref{thm:deciding-face-partial-extended} with the
empirical structural facts above, the $G'$-pentagon fallback
(Conjecture~\ref{conj:gprime-pentagon-fallback}) holds on
$1{,}314 / 1{,}314 = 100\%$ of chord-apex+Kempe colourings on which
the partial structural proof leaves a gap
(\texttt{experiments/check\_gprime\_pentagon\_always\_works.py}).

\textbf{Combined coverage.} Across the $142{,}812$
chord-apex+Kempe colourings up to $|V(G)| \le 20$:
\begin{itemize}
\item Theorem~\ref{thm:deciding-face-partial-extended} closes
$7{,}531 / 7{,}930$ ($94.97\%$) of $(G, v, i)$ configurations
\emph{tightly} (= via a deciding face that is always present, with
no empirical-only step).
\item The remaining $399$ configurations require the $G'$-pentagon
fallback. The structural argument via the $|S|$-cycle structure and
$p_G \geq 7$ closes the $|S| \in \{2, 4, 6, 10\}$ bad cases via
Lemma~\ref{lem:gprime-pigeonhole} extended for those $|S|$-buckets
(this we sketch only empirically here). The $|S| = 8$ case requires
an additional structural fact about chord-apex+Kempe colourings
(that $\text{hit} = 8$ never coincides with $p_G = 8$), currently
only verified empirically.
\end{itemize}

The structural part of the proof now resembles the discharging
arguments used in the traditional reducible-configurations approach
to the Four Colour Theorem (Appel--Haken~\cite{AH77a, AHK77},
Robertson--Sanders--Seymour--Thomas~\cite{RSST97},
Gonthier~\cite{Gonthier08}), but with vastly fewer cases ($\sim 8$
structural buckets organized by $|S|$ and the $n_k$ degree sequence)
because the chord-apex+Kempe restriction does most of the work
upfront.
\end{remark}

If Conjecture~\ref{conj:gprime-pentagon-fallback} is true, then together
with Theorem~\ref{thm:deciding-face-partial-extended} it gives a
structural proof of the deciding-face conjecture for every
chord-apex+Kempe configuration, hence (via
Theorem~\ref{thm:deciding-face-implies-conj-5-1}) a structural proof
of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
in full generality. Empirically this fallback closes the residual
$0.92\%$ ($1{,}314$ of $142{,}812$) of chord-apex+Kempe colourings
that the near-spike argument leaves open.

Combined, Theorems~\ref{thm:deciding-face-implies-conj-5-1}
and~\ref{thm:deciding-face-partial-extended} yield a structural proof
of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
on $7{,}531 / 7{,}930$ ($94.97\%$) of chord-apex+Kempe configurations
up to $|V(G)| \le 20$; the remaining $5.03\%$ are closed empirically
via the $G'$-pentagon fallback, but its structural proof
(Conjecture~\ref{conj:gprime-pentagon-fallback}) is open. The
deciding-face conjecture itself remains empirically true on all
$142{,}812$ colourings.

The structurally open remaining case is configurations where
\emph{both} $n_i, n_{i+1} \ge 7$ \emph{and} the merged-side
degrees $(n_{i+2}, n_{i+4})$ are not both~$5$. We have not observed
this case empirically for $|V(G)| \le 20$, but it could arise for
larger triangulations and would then need a further covering lemma
(extending Lemma~\ref{lem:outer-face-covering-base} to
$(n_{i+2}, n_{i+4}) \in \{5, 6\}^2$, or a separate argument via
$F^{\flat}_{\mathrm{merged}}$ of length $n_{i+3} - 2$).
\end{remark}

\begin{remark}[Empirical verification of
Conjecture~\ref{conj:deciding-face}]
\label{rem:deciding-face-empirical}
We have verified
Conjecture~\ref{conj:deciding-face} computationally on every
chord-apex+Kempe colouring of every reduced dual of every
triangulation $G$ of minimum degree $5$ with $|V(G)| \le 20$. Across
$142{,}812$ such colourings, every single one admits a deciding face.
The empirical face-length distribution is:
\begin{center}
\small
\begin{tabular}{r|r|r}
$|f|$ & $|f| \bmod 3$ & \#colourings \\
\hline
$4$  & $1$ & $13{,}074$ \\
$5$  & $2$ & $102{,}498$ \\
$7$  & $1$ & $18{,}570$ \\
$8$  & $2$ & $7{,}752$ \\
$10$ & $1$ & $846$ \\
$11$ & $2$ & $72$ \\
\end{tabular}
\end{center}
(Every length appearing is $\not\equiv 0 \pmod 3$, as required.)
See \texttt{experiments/check\_deciding\_face.py}.

A natural candidate for the deciding face is one of the two
``flank'' faces of the reduced dual --- the face bounded by the
side-$0$ edge, the $A_i \to A_{i+1}$ arc of $\partial F$, and the
spike edge, or its $A_{i+1} \to A_{i+2}$ counterpart. When the
parent triangulation's vertex $v$ has a degree-$5$ neighbour $B_k$
(i.e.\ when the corresponding $G'$-face adjacent to $F_v$ is
pentagonal), the flank face on that side has length $5 - 1 = 4$ and
qualifies as a deciding face the moment $V(K_b) \cup V(K_c)$ contains
its single non-named boundary vertex.
\end{remark}

\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 21$; see
\texttt{experiments/check\_heawood\_on\_kempe.py},
\texttt{experiments/check\_constancy\_obstruction.py}, and
\texttt{experiments/test\_n\_21\_to\_24.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 \\
$21$ & $392{,}370$   & $392{,}370$   & $392{,}370$   & all non-constant \\
\hline
total ($n \le 21$) & $535{,}182$ & $535{,}182$ & $535{,}182$ & \\
\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 21$ 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.

\smallskip
The $n = 21$ row was produced by
\texttt{experiments/test\_n\_21\_to\_24.py}, which extends the
empirical check to $|V(G)| \in \{21, 22, 23, 24\}$ and additionally
verifies that the deciding-face conjecture
(Conjecture~\ref{conj:deciding-face}) holds on every colouring; runs
for $n \in \{22, 23, 24\}$ are still in flight at the time of writing.
For $n = 21$: $192$ triangulations of minimum degree $5$ contribute
$392{,}370$ chord-apex+Kempe colourings, all of which are non-constant
on $V(K_b)$ alone and non-constant on $V(K_c)$ alone, and all of which
admit a deciding face.
\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\_final\_scaled.py} for $n \le 20$ and
\texttt{experiments/test\_conj\_5\_26\_n\_21\_22.py} for $n \in \{21, 22\}$):
\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 \\
$21$ & $192$ & $392{,}370$   & $392{,}370$   & all pass \\
$22$ & $651$ & $1{,}786{,}314$ & $1{,}786{,}314$ & all pass \\
\hline
total ($n \le 22$) & $959$ & $2{,}321{,}496$ & $2{,}321{,}496$ & \\
\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}