dual_decomposition: swap algorithm trace to n=14 + final-graph conjecture

- Replace the dodecahedron trace at the end of section 3 with the n=14
  triangulation found by search_kempe_property.py: its H_1 admits a
  proper 3-edge-colouring satisfying both chord-apex and Kempe-cycle
  conditions (Lemmas 2.6, 2.7).
- experiments/draw_iterated_reduction_n14.py: rebuilds fig_alg_step{0,1,2}
  with Tutte barycentric layouts (outer face chosen to keep v_n in the
  interior); also runs the algorithm to completion, checking chord-apex +
  Kempe at each step (step 1 satisfies all; step 2 fails chord-apex;
  step 3 terminates).
- Add Conjecture 3.4: G is a minimal counterexample iff no proper
  3-edge-colouring of the final reduced graph H_{t*} has all (spike_t,
  merged_t) pairs in distinct colours.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

papers/dual_decomposition_minimal_counterexamples/paper.tex

@@ -12,6 +12,7 @@
 \newtheorem{lemma}[theorem]{Lemma}
 \newtheorem{corollary}[theorem]{Corollary}
 \newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{conjecture}[theorem]{Conjecture}
 
 \theoremstyle{definition}
 \newtheorem{definition}[theorem]{Definition}
@@ -478,17 +479,36 @@ any further structure to $\varphi_t$ for $t \geq 2$ is left open.
 \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' = $ dodecahedron
-(dual of the icosahedron). \emph{Left:} $G'$ (20 vertices, 30 edges), with
-$F_v$ (the inner pentagon) shaded as the face chosen for the first reduction.
-\emph{Centre:} $H_1$ (16 vertices, 24 edges) after step~(1) with $i_1 = 0$,
-$3$-edge-coloured by Sage; the four edges around $v_n^{(1)}$ in $E$ are drawn
-thicker. \emph{Right:} $H_2$ (12 vertices, 18 edges) after step~(3) with
-$i_t = 0$; the only safe pentagonal face in $H_1$ was the outer pentagon,
-whose deletion produces $v_n^{(2)}$ and a second chord, giving eight protected
-edges. No safe pentagonal face remains, so the algorithm terminates. The
-generating script is \texttt{experiments/draw\_iterated\_reduction.py}.}
+\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{conjecture}
+\label{conj:no-all-distinct-coloring}
+Let $G$ be a maximal planar graph of minimum degree $\geq 5$, and let
+$H_{t^*}$ be the final reduced graph produced by some terminating execution
+of Algorithm~\ref{alg:iterated-reduction} on $G$, with the corresponding
+sequence of named pairs $(\mathrm{spike}_t, \mathrm{merged}_t)$ for
+$t = 1, \dots, t^*$. Then $G$ is a minimal counterexample to the Four Colour
+Theorem if and only if there is no proper $3$-edge-colouring of $H_{t^*}$
+under which $\mathrm{spike}_t$ and $\mathrm{merged}_t$ receive different
+colours for every $t \in \{1, \dots, t^*\}$.
+\end{conjecture}
+
 \end{document}