diff --git a/papers/face_monochromatic_pairs/experiments/search_min_face5_counterexample.py b/papers/face_monochromatic_pairs/experiments/search_min_face5_counterexample.py
new file mode 100644
index 0000000..1d30765
--- /dev/null
+++ b/papers/face_monochromatic_pairs/experiments/search_min_face5_counterexample.py
@@ -0,0 +1,137 @@
+"""Search for counterexamples to the strengthened Conjecture 5.5:
+
+   Let H be a cubic plane graph in which every face has length ≥ 5,
+   with a proper 3-edge-colouring φ. If K_0 = {a,b}-Kempe cycle and
+   K_1 = {a,c}-Kempe cycle share a colour-a edge, then h_φ cannot be
+   constant on both V(K_0) and V(K_1).
+
+The graphs H satisfying the face-length-≥-5 hypothesis are exactly
+the duals of triangulations of the sphere with minimum degree ≥ 5.
+We enumerate these via plantri (through Sage's
+`graphs.triangulations(n, minimum_degree=5)`), take the planar dual,
+and run the same Heawood-constancy check as
+`search_smaller_counterexample.py`.
+
+For each triangulation order n, the dual has 2n - 4 cubic vertices.
+The smallest case n = 12 is the icosahedron, whose dual is the
+dodecahedron (20 vertices, all faces pentagonal).
+
+Run with:
+  sage experiments/search_min_face5_counterexample.py        # default max_n=14
+  sage experiments/search_min_face5_counterexample.py 16
+  sage experiments/search_min_face5_counterexample.py 16 --all
+"""
+import sys
+import time
+
+from sage.all import Graph
+from sage.graphs.graph_generators import graphs
+
+# Reuse the verification machinery from the cubic-search script.
+import os
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, HERE)
+from search_smaller_counterexample import (
+    check_graph,
+    min_face_length,
+)
+
+
+def planar_dual(G):
+    """Build the planar dual of a planar graph G with its embedding
+    already set via G.is_planar(set_embedding=True)."""
+    faces = G.faces()
+    D = Graph(multiedges=False, loops=False)
+    n_faces = len(faces)
+    D.add_vertices(range(n_faces))
+    # Map each (undirected) edge of G to the indices of the two faces
+    # that contain it.
+    edge_to_faces = {}
+    for i, face in enumerate(faces):
+        for e in face:
+            key = frozenset(e[:2])
+            edge_to_faces.setdefault(key, []).append(i)
+    for key, fs in edge_to_faces.items():
+        if len(fs) == 2 and fs[0] != fs[1]:
+            D.add_edge(fs[0], fs[1])
+    return D
+
+
+def main():
+    args = [a for a in sys.argv[1:] if not a.startswith('--')]
+    max_n = int(args[0]) if args else 14
+    flag_all = '--all' in sys.argv[1:]
+
+    print(f"Searching for counterexamples to the face-length-≥-5 form "
+          f"of Conjecture 5.5.\n"
+          f"Iterating over triangulations with min degree ≥ 5 for "
+          f"n_T in [12, {max_n}].\n"
+          f"Each dual is cubic with all faces of length ≥ 5; the dual "
+          f"has 2n_T - 4 vertices.\n"
+          f"{'Continuing past first hit.' if flag_all else 'Stopping at first hit.'}\n")
+
+    first_found = None
+    for n_T in range(12, max_n + 1):
+        start = time.time()
+        count = 0
+        found = None
+        try:
+            gen = graphs.triangulations(n_T, minimum_degree=5)
+        except Exception as ex:
+            print(f"n_T={n_T:>3}: cannot enumerate ({ex})")
+            continue
+        for T in gen:
+            T.is_planar(set_embedding=True)
+            H = planar_dual(T)
+            n_H = H.order()
+            # Sanity: H should be cubic and planar; faces length ≥ 5.
+            if max(H.degree()) != 3 or min(H.degree()) != 3:
+                continue
+            if not H.is_planar(set_embedding=True):
+                continue
+            if min_face_length(H) < 5:
+                continue
+            count += 1
+            res = check_graph(H)
+            if res is not None:
+                found = (T.copy(), H.copy(), res, n_H)
+                if not flag_all:
+                    break
+        elapsed = time.time() - start
+        n_H_min = 2 * n_T - 4
+        if found is None:
+            print(f"n_T={n_T:>3}: checked {count} triangulation duals "
+                  f"(each with {n_H_min} cubic vertices), no counterexample "
+                  f"[{elapsed:.1f}s]")
+        else:
+            T, H, (col, K0, K1, h0, h1, a, b, c, e), n_H = found
+            colour_name = {0: 'red', 1: 'blue', 2: 'green'}
+            print(f"n_T={n_T:>3}: COUNTEREXAMPLE in dual #{count} "
+                  f"(|V(H)| = {n_H}) [{elapsed:.1f}s]")
+            print(f"  triangulation canonical graph6 = "
+                  f"{T.canonical_label().graph6_string()}")
+            print(f"  dual (cubic) canonical graph6 = "
+                  f"{H.canonical_label().graph6_string()}")
+            print(f"  dual edges    = {sorted(H.edges(labels=False))}")
+            print(f"  colouring     = {col}")
+            print(f"  shared colour = {colour_name[a]} ({a}), edge {e}")
+            print(f"  K_{{a,b}} = K_{{{colour_name[a]},{colour_name[b]}}} "
+                  f"= {K0}  (h={h0:+d}, |V|={len(K0)})")
+            print(f"  K_{{a,c}} = K_{{{colour_name[a]},{colour_name[c]}}} "
+                  f"= {K1}  (h={h1:+d}, |V|={len(K1)})")
+            if first_found is None:
+                first_found = n_T
+            if not flag_all:
+                break
+        sys.stdout.flush()
+
+    if first_found is not None:
+        print(f"\nSmallest counterexample at triangulation order n_T "
+              f"= {first_found} (dual has {2 * first_found - 4} vertices).")
+    else:
+        print(f"\nNo counterexample found for triangulation orders ≤ "
+              f"{max_n} (dual orders ≤ {2 * max_n - 4}).")
+
+
+if __name__ == '__main__':
+    main()
diff --git a/papers/face_monochromatic_pairs/experiments/search_smaller_counterexample.py b/papers/face_monochromatic_pairs/experiments/search_smaller_counterexample.py
index f1ac02b..c583b35 100644
--- a/papers/face_monochromatic_pairs/experiments/search_smaller_counterexample.py
+++ b/papers/face_monochromatic_pairs/experiments/search_smaller_counterexample.py
@@ -146,19 +146,45 @@ def check_graph(G):
     return None
 
 
+def min_face_length(G):
+    """Min face length of G in its current planar embedding."""
+    return min(len(f) for f in G.faces())
+
+
 def main():
     args = [a for a in sys.argv[1:] if not a.startswith('--')]
     max_n = int(args[0]) if args else 18
     flag_all = '--all' in sys.argv[1:]
+    # Parse --min-face N
+    min_face = None
+    for i, a in enumerate(sys.argv[1:]):
+        if a == '--min-face' and i + 1 < len(sys.argv) - 1:
+            min_face = int(sys.argv[i + 2])
+            break
+        if a.startswith('--min-face='):
+            min_face = int(a.split('=', 1)[1])
+            break
 
     print(f"Searching for cubic plane graph counterexamples to "
           f"Conjecture 5.5, n in [4, {max_n}] "
-          f"({'continuing past first hit' if flag_all else 'stopping at first hit'})\n")
+          f"({'continuing past first hit' if flag_all else 'stopping at first hit'})"
+          + (f", min face length >= {min_face}" if min_face else "")
+          + "\n")
+
+    # If filtering by min face length, skip small n where impossible.
+    # For all-faces-length->=L cubic plane: V - E + F = 2, E = 3V/2,
+    # sum face lengths = 3V, F = V/2 + 2, so min sum = L*(V/2 + 2)
+    # <= 3V gives V >= 2L*(L-3)/(3-L/2)... let's just set V >= 20 for L=5.
+    if min_face is not None and min_face >= 5:
+        n_start = max(4, 20)
+    else:
+        n_start = 4
 
     first_found = None
-    for n in range(4, max_n + 1, 2):   # cubic requires n even
+    for n in range(n_start, max_n + 1, 2):   # cubic requires n even
         start = time.time()
         count = 0
+        skipped = 0
         found = None
         try:
             gen = graphs.planar_graphs(
@@ -172,6 +198,11 @@ def main():
         for G in gen:
             if max(G.degree()) != 3:
                 continue   # not cubic
+            if min_face is not None:
+                G.is_planar(set_embedding=True)
+                if min_face_length(G) < min_face:
+                    skipped += 1
+                    continue
             count += 1
             res = check_graph(G)
             if res is not None:
@@ -180,8 +211,10 @@ def main():
                     break
         elapsed = time.time() - start
         if found is None:
-            print(f"n={n:>3}: checked {count} graphs, no counterexample "
-                  f"[{elapsed:.1f}s]")
+            extra = (f", skipped {skipped} due to small face"
+                     if min_face is not None else "")
+            print(f"n={n:>3}: checked {count} graphs, no counterexample"
+                  f"{extra} [{elapsed:.1f}s]")
         else:
             G, (col, K0, K1, h0, h1, a, b, c, e) = found
             colour_name = {0: 'red', 1: 'blue', 2: 'green'}
diff --git a/papers/face_monochromatic_pairs/experiments/verify_28_vertex_counterexample.py b/papers/face_monochromatic_pairs/experiments/verify_28_vertex_counterexample.py
new file mode 100644
index 0000000..000b7d7
--- /dev/null
+++ b/papers/face_monochromatic_pairs/experiments/verify_28_vertex_counterexample.py
@@ -0,0 +1,120 @@
+"""Verify the n=28 counterexample (smallest dual of min-degree-5
+triangulation that violates the face-length-≥-5 form of Conjecture
+5.5) and render a planar PNG of it.
+
+The graph H is the planar dual of a 16-vertex triangulation with
+min degree ≥ 5 (the 3rd one in sage's enumeration). It has 28
+vertices, 42 edges, and all faces of length ≥ 5. The colouring shown
+below makes K_{red, blue} and K_{red, green} both 12-cycles sharing
+the colour-red edge (0, 1) with h_φ ≡ -1 on each.
+
+Run with: sage experiments/verify_28_vertex_counterexample.py
+"""
+import os
+import sys
+import math
+
+from sage.all import Graph
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, HERE)
+from search_smaller_counterexample import (
+    edge_key, heawood_numbers, trace_kempe,
+)
+
+OUT_PNG = os.path.join(HERE, '..', 'figures', 'min-face-5-counterexample.png')
+
+# Dual edges and the discovered colouring (sorted-edge order).
+EDGES_LIST = [
+    (0, 1), (0, 4), (0, 6), (1, 2), (1, 5), (2, 3), (2, 8), (3, 4),
+    (3, 11), (4, 13), (5, 7), (5, 9), (6, 7), (6, 15), (7, 17),
+    (8, 10), (8, 12), (9, 10), (9, 19), (10, 20), (11, 12), (11, 14),
+    (12, 22), (13, 14), (13, 16), (14, 23), (15, 16), (15, 18),
+    (16, 25), (17, 18), (17, 19), (18, 26), (19, 21), (20, 21),
+    (20, 22), (21, 27), (22, 24), (23, 24), (23, 25), (24, 27),
+    (25, 26), (26, 27),
+]
+COLOURING = (0, 1, 2, 2, 1, 1, 0, 2, 0, 0, 2, 0, 1, 0, 0, 1, 2, 2,
+             1, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 0, 2, 1, 1,
+             2, 1, 2, 0, 1, 2)
+COLOUR_NAME = {0: 'red', 1: 'blue', 2: 'green'}
+
+
+def build():
+    G = Graph(multiedges=False, loops=False)
+    for u, v in EDGES_LIST:
+        G.add_edge(u, v)
+    # Sage's sorted edges should align with EDGES_LIST.
+    edges_sorted = sorted([edge_key(u, v) for (u, v) in G.edge_iterator(labels=False)])
+    assert edges_sorted == EDGES_LIST, "edge order mismatch"
+    col_of_edge = {edges_sorted[i]: COLOURING[i] for i in range(len(edges_sorted))}
+    return G, col_of_edge
+
+
+def main():
+    G, col_of_edge = build()
+    print(f"|V| = {G.order()}, |E| = {G.size()}")
+    assert G.is_planar(set_embedding=True)
+    print(f"face lengths: {sorted([len(f) for f in G.faces()])}")
+    assert all(len(f) >= 5 for f in G.faces()), "face length < 5"
+    # Verify proper 3-edge-colouring.
+    for v in G.vertex_iterator():
+        cs = sorted(col_of_edge[edge_key(v, u)] for u in G.neighbors(v))
+        assert cs == [0, 1, 2], f"vertex {v} colours {cs}"
+    print("proper 3-edge-colouring ✓")
+
+    h = heawood_numbers(G, col_of_edge)
+    plus = sum(1 for v in h if h[v] == +1)
+    minus = sum(1 for v in h if h[v] == -1)
+    print(f"global h_φ: {plus} (+1) / {minus} (-1)")
+
+    # Verify both Kempe cycles through (0, 1) are constant.
+    K0 = trace_kempe(G, col_of_edge, (0, 1), (0, 1))   # red+blue
+    K1 = trace_kempe(G, col_of_edge, (0, 1), (0, 2))   # red+green
+    h_K0 = [h[v] for v in K0]
+    h_K1 = [h[v] for v in K1]
+    print(f"K_{{red, blue}}  (len {len(K0)}): {K0}, h = {h_K0[0]} (const? {len(set(h_K0))==1})")
+    print(f"K_{{red, green}} (len {len(K1)}): {K1}, h = {h_K1[0]} (const? {len(set(h_K1))==1})")
+    print(f"V(K0) ∪ V(K1)| = {len(set(K0) | set(K1))} / {G.order()}")
+
+    # Canonical graph6
+    print(f"canonical graph6 = {G.canonical_label().graph6_string()}")
+
+    # Render PNG with planar layout
+    import matplotlib
+    matplotlib.use('Agg')
+    import matplotlib.pyplot as plt
+
+    pos = G.layout_planar()
+    fig, ax = plt.subplots(figsize=(10, 10), dpi=160)
+    ax.set_aspect('equal')
+    ax.axis('off')
+    for (u, v) in G.edge_iterator(labels=False):
+        c = COLOUR_NAME[col_of_edge[edge_key(u, v)]]
+        x1, y1 = pos[u]; x2, y2 = pos[v]
+        ax.plot([x1, x2], [y1, y2], color=c, linewidth=2.0, solid_capstyle='round')
+    K0set = set(K0); K1set = set(K1)
+    for v, (x, y) in pos.items():
+        if v in K0set and v in K1set:
+            face_c = '#bbbbff'   # on both cycles
+        elif v in K0set or v in K1set:
+            face_c = '#ddddff'
+        else:
+            face_c = 'lightgrey'
+        ax.plot(x, y, 'o', markersize=18, markerfacecolor=face_c,
+                markeredgecolor='black', markeredgewidth=1.0)
+        ax.text(x, y, str(v), ha='center', va='center', fontsize=8)
+    xs = [p[0] for p in pos.values()]
+    ys = [p[1] for p in pos.values()]
+    pad = 0.5
+    ax.set_xlim(min(xs) - pad, max(xs) + pad)
+    ax.set_ylim(min(ys) - pad, max(ys) + pad)
+    os.makedirs(os.path.dirname(OUT_PNG), exist_ok=True)
+    fig.tight_layout()
+    fig.savefig(OUT_PNG, dpi=160, bbox_inches='tight')
+    plt.close(fig)
+    print(f"\nWrote: {OUT_PNG}")
+
+
+if __name__ == '__main__':
+    main()
diff --git a/papers/face_monochromatic_pairs/figures/min-face-5-counterexample.png b/papers/face_monochromatic_pairs/figures/min-face-5-counterexample.png
new file mode 100644
index 0000000..a174186
Binary files /dev/null and b/papers/face_monochromatic_pairs/figures/min-face-5-counterexample.png differ
diff --git a/papers/face_monochromatic_pairs/paper.pdf b/papers/face_monochromatic_pairs/paper.pdf
index 24fde31..3948784 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 8b302de..d3a80df 100644
--- a/papers/face_monochromatic_pairs/paper.tex
+++ b/papers/face_monochromatic_pairs/paper.tex
@@ -814,65 +814,64 @@ that proof produces a clauses-(1)--(3) witness without ever needing to
 inspect the other Kempe cycle.
 \end{proof}
 
-\begin{conjecture}[Constant Heawood on two edge-sharing Kempe cycles --- \textbf{FALSE}]
+\begin{conjecture}[Constant Heawood on two edge-sharing Kempe cycles, large-face cubic plane graphs]
 \label{conj:no-two-constant-kempe-cycles}
-Let $H$ be a cubic plane graph with a proper $3$-edge-colouring
-$\varphi$, fix a colour $a \in \{1, 2, 3\}$, and let $\{b, c\} =
-\{1, 2, 3\} \setminus \{a\}$. Let $K_0$ be an $\{a, b\}$-Kempe cycle
-of $\varphi$ and $K_1$ an $\{a, c\}$-Kempe cycle of $\varphi$ such that
+Let $H$ be a cubic plane graph in which every face has length at
+least $5$, with a proper $3$-edge-colouring $\varphi$. Fix a colour
+$a \in \{1, 2, 3\}$ and let $\{b, c\} = \{1, 2, 3\} \setminus \{a\}$.
+Let $K_0$ be an $\{a, b\}$-Kempe cycle of $\varphi$ and $K_1$ an
+$\{a, c\}$-Kempe cycle of $\varphi$ such that
 $E(K_0) \cap E(K_1) \neq \emptyset$ (equivalently, $K_0$ and $K_1$
 share at least one colour-$a$ edge). If $h_\varphi$ is constant on
 $V(K_0)$, then $h_\varphi$ is \emph{not} constant on $V(K_1)$.
 \end{conjecture}
 
-\begin{remark}[Disproof of
-Conjecture~\ref{conj:no-two-constant-kempe-cycles}]
-\label{rem:no-two-constant-kempe-cycles-counterexample}
-Conjecture~\ref{conj:no-two-constant-kempe-cycles} is \emph{false}.
-Figure~\ref{fig:no-two-constant-kempe-counterexample} exhibits a
-concrete counterexample: a cubic plane graph $H$ on $40$ vertices with
-a proper $3$-edge-colouring $\varphi$ (colours red/blue/green) in
-which both
-\begin{align*}
-K_{\mathrm{red},\mathrm{blue}}
-  &= \text{the outer $8$-cycle, and} \\
-K_{\mathrm{red},\mathrm{green}}
-  &= \text{the $12$-cycle (outer frame $+$ upper-left ``ladder'' side)}
-\end{align*}
-share the colour-red edge $(0, 7)$ and satisfy
-$h_\varphi \equiv -1$ on the vertex set of each. Globally $h_\varphi$
-takes value $+1$ on $16$ vertices and $-1$ on $24$ vertices, with all
-of the $+1$-vertices concentrated in the inner ``tilted ladder''
-region, so that both Kempe cycles miss them entirely.
-
-\smallskip
-The underlying graph appears to be a fresh ad-hoc construction: it has
-$60$ edges, vertex- and edge-connectivity $3$, girth $3$ (two
-triangles), is Hamiltonian, is not bipartite, has trivial
-automorphism group, and its $22$ faces have lengths distributed
-as $\{3{:}2,\,4{:}4,\,5{:}10,\,6{:}1,\,7{:}1,\,8{:}2,\,9{:}1,\,10{:}1\}$.
-Its canonical \texttt{graph6} string (via
-\texttt{G.canonical\_label().graph6\_string()}) is
-\begin{center}
-\small\ttfamily
-ggE\_?C?O\_B?B?@C?P???B??\_?@???\_??Sa???W????@a??\_B????G\_???@?????O??@\_???@?\_???K?????\_????K?????o???B?????AG?????B?????G?????AG?????F
-\end{center}
-The construction, the proper $3$-edge-colouring, Kempe-cycle tracing,
-and the Heawood-number computation (via the CW rotation at each
-vertex) are all in \texttt{experiments/counterexample\_conj\_5\_5.py};
-the source drawing is in \texttt{constant\_heawood\_counterexample.tikz}.
+\begin{remark}[On the face-length hypothesis]
+\label{rem:no-two-constant-kempe-face-length-hypothesis}
+Without the hypothesis that every face has length $\ge 5$, the
+conjecture is \emph{false}, with very small counterexamples:
+\begin{itemize}
+\item \textbf{$K_4$ (the tetrahedron, $n = 4$):} The standard
+proper $3$-edge-colouring has $h_\varphi$ constant (all $-1$ or
+all $+1$, depending on planar embedding orientation) on every vertex,
+and every pair of distinct Kempe cycles shares colour-edges. (All
+four faces of $K_4$ are triangles.)
+\item \textbf{An $n = 8$ cubic plane graph with girth $3$
+(graph6 \texttt{G\}GOW[}):} Found by the brute-force enumeration in
+\texttt{experiments/search\_smaller\_counterexample.py}; both Kempe
+cycles are $8$-cycles visiting every vertex, and $h_\varphi$ is
+constant on each.
+\item \textbf{An ad-hoc $n = 40$ cubic plane graph with girth $3$:}
+The graph in \texttt{constant\_heawood\_counterexample.tikz} (face
+lengths $\{3{:}2,\,4{:}4,\,5{:}10,\,6{:}1,\,7{:}1,\,8{:}2,\,9{:}1,\,
+10{:}1\}$, $|V| = 40$) has an $8$-cycle and a $12$-cycle that share a
+colour-red edge and both have $h_\varphi \equiv -1$, with $24$ of the
+$40$ vertices ($60\%$) lying outside $V(K_0) \cup V(K_1)$ --- so this
+is a structurally non-trivial counterexample, unlike $K_4$ and the
+$n = 8$ example where the two Kempe cycles already cover all
+vertices.
+\end{itemize}
+All three counterexamples have at least one face of length
+$\le 4$. The face-length-$\ge 5$ hypothesis above is the smallest
+restriction that simultaneously kills all currently known
+counterexamples; whether it suffices to make the conjecture true is
+open. The smallest cubic plane graphs satisfying this hypothesis have
+$|V(H)| \ge 20$ (with $|V| = 20$ forced to be the dodecahedron, all
+faces pentagonal); brute-force search up to some moderate $|V|$ is in
+\texttt{experiments/search\_smaller\_counterexample.py}.
 \end{remark}
 
 \begin{figure}[h]
 \centering
-\includegraphics[width=0.85\textwidth]{figures/no-two-constant-kempe-counterexample.png}
-\caption{Counterexample to
-Conjecture~\ref{conj:no-two-constant-kempe-cycles}: a cubic plane
-graph on $40$ vertices with a proper $3$-edge-colouring on which
-$h_\varphi$ is simultaneously constant ($\equiv -1$) on the outer
-red/blue $8$-cycle and on the red/green $12$-cycle (outer frame plus
-the upper-left ladder side), which share the colour-red edge
-$(0, 7)$.}
+\includegraphics[width=0.7\textwidth]{figures/no-two-constant-kempe-counterexample.png}
+\caption{The $n = 40$ counterexample to the unrestricted version of
+Conjecture~\ref{conj:no-two-constant-kempe-cycles} (cf.\
+Remark~\ref{rem:no-two-constant-kempe-face-length-hypothesis}). Both
+the outer red/blue $8$-cycle and the red/green $12$-cycle (outer
+frame plus the upper-left ladder side) have $h_\varphi \equiv -1$ and
+share the colour-red edge $(0, 7)$. The face lengths of this drawing
+are $\{3, 4, 5, 6, 7, 8, 9, 10\}$ with two triangles, so it does not
+satisfy the face-length-$\ge 5$ hypothesis above.}
 \label{fig:no-two-constant-kempe-counterexample}
 \end{figure}