face_monochromatic_pairs: Theorem 5.5 Step 4 closes Case A (lune face contradiction)

Case A: K_1 visits the four shared vertices {p, p', q, q'} in the same
cyclic order as K_0. The K_0-arc A_1 from p' to q and the K_1-arc B_1
from p' to q share both endpoints, so they bound a "lune" face Φ* of
K_0 ∪ K_1 with two (b, c)-corners.
  - Planarity: B_1's interior is non-shared, so B_1 lies on one side of
    K_0; hence c-edges at p' and q (endpoints of B_1) point to the
    SAME side of K_0.
  - Lemma 5.2 along A_1 (m odd): c-edges at p' and q alternate, so
    they point to OPPOSITE sides of K_0.
  → Contradiction.

This is clean and uses only Lemma 5.2 + planarity (does not require
the mod 3 face-sum from Step 3).

Case B: K_1 visits the shared vertices in opposite order
{p, p', q', q}. Then K_0 ∪ K_1's faces are 3-corner triangles instead
of lunes; both Lemma 5.2 alternations and the mod 3 face-sum hold
consistently. Listed as the explicit open case.

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

papers/face_monochromatic_pairs/paper.tex

@@ -935,18 +935,55 @@ contribution is a multiple of $3$ and drops out.) Hence
 \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$.)}
+\textbf{Step 4 (lune-face contradiction, Case A).} Pick any two
+\emph{consecutive} shared a-edges on the $K_0$-walk: $e_1 = (p, p')$
+and $e_2 = (q, q')$, separated by a $K_0$-arc $A_1$ from $p'$ to $q$
+of length $m$. The arc begins with the colour-$b$ edge at $p'$ and
+ends with the colour-$b$ edge at $q$, so $m$ is odd. Both $K_0$ and
+$K_1$ traverse $e_1$ and $e_2$, so the four vertices
+$\{p, p', q, q'\}$ are shared. Two cases for the cyclic order in which
+$K_1$ visits these four:
+
+\begin{description}
+\item[Case A.] $K_1$ visits them in the same cyclic order
+$p, p', q, q'$ as $K_0$. Then $K_1$ has a $K_1$-arc $B_1$ from $p'$
+to $q$ (between $e_1$ and $e_2$ on the $K_1$-walk), of odd length
+$n$, whose intermediate vertices are all non-shared.
+\item[Case B.] $K_1$ visits them in the opposite order
+$p, p', q', q$. Then $K_1$'s arcs between $e_1, e_2$ go from $p'$ to
+$q'$ and from $q$ to $p$; they do not share endpoints with $A_1$.
+\end{description}
+
+\emph{Case A is impossible.} The arcs $A_1$ and $B_1$ share both
+endpoints $p', q$ and meet only at those endpoints, so they bound a
+``lune'' face $\Phi^*$ of $K_0 \cup K_1$ whose boundary has exactly
+two corners (both of wedge type $(b, c)$) and length $m + n$. Now
+\begin{itemize}
+\item Every intermediate vertex of $B_1$ is a non-shared $K_1$-vertex,
+hence not on $K_0$, hence lies in one of the two open regions of
+$\mathbb{R}^2 \setminus K_0$. Since $B_1$ is a connected path joining
+$p', q \in V(K_0)$ and never visits $V(K_0)$ in its interior,
+$B_1 \setminus \{p', q\}$ lies entirely on \emph{one} side of $K_0$.
+In particular the colour-$c$ edges at $p'$ and at $q$ (the first
+and last edges of $B_1$) point into the \emph{same} side of $K_0$.
+\item By Lemma~\ref{lem:kempe-heawood-constant} applied along the
+$K_0$-arc from $p'$ to $q$, consecutive colour-$c$ non-cycle edges
+alternate sides. After $m$ steps with $m$ odd, the colour-$c$ edges
+at $p'$ and at $q$ lie on \emph{opposite} sides of $K_0$.
+\end{itemize}
+These two conclusions are incompatible, contradicting the assumption
+that both $K_0$ and $K_1$ have constant $h_\varphi$ in Case A.
+
+\textbf{Step 5 (Case B --- TBD).} In Case B, the four faces of
+$K_0 \cup K_1$ are each three-corner ``triangles'' bounded by one
+$K_0$-arc, one $K_1$-arc, and one shared a-edge (one corner each of
+types $(a,b)$, $(b,c)$, $(c,a)$). For such a face the
+Step~4 lune argument does not apply: $A_1$ and the corresponding
+$K_1$-arc $B_1$ no longer share both endpoints, and both
+Lemma~\ref{lem:kempe-heawood-constant} alternations and the mod-$3$
+constraint~\eqref{eq:face-sum-mod3} can be checked to be
+consistent on the parity counts. The contradiction in this case is
+\emph{open}.
 
 \emph{Empirical note.} The theorem's hypothesis is never observed:
 across the $142{,}812$ chord-apex+Kempe colourings of reduced duals