face_monochromatic_pairs: reduce Conj 5.1 to a "deciding face" conjecture

NEW PROOF STRATEGY for Conjecture 5.1 (face-monochromatic-pair):

1. NEW Conjecture (Deciding face): For every chord-apex+Kempe
   colouring φ of every reduced dual, the reduced dual has a face f
   with ∂f ⊆ V(K_b) ∪ V(K_c) and |f| ≢ 0 (mod 3).

2. NEW Theorem: Deciding-face conjecture implies Conj 5.1.

   Proof: contradiction. Assume no clauses-(1)-(3) witness for some
   chord-apex+Kempe φ. By Lemma 5.3, h_φ ≡ ε ∈ {±1} on V(K_b) ∪ V(K_c).
   By the deciding-face conjecture, ∃ face f with ∂f ⊆ V(K_b) ∪ V(K_c),
   |f| ≢ 0 (mod 3). Heawood's face-sum identity (Heawood 1898) gives
   Σ_{v ∈ ∂f} h_φ(v) = ε|f| ≡ 0 (mod 3). Since gcd(|f|, 3) = 1, we get
   ε ≡ 0 (mod 3), but ε ∈ {±1} — contradiction.

3. EMPIRICAL: Conjecture (Deciding face) verified on 142,812 / 142,812
   chord-apex+Kempe colourings of reduced duals up to |V(G)| ≤ 20 --
   matching the full coverage of check_constancy_obstruction.py.
   Face-length distribution:
     |f| = 4:  13,074
     |f| = 5: 102,498 (most common)
     |f| = 7:  18,570
     |f| = 8:   7,752
     |f| = 10:    846
     |f| = 11:     72
   (All ≢ 0 mod 3.)

New scripts:
  - check_kb_kc_coverage.py: |V(K_b) ∪ V(K_c)| / |V(Ĝ')| distribution.
    73.87% of colourings have V(K_b) ∪ V(K_c) = V (full coverage); the
    remaining 26% have coverage ≥ 70%, mostly ≥ 90%.
  - check_deciding_face.py: existence of deciding face across all
    colourings; 100.00% / 142,812.

Why this is the right reduction:
  - It uses ALL THREE pieces of chord-apex+Kempe structure: Lemma 5.3
    (constancy from no-witness), forced colour-equality at merged/spike,
    and forced Kempe-cycle containment of merged + spike + side edges
    (the latter two enter via V(K_b) ∪ V(K_c) covering specific
    structural vertices).
  - It uses Heawood's face-sum identity, which is the classical 3-fold
    parity constraint on cubic plane 3-edge-colourings.
  - The C28 counterexample to Conjecture 5.5 is not affected: it's not
    a chord-apex+Kempe colouring of a reduced dual, so the deciding-face
    structure doesn't apply.

Remaining work: prove the deciding-face conjecture structurally (likely
via the specific F_01 / F_12 "flank face" of the reduced dual, whose
length n_0 - 1 from the adjacent G'-face of length n_0 ≥ 5 is ≢ 0 mod 3
exactly when n_0 ≢ 1 mod 3, plus boundary-in-V(K_b) ∪ V(K_c) which
follows from Lemma 5.X kempe-spike + colour analysis at A_i).

Paper grows from 17 to 18 pages.

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

papers/face_monochromatic_pairs/paper.tex

@@ -891,6 +891,108 @@ $V(K_0) \cup V(K_1) \setminus V(K_0) \cap V(K_1)$; grey on neither.}
 \label{fig:no-two-constant-kempe-counterexample}
 \end{figure}
 
+\subsection*{A reduction of Conjecture
+\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} via Heawood's
+face-sum identity}
+
+The empirical work of Section~\ref{sec:reduced-dual} (the
+$0/142{,}812$ result on chord-apex+Kempe colourings, recorded in
+Remark~\ref{rem:heawood-empirical}) suggests a structural proof
+strategy via the classical Heawood face-sum identity
+\cite{Heawood1898}:
+\begin{equation}
+\label{eq:heawood-face-sum}
+\sum_{v \in \partial f} h_\varphi(v) \;\equiv\; 0 \pmod 3
+\qquad\text{for every face $f$ of $H$,}
+\end{equation}
+which holds for any proper $3$-edge-colouring $\varphi$ of any cubic
+plane graph $H$.
+
+\begin{conjecture}[Deciding face]
+\label{conj:deciding-face}
+Let $G$ be a minimal counterexample to the Four Colour Theorem, let
+$\widehat{G}'_{v,i}$ be a reduced dual of $G'$, and let $\varphi$ be
+a chord-apex+Kempe colouring of $\widehat{G}'_{v,i}$. Write $K_b$ and
+$K_c$ for the two Kempe cycles through the spike edge
+(Lemma~\ref{lem:kempe-spike}). Then $\widehat{G}'_{v,i}$ has a face
+$f$ satisfying
+\[
+\partial f \subseteq V(K_b) \cup V(K_c)
+\qquad\text{and}\qquad
+|f| \not\equiv 0 \pmod 3.
+\]
+\end{conjecture}
+
+\begin{theorem}
+\label{thm:deciding-face-implies-conj-5-1}
+Conjecture~\ref{conj:deciding-face} implies
+Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}.
+\end{theorem}
+
+\begin{proof}
+We argue by contradiction. Suppose
+Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
+fails: there exist a minimal counterexample $G$, a reduced dual
+$\widehat{G}'_{v,i}$, and a chord-apex+Kempe colouring $\varphi$ of
+$\widehat{G}'_{v,i}$ admitting no clauses-(1)-(3) witness of
+Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}.
+
+By Lemma~\ref{lem:both-kempe-constant}, the absence of any
+clauses-(1)-(3) witness forces $h_\varphi$ to be constant on
+$V(K_b) \cup V(K_c)$; write the common value as
+$\varepsilon \in \{+1, -1\}$.
+
+By Conjecture~\ref{conj:deciding-face}, there is a face $f$ of
+$\widehat{G}'_{v,i}$ with $\partial f \subseteq V(K_b) \cup V(K_c)$
+and $|f| \not\equiv 0 \pmod 3$. Applying~\eqref{eq:heawood-face-sum}
+to $f$ and using $h_\varphi(v) = \varepsilon$ for every
+$v \in \partial f$:
+\[
+\sum_{v \in \partial f} h_\varphi(v)
+  \;=\; \varepsilon \cdot |f|
+  \;\equiv\; 0 \pmod 3.
+\]
+Since $3$ is prime and $\gcd(|f|, 3) = 1$, we obtain
+$\varepsilon \equiv 0 \pmod 3$. But $\varepsilon \in \{+1, -1\}$,
+so $\varepsilon \not\equiv 0 \pmod 3$ --- contradiction.
+\end{proof}
+
+\begin{remark}[Empirical verification of
+Conjecture~\ref{conj:deciding-face}]
+\label{rem:deciding-face-empirical}
+We have verified
+Conjecture~\ref{conj:deciding-face} computationally on every
+chord-apex+Kempe colouring of every reduced dual of every
+triangulation $G$ of minimum degree $5$ with $|V(G)| \le 20$. Across
+$142{,}812$ such colourings, every single one admits a deciding face.
+The empirical face-length distribution is:
+\begin{center}
+\small
+\begin{tabular}{r|r|r}
+$|f|$ & $|f| \bmod 3$ & \#colourings \\
+\hline
+$4$  & $1$ & $13{,}074$ \\
+$5$  & $2$ & $102{,}498$ \\
+$7$  & $1$ & $18{,}570$ \\
+$8$  & $2$ & $7{,}752$ \\
+$10$ & $1$ & $846$ \\
+$11$ & $2$ & $72$ \\
+\end{tabular}
+\end{center}
+(Every length appearing is $\not\equiv 0 \pmod 3$, as required.)
+See \texttt{experiments/check\_deciding\_face.py}.
+
+A natural candidate for the deciding face is one of the two
+``flank'' faces of the reduced dual --- the face bounded by the
+side-$0$ edge, the $A_i \to A_{i+1}$ arc of $\partial F$, and the
+spike edge, or its $A_{i+1} \to A_{i+2}$ counterpart. When the
+parent triangulation's vertex $v$ has a degree-$5$ neighbour $B_k$
+(i.e.\ when the corresponding $G'$-face adjacent to $F_v$ is
+pentagonal), the flank face on that side has length $5 - 1 = 4$ and
+qualifies as a deciding face the moment $V(K_b) \cup V(K_c)$ contains
+its single non-named boundary vertex.
+\end{remark}
+
 \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