Files
math-research/papers/face_monochromatic_pairs/paper.tex
T
didericis cfc53dcbe2 face_monochromatic_pairs: add Lemma 5.3 (constancy on both Kempe cycles)
Follow-up to Lemma 5.2. States that if Conjecture 5.1 has no
clauses-(1)-(3) witness for (G, G'^_{v,i}, phi), then h_phi is
constant on both Kempe cycles through merged, and the two constants
agree (since merged is on both cycles, so its endpoints force the
constants to match).

Proof is the V1-direction of the case analysis: differing h_phi on
either K_b or K_c reproduces a clause-(1)-(3) witness by the same
F_R/F_L geometry as Lemma 5.2's proof but with the hypothesis
"h_phi(v_0) != h_phi(v_1)", under which the matching-colour edges
land on the SAME face of e. Case B's merged-incidence corner is
handled by choosing a differing-Heawood pair away from merged's
endpoints.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-24 22:45:26 -04:00

995 lines
46 KiB
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{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}