face_monochromatic_pairs: per-cycle refinement + Corollary 5.4

Empirical refinement of Lemma 5.3: h_phi is non-constant on V(K_b)
alone (not just on the union) and likewise on V(K_c) alone, in every
one of 142,812 chord-apex+Kempe colourings tested (n in [12, 20]).
This is strictly stronger than what we previously reported.

The proof of Lemma 5.3 already constructs the (F, e_1, e_2) witness
from any consecutive same-Heawood failure on either Kempe cycle
through merged -- never needing the other cycle. Pull that out into
a separate Corollary 5.4 ("Per-cycle form"), which makes the
empirical-to-conjecture path more direct.

Update Remark 5.5 to:
  - Cite Corollary 5.4 instead of the contrapositive of Lemma 5.3.
  - Replace "non-constant on V(K_b) U V(K_c)" with the per-cycle form.
  - Extend the empirical table with separate columns for K_b and K_c
    non-constancy.

Also commit experiments/check_constancy_obstruction.py, the script
that produced these refined empirical findings. It additionally
records that no single named vertex (v_n, A_i, ..., A_{i+4}) is
structurally majority or minority -- the minority rates cluster in
31-39%, ruling out a single-vertex-mismatch identity.

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

papers/face_monochromatic_pairs/paper.tex

@@ -795,43 +795,67 @@ cycles, so its two endpoints --- which lie on $V(K_b) \cap V(K_c)$ ---
 force the two constants to coincide.
 \end{proof}
 
-\begin{remark}[Empirical near-proof of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} via Lemma~\ref{lem:both-kempe-constant}]
+\begin{corollary}[Per-cycle form]
+\label{cor:single-cycle-non-constancy}
+Let $G$, $\widehat{G}'_{v,i}$, $\varphi$ be as in
+Lemma~\ref{lem:both-kempe-constant}, and let $K$ be either of the two
+Kempe cycles of $\varphi$ through the merged edge. If $h_\varphi$ is not
+constant on $V(K)$, then a triple $(F, e_1, e_2)$ satisfying
+clauses~(1)--(3) of
+Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} on
+$(G, \widehat{G}'_{v,i}, \varphi)$ exists.
+\end{corollary}
+
+\begin{proof}
+This is precisely the case analysis used to prove
+Lemma~\ref{lem:both-kempe-constant}: applied to any consecutive pair of
+vertices on $K$ with differing Heawood numbers, the construction in
+that proof produces a clauses-(1)--(3) witness without ever needing to
+inspect the other Kempe cycle.
+\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
-The contrapositive of Lemma~\ref{lem:both-kempe-constant} reduces
-Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} to
-the following structural claim:
+By Corollary~\ref{cor:single-cycle-non-constancy},
+Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
+follows from the (a~priori weaker) structural claim:
 \emph{for every chord-apex+Kempe colouring $\varphi$ of every reduced
-dual $\widehat{G}'_{v,i}$, $h_\varphi$ is not constant on
-$V(K_b) \cup V(K_c)$.} We have verified this claim computationally on
-all chord-apex+Kempe colourings of reduced duals with $|V(G)| \le 20$
-(including the six Holton--McKay duals at $n = 21$ as a special case);
-see \texttt{experiments/check\_heawood\_on\_kempe.py}.
+dual $\widehat{G}'_{v,i}$, $h_\varphi$ is not constant on $V(K_b)$
+(equivalently, not constant on $V(K_c)$).} We have verified this claim
+computationally on all chord-apex+Kempe colourings of reduced duals
+with $|V(G)| \le 20$ (including the six Holton--McKay duals at
+$n = 21$ as a special case); see
+\texttt{experiments/check\_heawood\_on\_kempe.py} and
+\texttt{experiments/check\_constancy\_obstruction.py}.
 \begin{center}
 \small
 \renewcommand{\arraystretch}{1.15}
-\begin{tabular}{r|r|r|l}
-$n$ & \#col.\ tested & \#non-constant on $V(K_b)\cup V(K_c)$ & status \\
+\begin{tabular}{r|r|r|r|l}
+$n$ & \#col.\ tested
+    & \#non-const. on $V(K_b)$
+    & \#non-const. on $V(K_c)$ & status \\
 \hline
-$14$ & $216$       & $216$       & all non-constant \\
-$16$ & $864$       & $864$       & all non-constant \\
-$17$ & $4{,}650$   & $4{,}650$   & all non-constant \\
-$18$ & $8{,}070$   & $8{,}070$   & all non-constant \\
-$19$ & $21{,}138$  & $21{,}138$  & all non-constant \\
-$20$ & $107{,}874$ & $107{,}874$ & all non-constant \\
+$14$ & $216$       & $216$       & $216$       & all non-constant \\
+$16$ & $864$       & $864$       & $864$       & all non-constant \\
+$17$ & $4{,}650$   & $4{,}650$   & $4{,}650$   & all non-constant \\
+$18$ & $8{,}070$   & $8{,}070$   & $8{,}070$   & all non-constant \\
+$19$ & $21{,}138$  & $21{,}138$  & $21{,}138$  & all non-constant \\
+$20$ & $107{,}874$ & $107{,}874$ & $107{,}874$ & all non-constant \\
 \hline
-total ($n \le 20$) & $142{,}812$ & $142{,}812$ & \\
+total ($n \le 20$) & $142{,}812$ & $142{,}812$ & $142{,}812$ & \\
 \end{tabular}
 \end{center}
-\noindent Since $h_\varphi$ on $V(K_b) \cup V(K_c)$ was non-constant in
-every tested colouring, Lemma~\ref{lem:both-kempe-constant}'s
-contrapositive supplies a Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
-witness in each case --- giving an empirical near-proof of the
-conjecture for $|V(G)| \le 20$ that is independent of (and consistent
-with) the direct witness-search check of
-Remark~\ref{rem:conj-3-6-empirical}. A structural proof of
-non-constancy on $V(K_b) \cup V(K_c)$ would convert this into a proof
-of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
+\noindent In particular, $h_\varphi$ is non-constant on $V(K_b)$ alone
+in every tested colouring (and likewise on $V(K_c)$); by
+Corollary~\ref{cor:single-cycle-non-constancy} each such colouring
+admits a Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
+witness. This gives an empirical near-proof of the conjecture for
+$|V(G)| \le 20$ independent of (and consistent with) the direct
+witness-search check of Remark~\ref{rem:conj-3-6-empirical}. A
+structural proof of non-constancy on $V(K_b)$ (or on $V(K_c)$) would
+convert this into a proof of
+Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
 proper.
 \end{remark}