face_monochromatic_pairs: reframe Lemma 5.2 as a non-existence result

The previous statement "Heawood is constant on K through merged" was
strictly stronger than what the proof actually established without
Conjecture 5.3. Restate the lemma in the contrapositive direction:

  If h_phi is constant on V(K), then no edge e in E(K) admits a face
  F of G'^hat and edges e_1, e_2 on dF realising the clause-(3) arc
  of Conjecture 5.1 at the endpoints of e.

Proof structure is mostly preserved (same F_R/F_L geometry, same case
split on phi(e) in {a, b}, same reading-off of cyclic colour orders).
The hypothesis "h_phi(v_0) != h_phi(v_1)" becomes "h_phi(v_0) =
h_phi(v_1)", which flips the conclusion: the same-coloured non-e
edges at v_0, v_1 land on opposite faces of e instead of the same
face. No dependency on Conjecture 5.3 or Theorem 4.X.

Redraw the figure to match the new lemma: both vertices labelled
h_phi = +1, both showing CW order (a, b, c), and the same-colour pair
(b-edges in Case A, a-edges in Case B) drawn on opposite sides of e.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-24 22:31:10 -04:00
parent d99f8e23b3
commit 037d987c7d
6 changed files with 148 additions and 159 deletions
@@ -1,17 +1,17 @@
"""Two-panel illustration of the proof of Lemma 5.2
(Heawood constant on Kempe cycles through merged).
"""Two-panel illustration of the proof of Lemma 5.2 (a Heawood-constant
Kempe cycle does not admit the clause-(3) arc of Conjecture 5.1).
Each panel shows two consecutive vertices v_0, v_1 on the {a, b}-Kempe
cycle K, joined by an edge e, with h(v_0) = +1 (CW colour order (a, b, c))
and h(v_1) = -1 (CW colour order (a, c, b)).
cycle K, joined by an edge e, with h(v_0) = h(v_1) = +1: i.e., both
have the same clockwise colour order (a, b, c). The would-be witness
edges (b-edges in Case A, a-edges in Case B) lie on opposite sides of
e, so no face of the graph contains both of them.
Left panel (Case A): phi(e) = a. The two b-edges at v_0, v_1 both lie on
the same face F = F_R (right side of e); they form
the witness (e_1, e_2).
Left panel (Case A): phi(e) = a. The b-edges at v_0, v_1 are on
opposite sides of e (one south, one north).
Right panel (Case B): phi(e) = b. The two a-edges at v_0, v_1 both lie
on the same face F = F_L (left side of e); they
form the witness (e_1, e_2).
Right panel (Case B): phi(e) = b. The a-edges at v_0, v_1 are on
opposite sides of e.
Produces fig_lemma_kempe_heawood.png.
"""
@@ -25,12 +25,12 @@ OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
DARK = '#374151'
GRAY = '#9ca3af'
# Colour code matching earlier figures: a=red/orange, b=blue, c=green.
COL_A = '#ea580c' # 'a'
COL_B = '#2563eb' # 'b'
COL_C = '#16a34a' # 'c'
FACE_FILL = '#fef3c7'
FACE_FILL_R = '#fef3c7' # F_R shading (south)
FACE_FILL_L = '#dbeafe' # F_L shading (north)
V0 = (-1.6, 0.0)
V1 = ( 1.6, 0.0)
@@ -62,7 +62,7 @@ def label_text(ax, p, text, color=DARK, fontsize=12, dx=0, dy=0,
edgecolor='none', alpha=0.85))
def label_edge_midpoint(ax, p, q, text, color, fontsize=11, offset=(0, 0)):
def label_edge_midpoint(ax, p, q, text, color, fontsize=10, offset=(0, 0)):
mid = ((p[0] + q[0]) / 2 + offset[0],
(p[1] + q[1]) / 2 + offset[1])
ax.text(mid[0], mid[1], text, ha='center', va='center',
@@ -71,132 +71,122 @@ def label_edge_midpoint(ax, p, q, text, color, fontsize=11, offset=(0, 0)):
edgecolor='none', alpha=0.9))
def shade_face(ax, pts, color=FACE_FILL, alpha=0.7):
def shade_face(ax, pts, color, alpha=0.55):
poly = Polygon(pts, facecolor=color, edgecolor='none',
alpha=alpha, zorder=1)
ax.add_patch(poly)
def panel_case_A(ax):
# phi(e) = a. v_0 has CW order (a, b, c) starting from e at 0 deg:
# e (a) at 0 deg, b-edge at 300 deg (southeast), c-edge at 120 deg
# (northwest).
# v_1 has CW order (a, c, b) starting from e at 180 deg:
# e (a) at 180 deg, c-edge at 60 deg (northeast), b-edge at 240 deg
# (south-southwest).
e_color = COL_A
# Other endpoints (stubs) of the non-e edges.
b0 = edge_at(V0, -60) # b-edge at v_0, southeast
c0 = edge_at(V0, 120) # c-edge at v_0, northwest
c1 = edge_at(V1, 60) # c-edge at v_1, northeast
b1 = edge_at(V1, 240) # b-edge at v_1, southwest
# Same Heawood: v_0 and v_1 both have CW order (a, b, c) with e = a.
# v_0: e at 0 deg (east), b at 300 deg (south), c at 60 deg (north).
# v_1: e at 180 deg (west), b at 90 deg (north), c at 270 deg (south).
# The b-edges land on opposite sides of e (south of v_0, north of v_1).
b0 = edge_at(V0, 300) # south of v_0
c0 = edge_at(V0, 60) # north of v_0
b1 = edge_at(V1, 90) # north of v_1
c1 = edge_at(V1, 270) # south of v_1
# Shade F_R = south face: vertices roughly (b0, V0, V1, b1) plus a
# closing polygon below.
shade_face(ax, [V0, V1, b1, (b1[0] + 0.2, b1[1] - 0.6),
(b0[0] - 0.2, b0[1] - 0.6), b0])
label_text(ax, ((V0[0] + V1[0]) / 2, -1.6), 'face $F$', color=DARK,
fontsize=12, weight='bold')
# Shade both F_R (south) and F_L (north) lightly.
shade_face(ax, [V0, V1, c1, (c1[0] + 0.3, c1[1] - 0.6),
(b0[0] - 0.3, b0[1] - 0.6), b0], color=FACE_FILL_R)
shade_face(ax, [V0, c0, (c0[0] - 0.3, c0[1] + 0.6),
(b1[0] + 0.3, b1[1] + 0.6), b1, V1], color=FACE_FILL_L)
label_text(ax, ((V0[0] + V1[0]) / 2, -1.7), '$F_R$', color=DARK,
fontsize=11, weight='bold')
label_text(ax, ((V0[0] + V1[0]) / 2, 1.7), '$F_L$', color=DARK,
fontsize=11, weight='bold')
# Edges
draw_edge(ax, V0, V1, e_color) # e (color a)
draw_edge(ax, V0, b0, COL_B) # b-edge at v_0
draw_edge(ax, V0, c0, COL_C) # c-edge at v_0
draw_edge(ax, V1, c1, COL_C) # c-edge at v_1
draw_edge(ax, V1, b1, COL_B) # b-edge at v_1
draw_edge(ax, V0, V1, COL_A)
draw_edge(ax, V0, b0, COL_B)
draw_edge(ax, V0, c0, COL_C)
draw_edge(ax, V1, b1, COL_B)
draw_edge(ax, V1, c1, COL_C)
# Vertices
draw_vertex(ax, V0, DARK)
draw_vertex(ax, V1, DARK)
draw_vertex(ax, V0, DARK); draw_vertex(ax, V1, DARK)
draw_stub(ax, b0); draw_stub(ax, c0)
draw_stub(ax, c1); draw_stub(ax, b1)
draw_stub(ax, b1); draw_stub(ax, c1)
# Labels
label_text(ax, V0, '$v_0$', dy=0.28, fontsize=12)
label_text(ax, (V0[0] - 0.05, V0[1] - 0.28), '$h_\\varphi\\!=\\!+1$',
color=DARK, fontsize=9)
label_text(ax, V1, '$v_1$', dy=0.28, fontsize=12)
label_text(ax, (V1[0] + 0.05, V1[1] - 0.28), '$h_\\varphi\\!=\\!-1$',
label_text(ax, (V1[0] + 0.05, V1[1] - 0.28), '$h_\\varphi\\!=\\!+1$',
color=DARK, fontsize=9)
label_edge_midpoint(ax, V0, V1, '$e\\!=\\!a$', color=COL_A,
offset=(0, 0.16))
label_edge_midpoint(ax, V0, b0, '$e_1\\!=\\!b$', color=COL_B,
offset=(-0.05, 0.05))
offset=(0, 0.18))
label_edge_midpoint(ax, V0, b0, '$b$', color=COL_B,
offset=(-0.15, 0))
label_edge_midpoint(ax, V0, c0, '$c$', color=COL_C,
offset=(0.05, 0))
offset=(-0.15, 0))
label_edge_midpoint(ax, V1, b1, '$b$', color=COL_B,
offset=(0.15, 0))
label_edge_midpoint(ax, V1, c1, '$c$', color=COL_C,
offset=(-0.05, 0))
label_edge_midpoint(ax, V1, b1, '$e_2\\!=\\!b$', color=COL_B,
offset=(0.05, 0.05))
offset=(0.15, 0))
ax.set_title('Case A: $\\varphi(e) = a$. The two $b$-edges'
' at $v_0, v_1$ lie on $\\partial F$',
fontsize=11, color=DARK, pad=10, fontweight='bold')
ax.set_title('Case A: $\\varphi(e) = a$. The two $b$-edges are on\n'
'opposite sides of $e$ -- no common face',
fontsize=11, color=DARK, pad=8, fontweight='bold')
def panel_case_B(ax):
# phi(e) = b. v_0 has CW order (a, b, c) with b = e at 0 deg:
# a-edge at 60 deg (northeast), e (b) at 0 deg, c-edge at 300 deg
# (southeast).
# v_1 has CW order (a, c, b) with b = e at 180 deg:
# a-edge at 60 deg (northeast), c-edge at 300 deg (southeast), e
# (b) at 180 deg.
e_color = COL_B
a0 = edge_at(V0, 60) # a-edge at v_0, northeast
c0 = edge_at(V0, -60) # c-edge at v_0, southeast
a1 = edge_at(V1, 120) # a-edge at v_1, northwest
c1 = edge_at(V1, 240) # c-edge at v_1, southwest
# Same Heawood: v_0 and v_1 both have CW order (a, b, c) with e = b.
# v_0: a at 60 deg (north), e (b) at 0 deg (east), c at 300 deg (south).
# v_1: a at 270 deg (south), e (b) at 180 deg (west), c at 90 deg (north).
# The a-edges land on opposite sides of e (north of v_0, south of v_1).
a0 = edge_at(V0, 60) # north of v_0
c0 = edge_at(V0, 300) # south of v_0
a1 = edge_at(V1, 270) # south of v_1
c1 = edge_at(V1, 90) # north of v_1
# Shade F_L = north face: a0, V0, V1, a1, plus a closing polygon above.
shade_face(ax, [V0, a0, (a0[0] - 0.2, a0[1] + 0.6),
(a1[0] + 0.2, a1[1] + 0.6), a1, V1])
label_text(ax, ((V0[0] + V1[0]) / 2, 1.6), 'face $F$', color=DARK,
fontsize=12, weight='bold')
shade_face(ax, [V0, V1, a1, (a1[0] + 0.3, a1[1] - 0.6),
(c0[0] - 0.3, c0[1] - 0.6), c0], color=FACE_FILL_R)
shade_face(ax, [V0, a0, (a0[0] - 0.3, a0[1] + 0.6),
(c1[0] + 0.3, c1[1] + 0.6), c1, V1], color=FACE_FILL_L)
label_text(ax, ((V0[0] + V1[0]) / 2, -1.7), '$F_R$', color=DARK,
fontsize=11, weight='bold')
label_text(ax, ((V0[0] + V1[0]) / 2, 1.7), '$F_L$', color=DARK,
fontsize=11, weight='bold')
# Edges
draw_edge(ax, V0, V1, e_color)
draw_edge(ax, V0, V1, COL_B)
draw_edge(ax, V0, a0, COL_A)
draw_edge(ax, V0, c0, COL_C)
draw_edge(ax, V1, a1, COL_A)
draw_edge(ax, V1, c1, COL_C)
# Vertices
draw_vertex(ax, V0, DARK)
draw_vertex(ax, V1, DARK)
draw_vertex(ax, V0, DARK); draw_vertex(ax, V1, DARK)
draw_stub(ax, a0); draw_stub(ax, c0)
draw_stub(ax, a1); draw_stub(ax, c1)
# Labels
label_text(ax, V0, '$v_0$', dy=0.28, fontsize=12)
label_text(ax, (V0[0] - 0.05, V0[1] - 0.28), '$h_\\varphi\\!=\\!+1$',
color=DARK, fontsize=9)
label_text(ax, V1, '$v_1$', dy=0.28, fontsize=12)
label_text(ax, (V1[0] + 0.05, V1[1] - 0.28), '$h_\\varphi\\!=\\!-1$',
label_text(ax, (V1[0] + 0.05, V1[1] - 0.28), '$h_\\varphi\\!=\\!+1$',
color=DARK, fontsize=9)
label_edge_midpoint(ax, V0, V1, '$e\\!=\\!b$', color=COL_B,
offset=(0, -0.18))
label_edge_midpoint(ax, V0, a0, '$e_1\\!=\\!a$', color=COL_A,
offset=(-0.05, 0))
label_edge_midpoint(ax, V0, a0, '$a$', color=COL_A,
offset=(-0.15, 0))
label_edge_midpoint(ax, V0, c0, '$c$', color=COL_C,
offset=(0.05, 0))
label_edge_midpoint(ax, V1, a1, '$e_2\\!=\\!a$', color=COL_A,
offset=(0.05, 0))
offset=(-0.15, 0))
label_edge_midpoint(ax, V1, a1, '$a$', color=COL_A,
offset=(0.15, 0))
label_edge_midpoint(ax, V1, c1, '$c$', color=COL_C,
offset=(-0.05, 0))
offset=(0.15, 0))
ax.set_title('Case B: $\\varphi(e) = b$. The two $a$-edges'
' at $v_0, v_1$ lie on $\\partial F$',
fontsize=11, color=DARK, pad=10, fontweight='bold')
ax.set_title('Case B: $\\varphi(e) = b$. The two $a$-edges are on\n'
'opposite sides of $e$ -- no common face',
fontsize=11, color=DARK, pad=8, fontweight='bold')
def main():
plt.rcParams['text.usetex'] = False # keep matplotlib defaults
fig, axes = plt.subplots(1, 2, figsize=(13, 5.5))
fig, axes = plt.subplots(1, 2, figsize=(13, 5.8))
for ax in axes:
ax.set_xlim(-3.5, 3.5)
ax.set_ylim(-2.4, 2.4)
ax.set_ylim(-2.5, 2.5)
ax.set_aspect('equal')
ax.axis('off')
panel_case_A(axes[0])
Binary file not shown.

Before

Width:  |  Height:  |  Size: 70 KiB

After

Width:  |  Height:  |  Size: 62 KiB

+2 -2
View File
@@ -38,9 +38,9 @@
\newlabel{conj:face-monochromatic-pair-on-merged-kempe-cycle}{{5.1}{10}}
\newlabel{lem:kempe-heawood-constant}{{5.2}{11}}
\newlabel{rem:conj-3-6-empirical}{{5.3}{11}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces The two cases in the proof of Lemma\nonbreakingspace 5.2\hbox {}. Vertices $v_0, v_1$ are consecutive on the $\{a, b\}$-Kempe cycle $K$, joined by an edge $e$, with $h_\varphi (v_0) = +1$ (clockwise colour order $(a, b, c)$) and $h_\varphi (v_1) = -1$ (clockwise order $(a, c, b)$). \emph {Left (Case\nonbreakingspace A):} when $\varphi (e) = a$, the two $b$-edges at $v_0, v_1$ lie on the same face $F$, with $e$ as the unique $\partial F$-edge between them. \emph {Right (Case\nonbreakingspace B):} when $\varphi (e) = b$, the two $a$-edges at $v_0, v_1$ lie on the opposite face $F$ instead, again with $e$ between them on one arc. In either case $(F, e_1, e_2)$ witnesses clauses (1)--(3) of Conjecture\nonbreakingspace 5.1\hbox {}.}}{12}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces The two cases in the proof of Lemma\nonbreakingspace 5.2\hbox {}. Vertices $v_0, v_1$ are consecutive on the $\{a, b\}$-Kempe cycle $K$, joined by an edge $e$, with the lemma's hypothesis $h_\varphi (v_0) = h_\varphi (v_1) = +1$ --- so both vertices share the clockwise colour order $(a, b, c)$. \emph {Left (Case\nonbreakingspace A):} when $\varphi (e) = a$, the colour-$b$ edge at $v_0$ lies south of $e$ (on $\partial F_R$) and the colour-$b$ edge at $v_1$ lies north of $e$ (on $\partial F_L$); the two would-be witness edges are on opposite faces, so no face of $\setbox \z@ \hbox {\mathsurround \z@ $\textstyle G$}\mathaccent "0362{G}'_{v,i}$ contains both. \emph {Right (Case\nonbreakingspace B):} when $\varphi (e) = b$, the colour-$a$ edges at $v_0, v_1$ are likewise on opposite sides of $e$. In either case the clause-$(3)$ arc of Conjecture\nonbreakingspace 5.1\hbox {} cannot be realised at $e$.}}{12}{}\protected@file@percent }
\newlabel{fig:lemma-kempe-heawood}{{5}{12}}
\newlabel{conj:face-monochromatic-pair-strengthened}{{5.4}{13}}
\newlabel{conj:face-monochromatic-pair-strengthened}{{5.4}{12}}
\newlabel{rem:conj-3-8-empirical}{{5.5}{13}}
\newlabel{rem:implication-4ct}{{5.6}{13}}
\bibcite{Heawood1898}{1}
+9 -9
View File
@@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 21:49
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 22:13
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
@@ -262,23 +262,23 @@ Package pdftex.def Info: fig_thm_cubic_contraction_4face.png used on input lin
e 620.
(pdftex.def) Requested size: 352.79846pt x 160.78339pt.
[10 <./fig_thm_cubic_contraction_4face.png>]
<fig_lemma_kempe_heawood.png, id=72, 916.223pt x 335.654pt>
<fig_lemma_kempe_heawood.png, id=72, 916.223pt x 360.9485pt>
File: fig_lemma_kempe_heawood.png Graphic file (type png)
<use fig_lemma_kempe_heawood.png>
Package pdftex.def Info: fig_lemma_kempe_heawood.png used on input line 730.
(pdftex.def) Requested size: 352.79846pt x 129.2451pt.
Package pdftex.def Info: fig_lemma_kempe_heawood.png used on input line 727.
(pdftex.def) Requested size: 352.79846pt x 138.98488pt.
LaTeX Warning: `h' float specifier changed to `ht'.
[11] [12 <./fig_lemma_kempe_heawood.png>]
Underfull \hbox (badness 1648) in paragraph at lines 825--831
Underfull \hbox (badness 1648) in paragraph at lines 824--830
\OT1/cmr/m/it/10 Remark \OT1/cmr/m/n/10 5.5\OT1/cmr/m/it/10 . \OT1/cmr/m/n/10 T
he strength-ened con-jec-ture was tested on the same chord-
[]
Underfull \hbox (badness 1014) in paragraph at lines 825--831
Underfull \hbox (badness 1014) in paragraph at lines 824--830
\OT1/cmr/m/n/10 apex+Kempe colour-ings as Re-mark 5.3[]; for each colour-ing we
sought any
[]
@@ -287,11 +287,11 @@ Underfull \hbox (badness 1014) in paragraph at lines 825--831
Here is how much of TeX's memory you used:
3108 strings out of 478268
44593 string characters out of 5846347
348397 words of memory out of 5000000
349397 words of memory out of 5000000
21140 multiletter control sequences out of 15000+600000
478386 words of font info for 63 fonts, out of 8000000 for 9000
1302 hyphenation exceptions out of 8191
69i,12n,76p,875b,344s stack positions out of 10000i,1000n,20000p,200000b,200000s
69i,12n,76p,1047b,344s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2022/texmf-dist/fonts/type1/public
/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/
amsfonts/cm/cmbx8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
@@ -316,7 +316,7 @@ cal/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/loc
al/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/local
/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/local/
texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb>
Output written on paper.pdf (14 pages, 1081744 bytes).
Output written on paper.pdf (14 pages, 1077738 bytes).
PDF statistics:
192 PDF objects out of 1000 (max. 8388607)
106 compressed objects within 2 object streams
Binary file not shown.
+58 -59
View File
@@ -662,67 +662,64 @@ merged edge, such that:
\end{enumerate}
\end{conjecture}
\begin{lemma}[Heawood number is constant on the Kempe cycles through the merged edge]
\begin{lemma}[A Heawood-constant Kempe cycle does not admit the clause-(3) arc]
\label{lem:kempe-heawood-constant}
Let $G$ be a minimal counterexample to the Four Colour Theorem, fix a
reduced dual $\widehat{G}'_{v,i}$ of $G' = \mathrm{dual}(G)$, and let
$\varphi$ be a proper $3$-edge-colouring of $\widehat{G}'_{v,i}$. Set
$a := \varphi(\mathrm{merged})$. Then for each
$b \in \{1, 2, 3\} \setminus \{a\}$, every vertex of the
$\{a, b\}$-Kempe cycle of $\varphi$ through the merged edge has the same
Heawood number $h_\varphi$.
$a := \varphi(\mathrm{merged})$ and let $K$ be the $\{a, b\}$-Kempe
cycle of $\varphi$ through the merged edge for some
$b \in \{1, 2, 3\} \setminus \{a\}$. If $h_\varphi$ is constant on
$V(K)$, then no edge $e \in E(K)$ admits a face $F$ of
$\widehat{G}'_{v,i}$ and two non-incident edges
$e_1, e_2 \in \partial F$ such that
$\varphi(e_1) = \varphi(e_2)$ and $e$ is the unique edge of
$\partial F$ between $e_1$ and $e_2$ along one of the two arcs of
$\partial F$ --- that is, no edge of $K$ admits the clause-(3) arc of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
with $e_1, e_2$ at its two endpoints.
\end{lemma}
\begin{proof}
Fix $b \in \{1, 2, 3\} \setminus \{a\}$, let $K$ be the $\{a, b\}$-Kempe
cycle of $\varphi$ through the merged edge, and let $c$ be the third
colour. Suppose for contradiction that $h_\varphi$ is not constant on
$V(K)$. Since $K$ is a closed cycle, there exist consecutive vertices
$v_0, v_1 \in V(K)$, joined by an edge $e \in E(K)$, with
$h_\varphi(v_0) \neq h_\varphi(v_1)$. After possibly swapping
$v_0, v_1$, take $h_\varphi(v_0) = +1$ and $h_\varphi(v_1) = -1$. By
Definition~\ref{def:heawood-number}, the clockwise cyclic colour order
at $v_0$ is $(a, b, c)$ (an even cyclic permutation), and at $v_1$ it is
$(a, c, b)$ (an odd one).
Let $c$ be the third colour. Fix any edge $e \in E(K)$ joining
$v_0, v_1 \in V(K)$. By hypothesis $h_\varphi(v_0) = h_\varphi(v_1)$;
after possibly relabelling we may take
$h_\varphi(v_0) = h_\varphi(v_1) = +1$, so by
Definition~\ref{def:heawood-number} the clockwise cyclic colour order
at $v_0$ and at $v_1$ is the same even cyclic class $(a, b, c)$.
Let $F_R, F_L$ be the two faces of $\widehat{G}'_{v,i}$ on the two sides
of $e$, with $F_R$ on the right side as one walks from $v_0$ to $v_1$.
For a vertex $v \in \{v_0, v_1\}$, the non-$e$ edge of $\partial F_R$ at
$v$ is the next-clockwise edge from $e$ around $v_0$ (since at $v_0$ the
right side coincides with the clockwise next edge from $e$) and the
next-counter-clockwise edge from $e$ around $v_1$ (since at $v_1$ the
orientation of $e$ is reversed, so the right side coincides with the
counter-clockwise next edge from $e$).
Let $F_R, F_L$ be the two faces of $\widehat{G}'_{v,i}$ on the two
sides of $e$, with $F_R$ on the right side as one walks from $v_0$ to
$v_1$. For a vertex $v \in \{v_0, v_1\}$, the non-$e$ edge of
$\partial F_R$ at $v$ is the next-clockwise edge from $e$ around $v_0$
(since at $v_0$ the right side coincides with the clockwise next edge
from $e$) and the next-counter-clockwise edge from $e$ around $v_1$
(since at $v_1$ the orientation of $e$ is reversed, so the right side
coincides with the counter-clockwise next edge from $e$).
\emph{Case~A: $\varphi(e) = a$.} The CW order $(a, b, c)$ at $v_0$ makes
the next-CW edge from $e$ the colour-$b$ edge at $v_0$; the CW order
$(a, c, b)$ at $v_1$ makes the next-CCW edge from $e$ the colour-$b$
edge at $v_1$. Let $e_1, e_2$ be these colour-$b$ edges at $v_0$ and
$v_1$ respectively. Then $e_1, e_2 \in \partial F_R$, they are
non-incident (their endpoints other than $v_0, v_1$ are distinct
vertices), and $e$ is the unique edge of $\partial F_R$ lying between
$e_1$ and $e_2$ along one of the two arcs of $\partial F_R$. Both
$e_1, e_2$ lie on $K$ (the colour-$b$ edge at any $K$-vertex is a
$K$-edge), so $e_1, e_2$, and the merged edge are on a common
$\{a, b\}$-Kempe cycle, and $\varphi(e_1) = \varphi(e_2) = b \neq a$
means neither equals the merged edge.
\emph{Case~A: $\varphi(e) = a$.} In the CW order $(a, b, c)$ at $v_0$
the next-CW edge from $e$ has colour $b$; in the same CW order
$(a, b, c)$ at $v_1$ the next-CCW edge from $e$ has colour $c$ (since
CCW-next from $a$ in cyclic order $(a, b, c)$ is $c$). Hence the
non-$e$ edge of $\partial F_R$ at $v_0$ has colour $b$, while the
non-$e$ edge of $\partial F_R$ at $v_1$ has colour $c$ --- these
differ. Symmetrically, the non-$e$ edges of $\partial F_L$ at $v_0$
and $v_1$ have colours $c$ and $b$ respectively, again different.
Hence the colour-$b$ edges at $v_0$ and $v_1$ lie on opposite faces
of $e$, and the same for the colour-$c$ edges; no face of
$\widehat{G}'_{v,i}$ contains two same-coloured non-$e$ edges at
$\{v_0, v_1\}$.
\emph{Case~B: $\varphi(e) = b$.} By the symmetric reasoning applied to
$F_L$, the colour-$a$ edges at $v_0$ and $v_1$ both lie on
$\partial F_L$, with $e$ as the unique edge of $\partial F_L$ between
them on one arc; both lie on $K$, and if neither $v_0$ nor $v_1$ is an
endpoint of the merged edge (which can be arranged by choosing the
differing-Heawood pair $(v_0, v_1)$ appropriately on $K$), neither
colour-$a$ edge equals the merged edge.
\emph{Case~B: $\varphi(e) = b$.} By the analogous reasoning, the
non-$e$ edges of $\partial F_R$ at $v_0$ and $v_1$ have colours $c$
and $a$ respectively, and those of $\partial F_L$ have colours $a$
and $c$. The colour-$a$ edges at $v_0, v_1$ thus lie on opposite
faces of $e$, and so do the colour-$c$ edges.
Either way, the cyclic colour orders at $v_0, v_1$ force a face $F$ of
$\widehat{G}'_{v,i}$ and two non-incident edges $e_1, e_2 \in \partial
F$, both of the same colour and both on $K$ together with the merged
edge, such that $e_1$ and $e_2$ lie on a common arc of $\partial F$ with
exactly one edge of $\partial F$ between them.
The triple $(F, e_1, e_2)$ then satisfies clauses~(1)--(3) of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}.
In either case, no face $F$ of $\widehat{G}'_{v,i}$ has two same-coloured
non-$e$ edges at $\{v_0, v_1\}$ on $\partial F$, so the clause-(3) arc
(with $e$ as the unique $\partial F$-edge between $e_1$ and $e_2$ at the
endpoints of $e$) cannot be realised.
\end{proof}
\begin{figure}[h]
@@ -731,15 +728,17 @@ Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}.
\caption{The two cases in the proof of
Lemma~\ref{lem:kempe-heawood-constant}. Vertices $v_0, v_1$ are
consecutive on the $\{a, b\}$-Kempe cycle $K$, joined by an edge $e$,
with $h_\varphi(v_0) = +1$ (clockwise colour order $(a, b, c)$) and
$h_\varphi(v_1) = -1$ (clockwise order $(a, c, b)$). \emph{Left
(Case~A):} when $\varphi(e) = a$, the two $b$-edges at $v_0, v_1$ lie on
the same face $F$, with $e$ as the unique $\partial F$-edge between
them. \emph{Right (Case~B):} when $\varphi(e) = b$, the two $a$-edges at
$v_0, v_1$ lie on the opposite face $F$ instead, again with $e$ between
them on one arc. In either case $(F, e_1, e_2)$ witnesses clauses
(1)--(3) of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}.}
with the lemma's hypothesis $h_\varphi(v_0) = h_\varphi(v_1) = +1$ ---
so both vertices share the clockwise colour order $(a, b, c)$.
\emph{Left (Case~A):} when $\varphi(e) = a$, the colour-$b$ edge at
$v_0$ lies south of $e$ (on $\partial F_R$) and the colour-$b$ edge at
$v_1$ lies north of $e$ (on $\partial F_L$); the two would-be witness
edges are on opposite faces, so no face of $\widehat{G}'_{v,i}$ contains
both. \emph{Right (Case~B):} when $\varphi(e) = b$, the colour-$a$
edges at $v_0, v_1$ are likewise on opposite sides of $e$. In either
case the clause-$(3)$ arc of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
cannot be realised at $e$.}
\label{fig:lemma-kempe-heawood}
\end{figure}