face_monochromatic_pairs: sanity-check on G'-pentagon fallback — pigeonhole stops at |S|=1

Per user's request: try option 3 (push case analysis) as a sanity
check on the G'-pentagon fallback conjecture. Result: trivial
pigeonhole closes the |S| ≤ 1 case but no further.

Added:
  - Lemma (Partial proof, |S| ≤ 1): a single uncovered vertex hits
    at most 3 of the ≥ 6 G'-pentagons of the reduced dual, so 3
    pentagons remain fully covered. Trivial pigeonhole.
  - Remark "The pigeonhole stops at |S| = 1; the proof begins to
    resemble discharging": Theorem deciding-face-partial-extended
    + Lemma gprime-pigeonhole cover ~91% of chord-apex+Kempe
    configurations (73.87% with |S|=0 + 17% with |S|=1). The
    remaining ~9% have |S| ≥ 2 and need finer graph-structural
    input, exactly the discharging flavour Appel-Haken / RSST /
    Gonthier used for 4CT. We stop the case-by-case route here.

So the sanity check confirms the user's intuition: continuing the
case analysis would replay the irreducible-configurations approach
in different vocabulary. Pivoting to option 2 (global argument)
next.

Paper stays at 22 pages.

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

papers/face_monochromatic_pairs/paper.tex

@@ -1286,6 +1286,53 @@ face of $G'$ not equal to $F_v$ or to any of $F_i, \ldots, F_{i+4}$)
 satisfies $\partial f \subseteq V(K_b) \cup V(K_c)$.
 \end{conjecture}
 
+\begin{lemma}[Partial proof of
+Conjecture~\ref{conj:gprime-pentagon-fallback} for small uncovered
+set]
+\label{lem:gprime-pigeonhole}
+If $|V(\widehat{G}'_{v,i}) \setminus (V(K_b) \cup V(K_c))| \le 1$,
+then Conjecture~\ref{conj:gprime-pentagon-fallback} holds.
+\end{lemma}
+
+\begin{proof}
+The reduced dual contains at least $12 - 1 - 5 = 6$ $G'$-pentagons
+(from the classical lower bound of $12$ pentagons on any cubic plane
+graph with all faces of length $\ge 5$, minus $F_v$ and the five
+faces $F_i, \ldots, F_{i+4}$ that the reduction subdivides). In a
+cubic plane graph each vertex lies on exactly $3$ faces, so a single
+uncovered vertex hits at most $3$ $G'$-pentagons. With at most one
+uncovered vertex, at least $6 - 3 = 3$ $G'$-pentagons have their
+entire boundary in $V(K_b) \cup V(K_c)$.
+\end{proof}
+
+\begin{remark}[The pigeonhole stops at $|S| = 1$;
+\textbf{the proof begins to resemble discharging}]
+\label{rem:gprime-pigeonhole-stop}
+Lemma~\ref{lem:gprime-pigeonhole} adds significant structural
+coverage. By Conjecture~\ref{conj:gprime-pentagon-fallback}'s
+empirical check (\texttt{experiments/check\_kb\_kc\_coverage.py}),
+$73.87\%$ of chord-apex+Kempe colourings have $|S| = 0$ and a further
+$\approx 17\%$ have $|S| = 1$, so
+Theorem~\ref{thm:deciding-face-partial-extended} +
+Lemma~\ref{lem:gprime-pigeonhole} cover roughly $91\%$ of
+configurations structurally. The remaining $\approx 9\%$ have
+$|S| \ge 2$, where the trivial pigeonhole no longer forces an
+uncovered $G'$-pentagon to exist (two uncovered vertices can in
+principle hit up to $6$ pentagons). Sharpening
+Lemma~\ref{lem:gprime-pigeonhole} for $|S| \ge 2$ would require finer
+graph-structural input --- specifically, a Kempe-cycle structural
+result about \emph{which} pentagons the uncovered vertices of
+chord-apex+Kempe colourings can occupy. This is exactly the discharging
+flavour of the traditional reducible-configurations approach to the
+Four Colour Theorem (Appel--Haken~\cite{AH77a, AHK77},
+Robertson--Sanders--Seymour--Thomas~\cite{RSST97},
+Gonthier~\cite{Gonthier08}), and we expect the structural case
+analysis to fragment further as $|S|$ increases. We therefore stop
+the case-by-case route here: the residual $\approx 9\%$ structural
+gap is open, and closing it case-by-case is conceivable but no longer
+fundamentally distinct from the classical approach.
+\end{remark}
+
 If Conjecture~\ref{conj:gprime-pentagon-fallback} is true, then together
 with Theorem~\ref{thm:deciding-face-partial-extended} it gives a
 structural proof of the deciding-face conjecture for every