face_monochromatic_pairs: add Theorem 5.5 (constant Heawood on edge-sharing Kempe cycles is impossible)

If true, Theorem 5.5 + Lemma 5.3 → Conjecture 5.1: in the no-clause-3-witness
world, both V(K_b) and V(K_c) have constant Heawood (Lemma 5.3), but K_b
and K_c share the merged edge, contradicting Theorem 5.5.

Proof sketch sets up the two Lemma-5.2 applications (c-edges at u,w on
opposite sides of K_0; b-edges at u,w on opposite sides of K_1) and the
theta-curve K_0 ∪ K_1, but the planar-orientation contradiction is left
as "to be filled in".

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

papers/face_monochromatic_pairs/paper.tex

@@ -814,6 +814,50 @@ that proof produces a clauses-(1)--(3) witness without ever needing to
 inspect the other Kempe cycle.
 \end{proof}
 
+\begin{theorem}[Constant Heawood on two edge-sharing Kempe cycles is impossible]
+\label{thm:no-two-constant-kempe-cycles}
+Let $H$ be a cubic plane graph with a proper $3$-edge-colouring
+$\varphi$, fix a colour $a \in \{1, 2, 3\}$, and let $\{b, c\} =
+\{1, 2, 3\} \setminus \{a\}$. Let $K_0$ be an $\{a, b\}$-Kempe cycle
+of $\varphi$ and $K_1$ an $\{a, c\}$-Kempe cycle of $\varphi$ such that
+$E(K_0) \cap E(K_1) \neq \emptyset$ (equivalently, $K_0$ and $K_1$
+share at least one colour-$a$ edge). If $h_\varphi$ is constant on
+$V(K_0)$, then $h_\varphi$ is \emph{not} constant on $V(K_1)$.
+\end{theorem}
+
+\begin{proof}[Proof sketch]
+Suppose for contradiction that $h_\varphi$ is constant on both
+$V(K_0)$ and $V(K_1)$, and that $K_0, K_1$ share a colour-$a$ edge
+$e = (u, w)$, so that $u, w \in V(K_0) \cap V(K_1)$ are consecutive on
+both cycles.
+
+By Lemma~\ref{lem:kempe-heawood-constant} applied to $K_0$: at every
+consecutive pair of $K_0$-vertices the colour-$c$ non-cycle edges lie
+on opposite local sides of $K_0$. In particular the colour-$c$ edges
+at $u$ and $w$ lie on opposite sides of $K_0$.
+
+By Lemma~\ref{lem:kempe-heawood-constant} applied to $K_1$: at every
+consecutive pair of $K_1$-vertices the colour-$b$ non-cycle edges lie
+on opposite local sides of $K_1$. In particular the colour-$b$ edges
+at $u$ and $w$ lie on opposite sides of $K_1$.
+
+Now $K_0$ and $K_1$ share the arc $e$ in the plane, so $K_0 \cup K_1$
+is either a single closed curve (if $K_0 = K_1$, which is impossible
+since they use different colour pairs) or a theta-curve based at
+$\{u, w\}$. In the latter case the colour-$b$ edges at $u, w$ together
+with $K_0 \setminus e$ form one side of the theta, and the colour-$c$
+edges at $u, w$ together with $K_1 \setminus e$ form another side.
+The combined opposite-sides conditions above force $K_0$ and $K_1$ to
+both wind around the same way at $e$ --- which a planar theta-curve
+cannot realise.
+
+\textbf{(Full proof to be filled in.)} The cleanest formalisation is
+likely via a winding-number / orientation argument on the theta-curve
+$K_0 \cup K_1$ in the plane, combined with the local CW-order
+constraints at $u$ and $w$ that Lemma~\ref{lem:kempe-heawood-constant}
+forces.
+\end{proof}
+
 \begin{remark}[Empirical near-proof of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} via Corollary~\ref{cor:single-cycle-non-constancy}]
 \label{rem:heawood-empirical}
 \sloppy