dual_decomposition: move strengthened conjecture into Section 4 + 4CT implication

- Cut Conjecture 3.8 + Remark 3.9 from Section 3 and move into a new
  Section 4 "The Four Colour Theorem from a strengthened conjecture".
- Add Remark 4.X spelling out the implication: clause (4)(i) forces the
  cyclic colour pattern (c,a,c,b) on the new 4-face f_n, two opposite
  edges of which satisfy the hypothesis of Theorem 3.9 verbatim; case
  (ii) is conjecturally reducible to case (i) via a Kempe swap on the
  {b,c}-cycle through X_1 X_2. Theorem 3.9 then produces the proper
  3-edge-colouring of the contraction, contradicting minimality of G.
- Rewrite the bridge prose into the cubic-contraction definition to
  reference Section 4 forward, rather than the conjecture directly.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-24 13:43:09 -04:00
parent 753af5ffae
commit 440ec9cc86
4 changed files with 172 additions and 133 deletions
@@ -23,17 +23,20 @@
\newlabel{lem:all-distinct-exists}{{3.5}{9}}
\newlabel{conj:face-monochromatic-pair-on-merged-kempe-cycle}{{3.6}{9}}
\newlabel{rem:conj-3-6-empirical}{{3.7}{10}}
\newlabel{conj:face-monochromatic-pair-strengthened}{{3.8}{10}}
\newlabel{rem:conj-3-8-empirical}{{3.9}{11}}
\newlabel{def:cubic-edge-contraction}{{3.10}{11}}
\newlabel{thm:cubic-contraction-4face}{{3.11}{11}}
\newlabel{def:cubic-edge-contraction}{{3.8}{10}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Cubic-graph edge contraction (Definition\nonbreakingspace 3.8\hbox {}). Left: a fragment of a cubic plane graph with the contracted edge $e = uv$ highlighted in red. Middle: deleting $e$ leaves $u$ and $v$ of degree\nonbreakingspace $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.}}{11}{}\protected@file@percent }
\newlabel{fig:cubic-edge-contraction}{{4}{11}}
\newlabel{thm:cubic-contraction-4face}{{3.9}{11}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces The recolouring used in the proof of Theorem\nonbreakingspace 3.9\hbox {}. 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 contracted 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 contraction).}}{12}{}\protected@file@percent }
\newlabel{fig:thm-cubic-contraction-4face}{{5}{12}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{4}{The Four Colour Theorem from a strengthened conjecture}}{12}{}\protected@file@percent }
\newlabel{sec:toward-4ct}{{4}{12}}
\newlabel{conj:face-monochromatic-pair-strengthened}{{4.1}{12}}
\newlabel{tocindent-1}{0pt}
\newlabel{tocindent0}{0pt}
\newlabel{tocindent1}{17.77782pt}
\newlabel{tocindent2}{0pt}
\newlabel{tocindent3}{0pt}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Cubic-graph edge contraction (Definition\nonbreakingspace 3.10\hbox {}). Left: a fragment of a cubic plane graph with the contracted edge $e = uv$ highlighted in red. Middle: deleting $e$ leaves $u$ and $v$ of degree\nonbreakingspace $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.}}{12}{}\protected@file@percent }
\newlabel{fig:cubic-edge-contraction}{{4}{12}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces The recolouring used in the proof of Theorem\nonbreakingspace 3.11\hbox {}. 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 contracted 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 contraction).}}{13}{}\protected@file@percent }
\newlabel{fig:thm-cubic-contraction-4face}{{5}{13}}
\gdef \@abspage@last{13}
\newlabel{rem:conj-3-8-empirical}{{4.2}{13}}
\newlabel{rem:implication-4ct}{{4.3}{13}}
\gdef \@abspage@last{14}
@@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 13:27
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 13:42
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
@@ -299,71 +299,64 @@ Underfull \hbox (badness 6094) in paragraph at lines 498--498
[7] [8 <./fig_alg_step0.png> <./fig_alg_step1.png> <./fig_alg_step2.png>]
[9] [10]
Underfull \hbox (badness 1648) in paragraph at lines 705--710
\OT1/cmr/m/it/10 Remark \OT1/cmr/m/n/10 3.9\OT1/cmr/m/it/10 . \OT1/cmr/m/n/10 T
<fig_cubic_edge_contraction.png, id=75, 950.752pt x 203.159pt>
File: fig_cubic_edge_contraction.png Graphic file (type png)
<use fig_cubic_edge_contraction.png>
Package pdftex.def Info: fig_cubic_edge_contraction.png used on input line 702
.
(pdftex.def) Requested size: 341.9989pt x 73.08138pt.
[11 <./fig_cubic_edge_contraction.png>]
<fig_thm_cubic_contraction_4face.png, id=80, 916.223pt x 417.56pt>
File: fig_thm_cubic_contraction_4face.png Graphic file (type png)
<use fig_thm_cubic_contraction_4face.png>
Package pdftex.def Info: fig_thm_cubic_contraction_4face.png used on input lin
e 777.
(pdftex.def) Requested size: 352.79846pt x 160.78339pt.
[12 <./fig_thm_cubic_contraction_4face.png>]
Underfull \hbox (badness 1648) in paragraph at lines 837--842
\OT1/cmr/m/it/10 Remark \OT1/cmr/m/n/10 4.2\OT1/cmr/m/it/10 . \OT1/cmr/m/n/10 T
he strength-ened con-jec-ture was tested on the same chord-
[]
Underfull \hbox (badness 1014) in paragraph at lines 705--710
Underfull \hbox (badness 1014) in paragraph at lines 837--842
\OT1/cmr/m/n/10 apex+Kempe colour-ings as Re-mark 3.7[]; for each colour-ing we
sought any
[]
<fig_cubic_edge_contraction.png, id=75, 950.752pt x 203.159pt>
File: fig_cubic_edge_contraction.png Graphic file (type png)
<use fig_cubic_edge_contraction.png>
Package pdftex.def Info: fig_cubic_edge_contraction.png used on input line 769
.
(pdftex.def) Requested size: 341.9989pt x 73.08138pt.
LaTeX Warning: `h' float specifier changed to `ht'.
[11]
<fig_thm_cubic_contraction_4face.png, id=79, 916.223pt x 417.56pt>
File: fig_thm_cubic_contraction_4face.png Graphic file (type png)
<use fig_thm_cubic_contraction_4face.png>
Package pdftex.def Info: fig_thm_cubic_contraction_4face.png used on input lin
e 844.
(pdftex.def) Requested size: 352.79846pt x 160.78339pt.
LaTeX Warning: `h' float specifier changed to `ht'.
[12 <./fig_cubic_edge_contraction.png>] [13 <./fig_thm_cubic_contraction_4face.
png>] (./paper.aux) )
[13] [14] (./paper.aux) )
Here is how much of TeX's memory you used:
3112 strings out of 478268
44739 string characters out of 5846347
347356 words of memory out of 5000000
21143 multiletter control sequences out of 15000+600000
3114 strings out of 478268
44776 string characters out of 5846347
346374 words of memory out of 5000000
21145 multiletter control sequences out of 15000+600000
478077 words of font info for 62 fonts, out of 8000000 for 9000
1302 hyphenation exceptions out of 8191
69i,9n,76p,1306b,398s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2022/texmf-dist/fonts/type1/public/ams
fonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf
onts/cm/cmcsc10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf
onts/cm/cmex10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi5.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts
/cm/cmmi7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/c
m/cmmi9.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/
cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cm
r5.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.
pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb
></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pfb></
usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></u
sr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb></usr
/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/l
ocal/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/loc
al/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/loca
l/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/local/
texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/local/t
exlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb>
Output written on paper.pdf (13 pages, 1144897 bytes).
69i,9n,76p,1306b,326s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2022/texmf-dist/fonts/type1/public
/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/
amsfonts/cm/cmcsc10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/
amsfonts/cm/cmex10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/a
msfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
sfonts/cm/cmmi5.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf
onts/cm/cmmi7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi9.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts
/cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/c
m/cmr5.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/c
mr7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8
.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pf
b></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb><
/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></u
sr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr
/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/
local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/lo
cal/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/loc
al/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb>
Output written on paper.pdf (14 pages, 1148116 bytes).
PDF statistics:
172 PDF objects out of 1000 (max. 8388607)
92 compressed objects within 1 object stream
175 PDF objects out of 1000 (max. 8388607)
94 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
61 words of extra memory for PDF output out of 10000 (max. 10000000)
@@ -665,78 +665,11 @@ every $(G, F, i, \varphi)$ with content, all three clauses of the
conjecture hold simultaneously.
\end{remark}
\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, and the following additional clause holds.
Let $X_1, X_2$ be the new vertices subdividing $e_1, e_2$, joined by a new
edge $X_1 X_2$ inside $F$; write $\widehat{G}'^{+}$ for the resulting
modified graph (which has $|V(\widehat{G}'_{v,i})|+2$ vertices and
$|E(\widehat{G}'_{v,i})|+3$ edges, is again cubic and plane, and admits a
proper $3$-edge-colouring). 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. In particular $\varphi'$ agrees with $\varphi$ on every edge of
$\widehat{G}'_{v,i}$ outside that Kempe cycle, and at $X_1$ and $X_2$ the
two subdivision halves take the colours $\{a, b\}$ in the order forced by
propriety. Write $a := \varphi(e_1) = \varphi(e_2)$,
$c := \varphi'(X_1 X_2)$, and let $b$ be the third colour. Let $f_n$ be
the new $4$-edge face of $\widehat{G}'^{+}$ incident to $X_1 X_2$. Then:
\begin{enumerate}
\setcounter{enumi}{3}
\item 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-3.6-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
$12$ & $1$ & $0$ & --- & vacuous \\
$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 \\
\hline
total & $23$ & $13{,}800$ & $13{,}800$ & \\
\end{tabular}
\end{center}
\noindent A subtlety: only about half of the Conjecture-3.6-witnesses
individually satisfy clause (4) on each colouring, but in every case some
witness does. The conjecture is therefore an existential statement at the
witness level, not a property of every witness.
\end{remark}
\medskip
The next definition records a cubic-preserving analogue of edge contraction
which turns out --- under planar duality --- to coincide with simple-graph
contraction on the dual side. It will be useful when reasoning about the
modified graph $\widehat{G}'^{+}$ of Conjecture~\ref{conj:face-monochromatic-pair-strengthened}
and its further reductions.
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}[Cubic-graph edge contraction]
\label{def:cubic-edge-contraction}
@@ -855,4 +788,114 @@ by the contraction).}
\label{fig:thm-cubic-contraction-4face}
\end{figure}
\section{The Four Colour Theorem from a strengthened conjecture}
\label{sec:toward-4ct}
The next conjecture strengthens
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} by adding
a clause that arranges the new $4$-edge face $f_n$ to satisfy the hypotheses
of Theorem~\ref{thm:cubic-contraction-4face}. The strengthening, if true,
would imply the Four Colour Theorem.
\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, and the following additional clause holds.
Let $X_1, X_2$ be the new vertices subdividing $e_1, e_2$, joined by a new
edge $X_1 X_2$ inside $F$; write $\widehat{G}'^{+}$ for the resulting
modified graph (which has $|V(\widehat{G}'_{v,i})|+2$ vertices and
$|E(\widehat{G}'_{v,i})|+3$ edges, is again cubic and plane, and admits a
proper $3$-edge-colouring). 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. In particular $\varphi'$ agrees with $\varphi$ on every edge of
$\widehat{G}'_{v,i}$ outside that Kempe cycle, and at $X_1$ and $X_2$ the
two subdivision halves take the colours $\{a, b\}$ in the order forced by
propriety. Write $a := \varphi(e_1) = \varphi(e_2)$,
$c := \varphi'(X_1 X_2)$, and let $b$ be the third colour. Let $f_n$ be
the new $4$-edge face of $\widehat{G}'^{+}$ incident to $X_1 X_2$. Then:
\begin{enumerate}
\setcounter{enumi}{3}
\item 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-3.6-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
$12$ & $1$ & $0$ & --- & vacuous \\
$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 \\
\hline
total & $23$ & $13{,}800$ & $13{,}800$ & \\
\end{tabular}
\end{center}
\noindent A subtlety: only about half of the Conjecture-3.6-witnesses
individually satisfy clause (4) on each colouring, but in every case some
witness does. The conjecture is therefore an existential statement at the
witness level, not a property of every witness.
\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:cubic-contraction-4face}: they
lie on the $4$-face $f_n$, share no endpoint, and have different
$\varphi'$-colours. Theorem~\ref{thm:cubic-contraction-4face} then produces
a proper $3$-edge-colouring of the cubic-graph edge contraction
$\widehat{G}'^{+} \!\setminus\! e$ along 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:cubic-contraction-4face} now produces a proper
$3$-edge-colouring of the cubic-graph edge contraction of
$\widehat{G}'^{+}$ along 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}
\end{document}