dual_decomposition: chord-apex proof + diagrams

- Replace the chord-apex TODO with a full proof by contradiction: assume
  merged != spike, define X, Y, Z, W, lift to G' so that the externals
  inherit \psi(f) = (X, Y, Z, W, W), and split on W in {X, Z}. Either case
  meets the hypothesis of lem:pentagonal-externals, which extends \psi to a
  proper 3-edge-colouring of G' --- contradicting non-3-edge-colourability
  via Tait.
- Add fig:chord-apex-proof: the assumed reduced-dual colouring on top, and
  the two lifted-G' cases (W=Z, W=X) below, rendered on the dodecahedron.
- Add experiments/draw_chord_apex_proof.py.

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

papers/dual_decomposition_minimal_counterexamples/paper.tex

@@ -281,20 +281,71 @@ $\widehat{G}'_{v,i}$, the merged edge and the spike edge receive the same
 colour.
 \end{lemma}
 
+\begin{figure}[h]
+\centering
+\includegraphics[width=0.7\textwidth]{fig_chord_apex_step1.png}\\[0.4em]
+\includegraphics[width=0.48\textwidth]{fig_chord_apex_step2.png}\hfill
+\includegraphics[width=0.48\textwidth]{fig_chord_apex_step3.png}
+\caption{The proof of Lemma~\ref{lem:chord-apex}, illustrated for $i = 0$ on
+$G' = $ the dodecahedron. Top: under the assumption $W \neq Y$, propriety at
+$v_n$ forces $W \in \{X, Z\}$. Bottom: in either case the lift to $G'$ has
+externals satisfying the hypothesis of
+Lemma~\ref{lem:pentagonal-externals}, which colours $\partial F_v$ to extend
+$\psi$ to a proper $3$-edge-colouring of $G'$.}
+\label{fig:chord-apex-proof}
+\end{figure}
+
 \begin{proof}
-% TODO. Intended argument: given a proper 3-edge-colouring of
-% \widehat{G}'_{v,i}, the colour at each A_k of the new edge there (one of the
-% three v_n-edges for k in {i, i+1, i+2}, or the chord for k in {i+3, i+4})
-% determines the colour of f_k in any lift to G' --- it is the unique colour
-% not used by the two original edges at A_k. Because the chord has a single
-% colour, f_{i+3} and f_{i+4} agree. If the merged edge and the spike edge
-% receive distinct colours, the three v_n-edges contribute three distinct
-% colours to f_i, f_{i+1}, f_{i+2}, and the resulting f-vector has shape
-% (X, Y, Z, W, W) with X, Y, Z distinct and W \neq Y. By
-% Lemma~\ref{lem:pentagonal-externals} applied to G' at the face F_v, this
-% extends to a proper 3-edge-colouring of G' --- contradicting that G' (the
-% dual of the minimal counterexample G) is not 3-edge-colourable. Hence the
-% merged edge and the spike edge must share a colour.
+After cyclically relabelling, assume $i = 0$. Suppose for contradiction that
+$\varphi$ is a proper $3$-edge-colouring of $\widehat{G}'_{v,0}$ in which the
+merged edge $\{A_3, A_4\}$ and the spike edge $\{A_1, v_n\}$ receive different
+colours (Figure~\ref{fig:chord-apex-proof}, top), and write
+\[
+  X = \varphi(\{A_0, v_n\}), \quad
+  Y = \varphi(\{A_1, v_n\}), \quad
+  Z = \varphi(\{A_2, v_n\}), \quad
+  W = \varphi(\{A_3, A_4\}).
+\]
+Propriety of $\varphi$ at $v_n$ forces $\{X, Y, Z\} = \{1, 2, 3\}$, and the
+assumption $W \neq Y$ leaves $W \in \{X, Z\}$.
+
+We lift $\varphi$ to a colouring $\psi$ of $E(G')$ as follows. Let
+$B_0, \dots, B_4$ be the boundary vertices of $\partial F_v$ in $G'$, indexed
+so that $f_k = B_k A_k$. On every edge of $G'$ that survived the reduction,
+set $\psi = \varphi$. At each $A_k$ the two surviving edges retain their
+$\varphi$-colours, so the remaining edge at $A_k$ --- in $G'$ this is the
+external $f_k$; in $\widehat{G}'_{v,0}$ this is a $v_n$-edge ($k \in
+\{0, 1, 2\}$) or the chord ($k \in \{3, 4\}$) --- is forced to take the third
+colour at $A_k$. Since the two-surviving-edge colours at $A_k$ agree in $G'$
+and $\widehat{G}'_{v,0}$, the third colour does too, giving
+\[
+  \psi(f_0) = X, \quad \psi(f_1) = Y, \quad \psi(f_2) = Z, \quad
+  \psi(f_3) = \psi(f_4) = W
+\]
+(the last two equalities holding because the chord is a single edge contributing
+its colour at each of $A_3$ and $A_4$).
+
+It remains to assign colours to the five boundary edges $B_k B_{k+1}$ of
+$\partial F_v$. Apply Lemma~\ref{lem:pentagonal-externals} to $G'$ at the face
+$F_v$ with the $B_k$'s as its boundary vertices and the same indexing. The
+external vector $(\psi(f_0), \dots, \psi(f_4)) = (X, Y, Z, W, W)$ falls into
+one of two cases (Figure~\ref{fig:chord-apex-proof}, bottom):
+\begin{itemize}
+  \item if $W = Z$, it is $(X, Y, Z, Z, Z)$: three consecutive $Z$'s at
+        positions $2, 3, 4$, with $\{X, Y\} = \{1, 2, 3\} \setminus \{Z\}$;
+  \item if $W = X$, it is $(X, Y, Z, X, X)$: three consecutive $X$'s at
+        positions $3, 4, 0$, with $\{Y, Z\} = \{1, 2, 3\} \setminus \{X\}$.
+\end{itemize}
+Each case satisfies the hypothesis of Lemma~\ref{lem:pentagonal-externals};
+its $(\Leftarrow)$ direction therefore assigns colours to the boundary edges
+$B_k B_{k+1}$ that make $\psi$ proper at every $B_k$.
+
+The resulting $\psi$ is a proper $3$-edge-colouring of $G'$: proper at every
+$B_k$ by the lemma, at every $A_k$ by the construction, and at every other
+vertex because such a vertex has the same neighbourhood in $G'$ as in
+$\widehat{G}'_{v,0}$ with the same incident-edge colours. By Tait's theorem,
+$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}
 
 \end{document}