diff --git a/papers/face_monochromatic_pairs/experiments/check_deciding_face.py b/papers/face_monochromatic_pairs/experiments/check_deciding_face.py
new file mode 100644
index 0000000..47c78c0
--- /dev/null
+++ b/papers/face_monochromatic_pairs/experiments/check_deciding_face.py
@@ -0,0 +1,161 @@
+"""For every chord-apex+Kempe colouring of every reduced dual (up to
+|V(G)| ≤ 18), check whether there exists a "deciding face": a face f
+of the reduced dual whose boundary lies entirely in V(K_b) ∪ V(K_c)
+and whose length is not divisible by 3.
+
+If a deciding face exists, then under the (hypothetical) constancy
+hypothesis h_φ ≡ ε on V(K_b) ∪ V(K_c), Heawood's face-sum identity
+gives ε · |f| ≡ 0 (mod 3), which forces ε ≡ 0 since |f| ≢ 0 (mod 3) --
+contradicting ε ∈ {±1}. So existence of a deciding face in every
+chord-apex+Kempe colouring of every reduced dual would *prove*
+Conjecture 5.1 via the contrapositive of Lemma 5.3.
+
+This script reports, per (n_G, colouring): does a deciding face exist?
+And if not, why not (insufficient coverage, all in-coverage faces have
+length ≡ 0 mod 3, etc.).
+
+Run with: sage experiments/check_deciding_face.py
+"""
+import os
+import sys
+import time
+
+from sage.all import Graph
+from sage.graphs.graph_generators import graphs
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, HERE)
+
+from check_conj_3_8_scaled import (
+    apply_reduction,
+    proper_3_edge_colorings,
+    matches_chord_apex_kempe,
+    kempe_cycle_set,
+    edge_idx,
+)
+from check_heawood_on_kempe import (
+    dual_of, vertices_of_kempe,
+)
+
+
+def find_deciding_face(H, V_union):
+    """Return (face, |face| mod 3) of a deciding face (all boundary in
+    V_union, length not divisible by 3). None if no such face exists."""
+    for face in H.faces():
+        verts = {u for (u, v) in face} | {v for (u, v) in face}
+        if not verts.issubset(V_union):
+            continue
+        L = len(face)
+        if L % 3 != 0:
+            return face, L, L % 3
+    return None
+
+
+def test_one(D):
+    D.is_planar(set_embedding=True)
+    n_col = 0
+    n_with_deciding = 0
+    no_deciding_examples = []
+    deciding_lengths = {}   # |f| of deciding face -> count
+    for face in D.faces():
+        if len(face) != 5: continue
+        for i_red in range(5):
+            res = apply_reduction(D, face, i_red, 9999)
+            if res is None: continue
+            H = res['H']; named = res['named']
+            H.is_planar(set_embedding=True)
+            edges, colorings = proper_3_edge_colorings(H)
+            cand = [c for c in colorings
+                    if matches_chord_apex_kempe(edges, c, named)]
+            for col in cand:
+                n_col += 1
+                merged_idx = edge_idx(edges, named['merged'])
+                a = col[merged_idx]
+                bs = [c for c in range(3) if c != a]
+                kc_b = kempe_cycle_set(edges, col, merged_idx, (a, bs[0]))
+                kc_c = kempe_cycle_set(edges, col, merged_idx, (a, bs[1]))
+                V_b = vertices_of_kempe(edges, kc_b)
+                V_c = vertices_of_kempe(edges, kc_c)
+                V_union = V_b | V_c
+                deciding = find_deciding_face(H, V_union)
+                if deciding is not None:
+                    n_with_deciding += 1
+                    _, L, mod_r = deciding
+                    deciding_lengths[L] = deciding_lengths.get(L, 0) + 1
+                else:
+                    cov_ratio = len(V_union) / H.order()
+                    in_cov_face_lens = sorted([
+                        len(f) for f in H.faces()
+                        if {u for (u, v) in f} | {v for (u, v) in f}
+                           <= V_union])
+                    if len(no_deciding_examples) < 3:
+                        no_deciding_examples.append({
+                            'cov_ratio': cov_ratio,
+                            'in_cov_face_lens': in_cov_face_lens,
+                            'V_union_size': len(V_union),
+                            'V_total': H.order(),
+                        })
+    return n_col, n_with_deciding, deciding_lengths, no_deciding_examples
+
+
+def main(max_n=20, time_budget_per_n=1800):
+    print(f"Deciding-face existence on chord-apex+Kempe colourings, "
+          f"n_G ∈ [12, {max_n}]\n")
+    grand_col = 0
+    grand_dec = 0
+    grand_lens = {}
+    grand_no_dec_examples = []
+    for n in range(12, max_n + 1):
+        start = time.time()
+        try:
+            triangulations = list(graphs.triangulations(n, minimum_degree=5))
+        except Exception as ex:
+            print(f"n={n}: cannot enumerate ({ex})")
+            continue
+        n_col_n = 0
+        n_dec_n = 0
+        for tri_idx, G in enumerate(triangulations):
+            if time.time() - start > time_budget_per_n:
+                print(f"  n={n}: timeout at tri {tri_idx}/{len(triangulations)}")
+                break
+            G.is_planar(set_embedding=True)
+            D = dual_of(G)
+            ni, ndec, lens, no_dec_ex = test_one(D)
+            n_col_n += ni
+            n_dec_n += ndec
+            for k, v in lens.items():
+                grand_lens[k] = grand_lens.get(k, 0) + v
+            if len(grand_no_dec_examples) < 5:
+                grand_no_dec_examples.extend(
+                    no_dec_ex[:5 - len(grand_no_dec_examples)])
+        elapsed = time.time() - start
+        pct = 100 * n_dec_n / max(n_col_n, 1)
+        print(f"n={n}: {n_col_n} col., {n_dec_n} with deciding face "
+              f"({pct:.2f}%) [{elapsed:.0f}s]")
+        sys.stdout.flush()
+        grand_col += n_col_n
+        grand_dec += n_dec_n
+
+    print()
+    print("=" * 70)
+    print(f"Grand totals: {grand_col} chord-apex+Kempe colourings")
+    pct = 100 * grand_dec / max(grand_col, 1)
+    print(f"  with deciding face: {grand_dec} ({pct:.2f}%)")
+    print(f"  without          : {grand_col - grand_dec} "
+          f"({100 - pct:.2f}%)")
+    if grand_lens:
+        print()
+        print("  Deciding face length distribution:")
+        for L in sorted(grand_lens):
+            print(f"    |f| = {L} (mod 3 = {L % 3}): {grand_lens[L]}")
+    if grand_no_dec_examples:
+        print()
+        print("  Sample colourings WITHOUT a deciding face:")
+        for ex in grand_no_dec_examples[:5]:
+            print(f"    coverage = {ex['V_union_size']}/{ex['V_total']} "
+                  f"({100*ex['cov_ratio']:.0f}%); in-coverage face "
+                  f"lengths = {ex['in_cov_face_lens']}")
+
+
+if __name__ == '__main__':
+    main()
diff --git a/papers/face_monochromatic_pairs/experiments/check_kb_kc_coverage.py b/papers/face_monochromatic_pairs/experiments/check_kb_kc_coverage.py
new file mode 100644
index 0000000..bfa2ec0
--- /dev/null
+++ b/papers/face_monochromatic_pairs/experiments/check_kb_kc_coverage.py
@@ -0,0 +1,132 @@
+"""Check what fraction of V(Ĝ'_{v,i}) is covered by V(K_b) ∪ V(K_c)
+across all chord-apex+Kempe colourings of all reduced duals up to
+|V(G)| ≤ 18.
+
+This is the key prerequisite for the Heawood-face-sum proof attempt:
+if V(K_b) ∪ V(K_c) = V(reduced dual) in many cases, then under
+constancy on V(K_b) ∪ V(K_c) every face of the reduced dual must
+satisfy ε * |f| ≡ 0 (mod 3); since ε = ±1, this forces |f| ≡ 0 mod 3
+for every face -- and any reduced dual with a face of length 4, 5, or
+7 (etc., not multiple of 3) would yield an immediate contradiction.
+
+Run with: sage experiments/check_kb_kc_coverage.py
+"""
+import os
+import sys
+import time
+
+from sage.all import Graph
+from sage.graphs.graph_generators import graphs
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, HERE)
+
+from check_conj_3_8_scaled import (
+    apply_reduction,
+    proper_3_edge_colorings,
+    matches_chord_apex_kempe,
+    kempe_cycle_set,
+    edge_idx,
+)
+from check_heawood_on_kempe import (
+    dual_of, heawood_numbers, vertices_of_kempe,
+)
+
+
+def test_one(D):
+    D.is_planar(set_embedding=True)
+    n_col = 0
+    coverage_dist = {}  # |V(K_b)∪V(K_c)| / |V| as ratio (rounded) -> count
+    full_coverage = 0
+    face_lengths_at_full = {}  # face length distribution when full coverage
+    for face in D.faces():
+        if len(face) != 5: continue
+        for i_red in range(5):
+            res = apply_reduction(D, face, i_red, 9999)
+            if res is None: continue
+            H = res['H']; named = res['named']
+            H.is_planar(set_embedding=True)
+            edges, colorings = proper_3_edge_colorings(H)
+            cand = [c for c in colorings
+                    if matches_chord_apex_kempe(edges, c, named)]
+            n_v = H.order()
+            face_lens = sorted([len(f) for f in H.faces()])
+            for col in cand:
+                n_col += 1
+                merged_idx = edge_idx(edges, named['merged'])
+                a = col[merged_idx]
+                bs = [c for c in range(3) if c != a]
+                kc_b = kempe_cycle_set(edges, col, merged_idx, (a, bs[0]))
+                kc_c = kempe_cycle_set(edges, col, merged_idx, (a, bs[1]))
+                V_b = vertices_of_kempe(edges, kc_b)
+                V_c = vertices_of_kempe(edges, kc_c)
+                cov = len(V_b | V_c)
+                cov_ratio = cov / n_v
+                bucket = round(cov_ratio * 20) / 20   # bucket in 5% increments
+                coverage_dist[bucket] = coverage_dist.get(bucket, 0) + 1
+                if cov == n_v:
+                    full_coverage += 1
+                    key = tuple(face_lens)
+                    face_lengths_at_full[key] = (
+                        face_lengths_at_full.get(key, 0) + 1)
+    return n_col, coverage_dist, full_coverage, face_lengths_at_full
+
+
+def main(max_n=18, time_budget_per_n=300):
+    print(f"V(K_b) ∪ V(K_c) coverage / V(Ĝ'_{{v,i}}) "
+          f"on chord-apex+Kempe colourings, n_G ∈ [12, {max_n}]\n")
+    grand_col = 0
+    grand_dist = {}
+    grand_full = 0
+    grand_full_faces = {}
+    for n in range(12, max_n + 1):
+        start = time.time()
+        try:
+            triangulations = list(graphs.triangulations(n, minimum_degree=5))
+        except Exception as ex:
+            print(f"n={n}: cannot enumerate ({ex})")
+            continue
+        n_col_n = 0
+        n_full_n = 0
+        for tri_idx, G in enumerate(triangulations):
+            if time.time() - start > time_budget_per_n:
+                print(f"  n={n}: timeout at tri {tri_idx}/{len(triangulations)}")
+                break
+            G.is_planar(set_embedding=True)
+            D = dual_of(G)
+            ni, dist, full, full_faces = test_one(D)
+            n_col_n += ni
+            n_full_n += full
+            for k, v in dist.items():
+                grand_dist[k] = grand_dist.get(k, 0) + v
+            for k, v in full_faces.items():
+                grand_full_faces[k] = grand_full_faces.get(k, 0) + v
+        elapsed = time.time() - start
+        print(f"n={n}: {n_col_n} col., {n_full_n} full-coverage "
+              f"({100 * n_full_n / max(n_col_n, 1):.1f}%) [{elapsed:.0f}s]")
+        sys.stdout.flush()
+        grand_col += n_col_n
+        grand_full += n_full_n
+
+    print()
+    print("=" * 70)
+    print(f"Grand totals: {grand_col} chord-apex+Kempe colourings")
+    print(f"  full coverage (V(K_b)∪V(K_c) = V):  {grand_full} "
+          f"({100 * grand_full / max(grand_col, 1):.2f}%)")
+    print()
+    print("  Coverage ratio distribution "
+          "(|V(K_b)∪V(K_c)| / |V(Ĝ')|):")
+    for r in sorted(grand_dist):
+        c = grand_dist[r]
+        pct = 100 * c / max(grand_col, 1)
+        bar = '#' * max(1, int(pct))
+        print(f"    {r:5.2f}: {c:>7} ({pct:5.2f}%) {bar[:50]}")
+    if grand_full > 0:
+        print()
+        print("  Face-length distributions among full-coverage cases:")
+        for key in sorted(grand_full_faces, key=lambda k: -grand_full_faces[k]):
+            print(f"    {key}: {grand_full_faces[key]}")
+
+
+if __name__ == '__main__':
+    main()
diff --git a/papers/face_monochromatic_pairs/paper.pdf b/papers/face_monochromatic_pairs/paper.pdf
index 781053b..99348b8 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 619ccfe..a4035c0 100644
--- a/papers/face_monochromatic_pairs/paper.tex
+++ b/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