dual_decomposition: Kempe-cycle lemma through the spike

- Update def:edge-names to distinguish side-0 ({A_i, v_n}) and side-1
  ({A_{i+2}, v_n}); merged and spike unchanged.
- Add a paragraph defining the {a,b}-Kempe cycle in a 3-edge-coloured cubic
  graph.
- Add lem:kempe-spike: in any proper 3-edge-colouring of the reduced dual,
  the {c, c_0}-Kempe cycle through the spike contains side-0 and merged
  (symmetrically for side-1 with c_1).
- Proof by Kempe swap: a hypothetical alternative cycle K containing merged
  but not spike would, after swapping c <-> c_0 on K, give a proper
  3-edge-colouring under which spike and merged disagree --- contradicting
  lem:chord-apex.

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

papers/dual_decomposition_minimal_counterexamples/paper.tex

@@ -177,11 +177,12 @@ $\widehat{G}'_{v,0}$.}
 \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}; and the edges $A_iv_n$ and
-$A_{i+2}v_n$ are the \emph{side edges}. In the $i = 0$ case of
-Figure~\ref{fig:reduced-dual-steps} these are $\{A_3, A_4\}$, $\{A_1, v_n\}$,
-and $\{A_0, v_n\}, \{A_2, v_n\}$ respectively.
+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
@@ -348,4 +349,46 @@ $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}
+
 \end{document}