dual_decomposition: split iterated reduction into companion paper

- Move the iterated-reduction algorithm, its two structural lemmas
  (exactly-one-match, all-distinct-exists), and the n=14 trace figure
  into a new companion paper at
  papers/dual_decomposition_iterated_reduction/. Figures and figure
  scripts moved via git mv (history preserved).
- In the main paper, Section 3 ("An iterated reduction") becomes
  Section 3 "Cubic-graph edge contraction" (just the contraction
  definition + 4-face theorem).
- Restructure Section 4 to host both the original face-monochromatic-pair
  conjecture (clauses 1-3) and its strengthening (adds clause 4) as
  separate conjectures, after briefly experimenting with folding them
  into one. The empirical evidence is asymmetric (n<=21 for (1)-(3),
  n<=18 for the full set), which the two-conjecture split presents more
  honestly. The companion-paper reference is now in Section 4's intro.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-24 14:07:08 -04:00
parent 440ec9cc86
commit 83e9dba8ac
13 changed files with 759 additions and 427 deletions
@@ -393,281 +393,11 @@ distinct colours, contradicting Lemma~\ref{lem:chord-apex} applied to
$\varphi'$.
\end{proof}
\section{An iterated reduction}
\section{Cubic-graph edge contraction}
The reduced-dual construction in Definition~\ref{def:reduced-dual} can be
iterated: starting from a proper $3$-edge-colouring $\varphi_1$ of a reduced
dual $\widehat{G}'_{v,i}$, we apply the construction again to that graph at
a pentagonal face whose ten incident edges avoid the four named edges from
the first reduction, extending $\varphi_1$ across the new reduction. The
protected edges accumulate into a set $E$ that grows by four per iteration,
and the process terminates when $E$ has blocked every pentagonal face.
\begin{algorithm}[Iterated reduction with protected edges]
\label{alg:iterated-reduction}
Let $G$ be a triangulation we assume to be a minimal counterexample to the
Four Colour Theorem. The algorithm produces a sequence $H_1, H_2, \dots$ of
cubic plane graphs, proper $3$-edge-colourings $\varphi_t$ of $H_t$, and a
growing set $E$ of protected edges.
\begin{enumerate}
\item[(0)] Form $G' := \mathrm{dual}(G)$, a cubic plane graph.
\item[(1)] Choose a degree-$5$ vertex $v$ of $G$ (equivalently a pentagonal
face $F_v$ of $G'$) and an index $i_1 \in \{0, \dots, 4\}$. Apply
Definition~\ref{def:reduced-dual} to form
$H_1 := \widehat{G'}_{v, i_1}$, and fix any proper
$3$-edge-colouring $\varphi_1$ of $H_1$ (one exists by the minimality
of $G$).
\item[(2)] Initialise $E := \{\text{spike}, \text{side-}0, \text{side-}1,
\text{merged}\}$, the four named edges of the reduction in (1).
\item[(3)] (Iterate.) At step $t \geq 2$, given $H_{t-1}$, $\varphi_{t-1}$,
and $E \subseteq E(H_{t-1})$:
\begin{enumerate}
\item[(a)] Find a pentagonal face $F$ of $H_{t-1}$ whose ten
incident edges --- the five boundary edges of $\partial F$
and the five external edges at $\partial F$ --- are all
outside $E$. If no such $F$ exists, terminate.
\item[(b)] By Lemma~\ref{lem:pentagonal-externals} applied to
$H_{t-1}$ at $F$ under $\varphi_{t-1}$, the external vector
has shape $(a, b, c, c, c)$ up to cyclic rotation. Choose an
index $i_t$ for which
$\varphi_{t-1}(f_{i_t + 3}) = \varphi_{t-1}(f_{i_t + 4})$ and
$\varphi_{t-1}(f_{i_t}), \varphi_{t-1}(f_{i_t + 1}),
\varphi_{t-1}(f_{i_t + 2})$ are three distinct colours.
\item[(c)] Apply Definition~\ref{def:reduced-dual} to $H_{t-1}$ at
$(F, i_t)$ to form $H_t$.
\item[(d)] Extend $\varphi_{t-1}$ to a proper $3$-edge-colouring
$\varphi_t$ of $H_t$: every surviving edge keeps its
$\varphi_{t-1}$-colour, and each new edge takes the unique
colour completing the palette at its endpoint (consistent
across both endpoints of the chord by the choice of $i_t$).
\item[(e)] Add the four named edges of the step-$t$ reduction to
$E$.
\end{enumerate}
\item[(4)] Repeat (3) until termination.
\end{enumerate}
\end{algorithm}
\begin{remark}
\label{rem:alg-invariants}
At each iteration, $|V(H_t)| = |V(H_{t-1})| - 4$ and
$|E(H_t)| = |E(H_{t-1})| - 6$, so $H_t$ shrinks at a fixed rate; the
protected set $|E|$ grows by exactly four; and every protected edge survives
all subsequent reductions. Since the graph is finite, termination is
guaranteed. By Lemma~\ref{lem:pentagonal-externals}, step~(b) never fails:
some valid $i_t$ always exists for any pentagonal face under any proper
colouring. Termination is therefore combinatorial: it occurs precisely when
$E$ touches every pentagonal face of $H_{t-1}$.
\end{remark}
\begin{remark}
\label{rem:alg-chord-apex}
Lemma~\ref{lem:chord-apex} applies only at $t = 1$, when $H_1$ is a reduced
dual of $G'$. For $t \geq 2$, $H_t$ is a reduced dual of $H_{t-1}$ rather than
of $G'$, and $H_{t-1}$ is itself $3$-edge-colourable, so the
non-$3$-edge-colourability argument that drives Lemma~\ref{lem:chord-apex}
does not carry over. Whether the constraints accumulated in $E$ propagate
any further structure to $\varphi_t$ for $t \geq 2$ is left open.
\end{remark}
\begin{figure}[h]
\centering
\includegraphics[width=0.32\textwidth]{fig_alg_step0.png}\hfill
\includegraphics[width=0.32\textwidth]{fig_alg_step1.png}\hfill
\includegraphics[width=0.32\textwidth]{fig_alg_step2.png}
\caption{Algorithm~\ref{alg:iterated-reduction} on $G'=\mathrm{dual}(G)$, where
$G$ is the first min-degree-$5$ plantri triangulation on $14$ vertices and
$\varphi_1$ is a specific proper $3$-edge-colouring of $H_1$ that satisfies
both the chord-apex condition (Lemma~\ref{lem:chord-apex}) and the Kempe-cycle
condition (Lemma~\ref{lem:kempe-spike}), found by
\texttt{experiments/search\_kempe\_property.py}. \emph{Left:} $G'$
($24$ vertices, $36$ edges) with the chosen pentagonal face shaded.
\emph{Centre:} $H_1$ ($20$ vertices, $30$ edges) after step~(1) with
$i_1 = 1$, $3$-edge-coloured by $\varphi_1$; the four edges around
$v_n^{(1)}$ in $E$ are drawn thicker, and the spike and merged edges share
the colour green. \emph{Right:} $H_2$ ($16$ vertices, $24$ edges) after
step~(3) with $i_t = 3$; eight edges are protected, and the algorithm
terminates one step later (no remaining safe pentagonal face in $H_2$).
The generating script is
\texttt{experiments/draw\_iterated\_reduction\_n14.py}; layouts are Tutte
barycentric embeddings with the outer face picked to keep $v_n^{(1)},
v_n^{(2)}$ in the interior.}
\label{fig:iterated-reduction-trace}
\end{figure}
\begin{lemma}[Exactly one matching pair in the algorithm's output]
\label{lem:exactly-one-match}
Let $G$ be a minimal counterexample to the Four Colour Theorem, and let
$(H_{t^*}, \varphi_{t^*})$ be the final graph-and-colouring produced by some
terminating execution of Algorithm~\ref{alg:iterated-reduction} on $G$, with
named pairs $(\mathrm{spike}_t, \mathrm{merged}_t)$ for $t = 1, \dots, t^*$.
Then there is exactly one $t$ with
$\varphi_{t^*}(\mathrm{spike}_t) = \varphi_{t^*}(\mathrm{merged}_t)$, and it
is $t = 1$.
\end{lemma}
\begin{proof}
The algorithm never re-colours an existing edge: at each iteration
step~(3d) every surviving edge keeps its $\varphi_{t-1}$-colour, and the
four new edges receive fresh colours forced by propriety. Hence for every
$1 \leq k \leq t \leq t^*$,
\[
\varphi_t(\mathrm{spike}_k) = \varphi_k(\mathrm{spike}_k),
\qquad
\varphi_t(\mathrm{merged}_k) = \varphi_k(\mathrm{merged}_k);
\]
the colours of the step-$k$ named edges, once written, are permanent. It
suffices to compare $\varphi_k(\mathrm{spike}_k)$ and
$\varphi_k(\mathrm{merged}_k)$ at the step where each pair is introduced.
\textbf{Case $k = 1$.} Since $G$ is a minimal counterexample, $H_1$ is a
reduced dual of $G'$. Lemma~\ref{lem:chord-apex} applied to $\varphi_1$ gives
$\varphi_1(\mathrm{spike}_1) = \varphi_1(\mathrm{merged}_1)$.
\textbf{Case $k \geq 2$.} At step $k$ the algorithm picks an index $i_k$ for
which $f_{i_k+3} = f_{i_k+4}$ (chord consistency) and $f_{i_k}, f_{i_k+1},
f_{i_k+2}$ are pairwise distinct (propriety at the new $v_n$), where $f$ is
the external vector of the chosen pentagonal face of $H_{k-1}$ under
$\varphi_{k-1}$. Step~(3d) then assigns
\[
\varphi_k(\mathrm{spike}_k) = f_{i_k+1},
\qquad
\varphi_k(\mathrm{merged}_k) = f_{i_k+3}.
\]
By Lemma~\ref{lem:pentagonal-externals}, $f$ has the $(2,2,1)$ pattern: a
block of three consecutive positions $\{p, p+1, p+2\}$ (mod $5$) on which it
is constantly some colour $c$, while the remaining two positions
$\{p+3, p+4\}$ hold the two non-$c$ colours, one each. The condition
$f_{i_k+3} = f_{i_k+4}$ forces $(i_k+3, i_k+4)$ to be either $(p, p+1)$ or
$(p+1, p+2)$ --- the two consecutive pairs inside the block --- and
correspondingly $i_k + 1 \in \{p+3, p+4\}$, \emph{outside} the block. So
$f_{i_k+1}$ is not $c$, whereas $f_{i_k+3} = c$, and hence
$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$.
Combining the two cases, exactly one $t \in \{1, \dots, t^*\}$ --- namely
$t = 1$ --- has $\varphi_{t^*}(\mathrm{spike}_t) =
\varphi_{t^*}(\mathrm{merged}_t)$.
\end{proof}
\begin{lemma}[All-distinct colouring exists on a 4-colourable graph]
\label{lem:all-distinct-exists}
Let $G$ be a $4$-colourable maximal planar graph of minimum degree $\geq 5$
(equivalently, a maximal planar graph that is \emph{not} a minimal
counterexample to the Four Colour Theorem). Then there is an execution of
Algorithm~\ref{alg:iterated-reduction} on $G$ whose final colouring
$\varphi_{t^*}$ satisfies
$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ for
every $t \in \{1, \dots, t^*\}$. In particular, there exists a proper
$3$-edge-colouring of $H_{t^*}$ under which every spike-merged pair has
distinct colours.
\end{lemma}
\begin{proof}
The argument mirrors Lemma~\ref{lem:exactly-one-match}, but extends a
colouring \emph{downward} from $G'$ rather than carrying one forward from
$H_1$.
Since $G$ is $4$-colourable, by Tait's theorem
$G' = \mathrm{dual}(G)$ admits a proper $3$-edge-colouring $\xi$. Apply
Lemma~\ref{lem:pentagonal-externals} to $\xi$ at the pentagonal face $F_v$
selected in step~(1): the external vector $f = (f_0, \dots, f_4)$ at $F_v$
under $\xi$ has the $(3,1,1)$ cyclic-consecutive shape, with a block of
three consecutive positions $\{p, p+1, p+2\}$ (mod $5$) holding a common
colour $c$, and the remaining two positions $\{p+3, p+4\}$ holding the two
non-$c$ colours, one each. The algorithm's choice of $i_1$ forces
$\{i_1+3, i_1+4\}$ inside the $c$-block (so the chord is consistently
coloured) and the three positions $\{i_1, i_1+1, i_1+2\}$ pairwise distinct;
in particular $i_1+1$ lies \emph{outside} the $c$-block.
Choose $\varphi_1$ to be the proper $3$-edge-colouring of $H_1$ that agrees
with $\xi$ on every surviving edge and assigns each new edge at $A_j$ the
unique third colour at $A_j$. Then
$\varphi_1(\mathrm{spike}_1) = f_{i_1+1}$, a value not equal to $c$, while
$\varphi_1(\mathrm{merged}_1) = f_{i_1+3} = c$, so
$\varphi_1(\mathrm{spike}_1) \neq \varphi_1(\mathrm{merged}_1)$.
The same argument repeats at every step $k \geq 2$: the external vector at
the chosen pentagonal face under $\varphi_{k-1}$ has the $(3,1,1)$
cyclic-consecutive shape (Lemma~\ref{lem:pentagonal-externals}), the
algorithm's index choice $i_k$ puts $i_k+3, i_k+4$ inside the colour block
and $i_k+1$ outside, and step~(3d) thus assigns
$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$. The
algorithm preserves these colours through every later step, so
$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ for
every $t \in \{1, \dots, t^*\}$.
\end{proof}
\begin{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)$,
\item $e_1$, $e_2$, and the merged edge all lie on a common
$\{a, b\}$-Kempe cycle of $\varphi$, and
\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$
and $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 bounded by exactly $4$
edges (the new edge, the two subdivision halves adjacent to it, and
the single $\partial F$-edge between $e_1$ and $e_2$).
\end{enumerate}
\end{conjecture}
\begin{remark}
\label{rem:conj-3-6-empirical}
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 counterexample's
reduced dual is forced to admit such colourings under any proper colouring.
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 tested 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), but
did not finish 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 proper $3$-edge-colouring satisfying chord-apex +
both Kempe-cycle conditions, so the conjecture has no content there. On
every $(G, F, i, \varphi)$ with content, all three clauses of the
conjecture hold simultaneously.
\end{remark}
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 the central tool in
We introduce 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 the central tool in
Section~\ref{sec:toward-4ct} below, where we formulate a sufficient
condition for the Four Colour Theorem.
@@ -788,39 +518,110 @@ by the contraction).}
\label{fig:thm-cubic-contraction-4face}
\end{figure}
\section{The Four Colour Theorem from a strengthened conjecture}
\section{The face-monochromatic-pair conjecture and the Four Colour Theorem}
\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.
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:cubic-contraction-4face}.
\begin{conjecture}[Strengthening of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}]
The reduced-dual construction of Definition~\ref{def:reduced-dual} can also
be applied \emph{iteratively}, producing a sequence $H_1, H_2, \dots$ of
progressively smaller cubic plane graphs and tracking an accumulating set
of ``protected'' edges; that iterated reduction, with its termination
analysis and structural lemmas about spike/merged pairs at each stage, is
the subject of a companion paper and is not used below.
\begin{conjecture}[Face-monochromatic-pair conjecture]
\label{conj:face-monochromatic-pair-on-merged-kempe-cycle}
Let $G$ be a minimal counterexample to the Four Colour Theorem, and let
$\widehat{G}'_{v,i}$ be a reduced dual of $G' = \mathrm{dual}(G)$. Then
for every proper $3$-edge-colouring $\varphi$ of $\widehat{G}'_{v,i}$
there exist a face $F$ of $\widehat{G}'_{v,i}$ and two distinct edges
$e_1, e_2 \in \partial F$, with neither $e_1$ nor $e_2$ equal to the
merged edge, such that:
\begin{enumerate}
\item $\varphi(e_1) = \varphi(e_2)$. Write
$a := \varphi(e_1) = \varphi(e_2)$.
\item $e_1$, $e_2$, and the merged edge all lie on a common
$\{a, b\}$-Kempe cycle of $\varphi$, for some colour $b \neq a$.
\item Exactly one edge of $\partial F$ lies between $e_1$ and $e_2$
along one of the two arcs of $\partial F$. Equivalently,
subdividing $e_1, e_2$ by new vertices $X_1, X_2$ and joining
them by a new edge $X_1 X_2$ inside $F$ creates a new face $f_n$
bounded by exactly $4$ edges (the new edge $X_1 X_2$, the two
subdivision halves adjacent to it, and the single
$\partial F$-edge between $e_1$ and $e_2$).
\end{enumerate}
\end{conjecture}
\begin{remark}
\label{rem:conj-3-6-empirical}
\sloppy
The conjecture cannot be tested on actual minimal counterexamples (none
exist by the Four Colour Theorem), but its conclusion is checkable on the
structural surrogates: proper $3$-edge-colourings of reduced duals that
satisfy both the chord-apex condition (Lemma~\ref{lem:chord-apex}) and
the Kempe-cycle conditions (Lemma~\ref{lem:kempe-spike}), since a minimal
counterexample's reduced dual is forced to admit such colourings. For
every min-degree-$5$ triangulation $G$ with $|V(G)| \leq 21$, every
pentagonal face $F$ of $G'$, and every reduction index
$i \in \{0,\dots,4\}$, we enumerated all such colourings and verified the
three clauses of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} (see
\texttt{experiments/check\_conj\_face\_kempe\_scaled.py}); $n = 22$ ran
past a $1800$\,s budget after $641{,}700$ colourings (all pass) without
finishing the full set of $651$ triangulations.
\begin{center}
\small
\renewcommand{\arraystretch}{1.15}
\begin{tabular}{r|r|r|r|l}
$n$ & \#tri & \#col.\ tested & \#sat. & status \\
\hline
$12$ & $1$ & $0$ & --- & vacuous (icosahedron) \\
$13$ & $0$ & --- & --- & no min-deg-$5$ tri \\
$14$ & $1$ & $216$ & $216$ & all pass \\
$15$ & $1$ & $0$ & --- & vacuous \\
$16$ & $3$ & $864$ & $864$ & all pass \\
$17$ & $4$ & $4{,}650$ & $4{,}650$ & all pass \\
$18$ & $12$ & $8{,}070$ & $8{,}070$ & all pass \\
$19$ & $23$ & $21{,}138$ & $21{,}138$ & all pass \\
$20$ & $73$ & $107{,}874$ & $107{,}874$ & all pass \\
$21$ & $192$ & $392{,}370$ & $392{,}370$ & all pass \\
$22$ (part.) & $651$ & $641{,}700$ & $641{,}700$ & timeout \\
\hline
total ($n \le 21$) & $311$ & $535{,}182$ & $535{,}182$ & \\
\end{tabular}
\end{center}
\noindent The vacuous rows ($n = 12, 15$) are those where the relevant
reduced duals admit no chord-apex+Kempe colourings, so the conjecture
has no content there.
\end{remark}
The following strengthening adds a fourth clause that arranges the new
$4$-face $f_n$ to satisfy the hypotheses of
Theorem~\ref{thm:cubic-contraction-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, 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:
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 either
\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
@@ -836,30 +637,29 @@ the new $4$-edge face of $\widehat{G}'^{+}$ incident to $X_1 X_2$. Then:
\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
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 \\
$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 \\
$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 \\
\hline
total & $23$ & $13{,}800$ & $13{,}800$ & \\
total ($n \le 18$) & $20$ & $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.
\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.
\end{remark}
\begin{remark}[The implication to the Four Colour Theorem]