dual_decomposition: Conj 3.6 (face/Kempe witness) and constructive lift

Paper:
- Lemmas 3.4 (exactly one match) and 3.5 (all-distinct exists for 4-colourable
  G) replace the earlier conjecture; both have proofs.
- Add Conjecture 3.6: every proper 3-edge-colouring of a counterexample's
  reduced dual has a face with two same-colour edges that share a Kempe
  cycle with the merged edge, neither of them being the merged edge.

Experiments (all under experiments/):
- search_conj_3_6_counterexample.py: finds n=14 tri#1 i_red=0 where the
  algorithm's phi_t* sits in a Kempe class with no all-distinct colouring
  (disproves an earlier formulation).
- check_kempe_class.py / check_kempe_class_invariance.py /
  check_kempe_class_monotone.py: Kempe-class counts on H_1 and H_t* for
  small triangulations; neither monotonicity direction holds.
- check_all_distinct_exists.py: even in the conj-3.6 disproof case, H_t*
  itself admits all-distinct colourings in the *other* Kempe class.
- check_constrained_feasibility.py: literal H_t*-interpretation of
  C1 + K0 + K1 is empirically unsatisfiable (gap in proof strategy noted).
- check_conj_face_kempe.py / check_conj_face_kempe_n15.py: test Conj 3.6
  on chord-apex+Kempe colourings of reduced duals at n=12, 14, 15;
  216/216 colourings on n=14 satisfy the conjecture, others vacuous.
- draw_step1_conj36.py: figure showing a Conj 3.6 witness on H_1 with two
  new vertices on the witness edges and a new red bridge between them.
- draw_step1_conj36_recolored.py: same but with the Kempe cycle recoloured
  alternately from merged so propriety holds.
- draw_lift_to_Gprime.py: lifts the modified+recoloured H_1 back to a
  proper 3-edge-colouring of the modified G' (24+2 vertices, 39 edges,
  same Tutte layout as figure 3's first graphic so positions line up).

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

papers/dual_decomposition_minimal_counterexamples/paper.tex

@@ -499,16 +499,121 @@ 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: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^*\}$.
+\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)$, and
+  \item $e_1$, $e_2$, and the merged edge all lie on a common
+        $\{a, b\}$-Kempe cycle of $\varphi$.
+\end{enumerate}
 \end{conjecture}
 
 \end{document}