diff --git a/papers/face_monochromatic_pairs/paper.pdf b/papers/face_monochromatic_pairs/paper.pdf
index 63b80c7..beaf4fc 100644
Binary files a/papers/face_monochromatic_pairs/paper.pdf and b/papers/face_monochromatic_pairs/paper.pdf differ
diff --git a/papers/face_monochromatic_pairs/paper.tex b/papers/face_monochromatic_pairs/paper.tex
index f35f153..74738f3 100644
--- a/papers/face_monochromatic_pairs/paper.tex
+++ b/papers/face_monochromatic_pairs/paper.tex
@@ -825,37 +825,134 @@ 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]
+\begin{proof}[Proof attempt]
 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.
+$e = (u, w)$. Then $u, w \in V(K_0) \cap V(K_1)$ are consecutive on
+both cycles. Since the two constants agree at the shared vertex $u$,
+they agree everywhere on $V(K_0) \cup V(K_1)$; WLOG
+$h_\varphi \equiv +1$ on $V(K_0) \cup V(K_1)$, so the CW edge order at
+every such vertex is $(a, b, c)$.
 
-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$.
+Orient both cycles so that they leave $u$ along $e$: write the $K_0$
+walk as $u = v_0 \xrightarrow{e} w = v_1 \to v_2 \to \cdots \to
+v_{L_0 - 1} \to v_0$, and the $K_1$ walk as $u = u_0 \xrightarrow{e}
+w = u_1 \to u_2 \to \cdots \to u_{L_1 - 1} \to u_0$. Let
+$F_R(e), F_L(e)$ be the two faces of $H$ incident to $e$, with $F_R$
+on the right and $F_L$ on the left of the $u \to w$ traversal.
 
-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$.
+\textbf{Step 1 (local sides at $u, w$).} The CW-order $(a, b, c)$ at
+$u$ and $w$ partitions the faces of $H$ at each endpoint into three
+wedges. Direct inspection (cf.\ the proof of
+Lemma~\ref{lem:kempe-heawood-constant}) gives
+\[
+F_R(e) = F_{ab}^u = F_{ca}^w, \qquad F_L(e) = F_{ca}^u = F_{ab}^w,
+\]
+where $F_{\alpha\beta}^v$ is the face of $H$ at $v$ in the CW wedge
+between the colour-$\alpha$ and colour-$\beta$ edges. Consequently:
+\begin{itemize}
+\item $e_c^u$ lies between $F_{bc}^u$ and $F_{ca}^u = F_L(e)$, so $e_c^u$
+is on the side of $K_0$ containing $F_L(e)$ near $u$; call this side
+$\mathrm{In}(K_0)$.
+\item $e_c^w$ lies between $F_{bc}^w$ and $F_{ca}^w = F_R(e)$, so
+$e_c^w$ is on the side $\mathrm{Out}(K_0)$ containing $F_R(e)$ near $w$.
+\item Symmetrically, $e_b^u$ is on the side of $K_1$ containing
+$F_R(e)$, call this $\mathrm{Out}(K_1)$, and $e_b^w$ is on the side
+$\mathrm{In}(K_1)$ containing $F_L(e)$.
+\end{itemize}
+This recovers exactly the conclusion of
+Lemma~\ref{lem:kempe-heawood-constant} applied to $(u, w)$ on each
+cycle.
 
-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{Step 2 (forced crossings).} Consider $K_1 \setminus e$, the
+path from $u$ to $w$ obtained by removing the open edge $e$ from
+$K_1$. By Step~1, this path leaves $u$ on the $\mathrm{In}(K_0)$ side
+and arrives at $w$ on the $\mathrm{Out}(K_0)$ side. Since $K_0$
+separates the plane into its two sides and $K_1 \setminus e$ is a
+continuous arc, the path must intersect $V(K_0)$ at an odd number of
+points strictly between $u$ and $w$ along the $K_1$-walk.
 
-\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.
+At any such intersection $x \in V(K_0) \cap V(K_1) \setminus \{u, w\}$,
+$K_1$ uses the colour-$a$ edge at $x$ (since $K_1$ uses only colours
+$a, c$ and only colour-$a$ edges can lie on $K_0$). That colour-$a$
+edge is therefore a shared edge $e^* \in E(K_0) \cap E(K_1)$ with
+$e^* \neq e$; both endpoints of $e^*$ lie in $V(K_0) \cap V(K_1)$.
+
+So $|E(K_0) \cap E(K_1)| - 1$ equals the (odd) number of crossings,
+giving
+\[
+|E(K_0) \cap E(K_1)| \text{ is even, and } \geq 2.
+\]
+The symmetric argument applied to $K_0 \setminus e$ crossing $K_1$
+yields the same conclusion.
+
+\textbf{Step 3 (Heawood face-sum on each face of $K_0 \cup K_1$).}
+View $K_0 \cup K_1$ as a planar subgraph of $H$ and consider any face
+$\Phi$ of this subgraph. Let $F_\Phi$ be the set of $H$-faces lying
+inside (the closed region of) $\Phi$. Applying Heawood's classical
+face-sum identity
+$\sum_{v \in \partial f} h_\varphi(v) \equiv 0 \pmod 3$
+\cite{Heawood1898}
+to every $f \in F_\Phi$ and summing gives
+\[
+\sum_{f \in F_\Phi} \sum_{v \in \partial f} h_\varphi(v) \;=\;
+\sum_{v} \mathrm{mult}_\Phi(v)\, h_\varphi(v) \;\equiv\; 0 \pmod 3,
+\]
+where $\mathrm{mult}_\Phi(v)$ counts the number of $H$-faces in
+$F_\Phi$ whose boundary contains $v$.
+
+A direct case-check on the cubic vertex structure gives:
+\begin{itemize}
+\item $\mathrm{mult}_\Phi(v) = 3$ if $v$ is strictly interior to $\Phi$
+(all three $H$-faces at $v$ lie in $F_\Phi$);
+\item $\mathrm{mult}_\Phi(v) = 1$ if $v$ is a degree-$3$
+(shared, branching) vertex of $K_0 \cup K_1$ on $\partial\Phi$ (only
+one of $v$'s three wedges lies in $\Phi$);
+\item $\mathrm{mult}_\Phi(v) = 2$ if $v$ is a degree-$2$ (non-shared)
+vertex of $K_0 \cup K_1$ on $\partial\Phi$ \emph{and} $v$'s third edge
+points into $\Phi$ (the third edge subdivides $v$'s wedge in $\Phi$
+into two $H$-faces);
+\item $\mathrm{mult}_\Phi(v) = 1$ if $v$ is a degree-$2$ non-shared
+boundary vertex with its third edge pointing into the opposite face.
+\end{itemize}
+
+Under the contradiction hypothesis $h_\varphi \equiv +1$ on
+$V(K_0) \cup V(K_1) \supseteq \partial\Phi$, the boundary contribution
+collapses to
+\[
+\sigma_\Phi + \nu_{1,\Phi} + 2\,\nu_{2,\Phi}
+\;=\; \ell_\Phi + \nu_{2,\Phi}
+\;\equiv\; 0 \pmod 3,
+\]
+where $\sigma_\Phi$ counts shared boundary vertices of $\Phi$,
+$\nu_{1,\Phi}$ and $\nu_{2,\Phi}$ count non-shared boundary vertices
+with third edge pointing out of / into $\Phi$ respectively, and
+$\ell_\Phi$ is the boundary length of $\Phi$. (The interior
+contribution is a multiple of $3$ and drops out.) Hence
+\begin{equation}
+\label{eq:face-sum-mod3}
+\nu_{2,\Phi} \;\equiv\; -\ell_\Phi \pmod 3
+\quad\text{for every face } \Phi \text{ of } K_0 \cup K_1.
+\end{equation}
+
+\textbf{Step 4 (Lemma~\ref{lem:kempe-heawood-constant} alternation as
+a side-assignment --- TBD).} The Lemma~\ref{lem:kempe-heawood-constant}
+alternation on $K_0$ determines, for each non-shared
+$K_0$-vertex $v$, exactly which side of $K_0$ its colour-$c$
+(``third'') edge lies on --- and that side is precisely the face
+$\Phi(v)$ of $K_0 \cup K_1$ that the third edge points into.
+Symmetrically for $K_1$. So the alternation gives an explicit
+prescription for $\nu_{2,\Phi}$ in terms of the parity of
+$K_0$- and $K_1$-walk indices along $\partial\Phi$.
+\emph{(The remaining work is to show that this prescription is
+incompatible with~\eqref{eq:face-sum-mod3} for some face
+$\Phi$.)}
+
+\emph{Empirical note.} The theorem's hypothesis is never observed:
+across the $142{,}812$ chord-apex+Kempe colourings of reduced duals
+with $|V(G)| \le 20$, ``$h_\varphi$ constant on $V(K_b)$'' fails on
+every colouring (see \texttt{experiments/check\_constancy\_obstruction.py}
+and Remark~\ref{rem:heawood-empirical}).
 \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}]