didericis/math-research
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

dual_decomposition: abstract + intro, rename to "edge suppression", bib

Browse Source 
- Fill in the abstract and add a Section 1 introduction.
- Rename "cubic-graph edge contraction" -> "edge suppression" throughout
  (section, definition, theorem, captions, prose, labels). The PNG
  filenames keep their old paths and still resolve.
- Reframe edge suppression as a classical operation we recall, not a new
  concept we introduce; the face-monochromatic-pair conjecture (with its
  strengthening) is the sole contribution.
- Add a bibliography citing Appel-Haken Parts I and II, Robertson-Sanders-
  Seymour-Thomas, and Gonthier, and \cite them in the intro.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
didericis
2026-05-24 14:35:35 -04:00
parent b6f2ee8d6e
commit 2158c54117
4 changed files with 271 additions and 143 deletions
Download Patch File Download Diff File Expand all files Collapse all files
papers/dual_decomposition_minimal_counterexamples/paper.aux
+46 -30
View File
@@ -1,35 +1,51 @@
\relax \relax
\@writefile{toc}{\contentsline {section}{\tocsection {}{1}{The minimal counterexample}}{1}{}\protected@file@percent } \citation{AH77a}
\newlabel{lem:triangulate}{{1.1}{1}} \citation{AHK77}
\newlabel{def:minimal}{{1.2}{1}} \citation{RSST97}
\newlabel{lem:mindeg}{{1.4}{1}} \citation{Gonthier08}
\@writefile{toc}{\contentsline {section}{\tocsection {}{2}{The reduced dual}}{2}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\tocsection {}{1}{Introduction}}{1}{}\protected@file@percent }
\newlabel{def:reduced-dual}{{2.1}{2}} \newlabel{sec:intro}{{1}{1}}
\newlabel{def:edge-names}{{2.3}{2}} \@writefile{toc}{\contentsline {paragraph}{\tocparagraph {}{}{Organization.}}{2}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces The four steps of Definition\nonbreakingspace 2.1\hbox {}, illustrated on $G' = $ the dodecahedron (dual of the icosahedron) with $F_v$ the inner pentagon and $i = 0$. Top left: delete the five boundary vertices of $F_v$, leaving five degree-$2$ vertices on a new face $F$. Top right: order them clockwise as $A_0,\dots ,A_4$. Bottom left: add $v_n$ joined to $A_0, A_1, A_2$. Bottom right: add the chord $A_3 A_4$, giving the cubic plane graph $\setbox \z@ \hbox {\mathsurround \z@ $\textstyle G$}\mathaccent "0362{G}'_{v,0}$.}}{3}{}\protected@file@percent } \@writefile{toc}{\contentsline {paragraph}{\tocparagraph {}{}{Companion paper.}}{2}{}\protected@file@percent }
\newlabel{fig:reduced-dual-steps}{{1}{3}} \@writefile{toc}{\contentsline {section}{\tocsection {}{2}{The minimal counterexample}}{2}{}\protected@file@percent }
\newlabel{lem:pentagonal-externals}{{2.4}{3}} \newlabel{sec:minimal}{{2}{2}}
\newlabel{lem:chord-apex}{{2.6}{4}} \newlabel{lem:triangulate}{{2.1}{2}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces The proof of Lemma\nonbreakingspace 2.6\hbox {}, illustrated for $i = 0$ on $G' = $ the dodecahedron. Top: under the assumption $W \neq Y$, propriety at $v_n$ forces $W \in \{X, Z\}$. Bottom: in either case the lift to $G'$ has externals satisfying the hypothesis of Lemma\nonbreakingspace 2.4\hbox {}, which colours $\partial F_v$ to extend $\psi $ to a proper $3$-edge-colouring of $G'$.}}{5}{}\protected@file@percent } \newlabel{def:minimal}{{2.2}{2}}
\newlabel{fig:chord-apex-proof}{{2}{5}} \newlabel{lem:mindeg}{{2.4}{3}}
\newlabel{lem:kempe-spike}{{2.7}{6}} \@writefile{toc}{\contentsline {section}{\tocsection {}{3}{The reduced dual}}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{Cubic-graph edge contraction}}{7}{}\protected@file@percent } \newlabel{sec:reduced-dual}{{3}{3}}
\newlabel{def:cubic-edge-contraction}{{3.1}{7}} \newlabel{def:reduced-dual}{{3.1}{3}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Cubic-graph edge contraction (Definition\nonbreakingspace 3.1\hbox {}). Left: a fragment of a cubic plane graph with the contracted edge $e = uv$ highlighted in red. Middle: deleting $e$ leaves $u$ and $v$ of degree\nonbreakingspace $2$. Right: smoothing $u$ and $v$ replaces each pair of incident edges by a single new edge, removing $u, v$ and giving a cubic plane graph again.}}{7}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces The four steps of Definition\nonbreakingspace 3.1\hbox {}, illustrated on $G' = $ the dodecahedron (dual of the icosahedron) with $F_v$ the inner pentagon and $i = 0$. Top left: delete the five boundary vertices of $F_v$, leaving five degree-$2$ vertices on a new face $F$. Top right: order them clockwise as $A_0,\dots ,A_4$. Bottom left: add $v_n$ joined to $A_0, A_1, A_2$. Bottom right: add the chord $A_3 A_4$, giving the cubic plane graph $\setbox \z@ \hbox {\mathsurround \z@ $\textstyle G$}\mathaccent "0362{G}'_{v,0}$.}}{4}{}\protected@file@percent }
\newlabel{fig:cubic-edge-contraction}{{3}{7}} \newlabel{fig:reduced-dual-steps}{{1}{4}}
\newlabel{thm:cubic-contraction-4face}{{3.2}{7}} \newlabel{def:edge-names}{{3.3}{4}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{4}{The face-monochromatic-pair conjecture and the Four Colour Theorem}}{8}{}\protected@file@percent } \newlabel{lem:pentagonal-externals}{{3.4}{4}}
\newlabel{sec:toward-4ct}{{4}{8}} \newlabel{lem:chord-apex}{{3.6}{5}}
\newlabel{conj:face-monochromatic-pair-on-merged-kempe-cycle}{{4.1}{8}} \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces The proof of Lemma\nonbreakingspace 3.6\hbox {}, illustrated for $i = 0$ on $G' = $ the dodecahedron. Top: under the assumption $W \neq Y$, propriety at $v_n$ forces $W \in \{X, Z\}$. Bottom: in either case the lift to $G'$ has externals satisfying the hypothesis of Lemma\nonbreakingspace 3.4\hbox {}, which colours $\partial F_v$ to extend $\psi $ to a proper $3$-edge-colouring of $G'$.}}{6}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces The recolouring used in the proof of Theorem\nonbreakingspace 3.2\hbox {}. Left: the $4$-face $f$ of $H$ under $\varphi $, with the forced colours $\varphi (e_0) = a$, $\varphi (e_1) = b$, $\varphi (e_2) = \varphi (e_3) = c$, $\varphi (w_0) = \varphi (w_1) = b$, and $\varphi (w_2) = \varphi (w_3) = a$. Right: the contracted graph $H'$ under $\varphi '$. The smoothed-in edges $e_2', e_3'$ inherit the colour $b$ from $w_0, w_1$, and $e_1$ is recoloured from $b$ to $c$; every edge outside the face neighbourhood keeps its $\varphi $-colour (dotted in red: the five edges of $H$ removed by the contraction).}}{9}{}\protected@file@percent } \newlabel{fig:chord-apex-proof}{{2}{6}}
\newlabel{fig:thm-cubic-contraction-4face}{{4}{9}} \newlabel{lem:kempe-spike}{{3.7}{7}}
\newlabel{rem:conj-3-6-empirical}{{4.2}{9}} \@writefile{toc}{\contentsline {section}{\tocsection {}{4}{Edge suppression}}{8}{}\protected@file@percent }
\newlabel{conj:face-monochromatic-pair-strengthened}{{4.3}{10}} \newlabel{sec:edge-suppression}{{4}{8}}
\newlabel{rem:conj-3-8-empirical}{{4.4}{10}} \newlabel{def:edge-suppression}{{4.1}{8}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Edge suppression (Definition\nonbreakingspace 4.1\hbox {}). Left: a fragment of a cubic plane graph with the suppressed edge $e = uv$ highlighted in red. Middle: deleting $e$ leaves $u$ and $v$ of degree\nonbreakingspace $2$. Right: smoothing $u$ and $v$ replaces each pair of incident edges by a single new edge, removing $u, v$ and giving a cubic plane graph again.}}{8}{}\protected@file@percent }
\newlabel{fig:edge-suppression}{{3}{8}}
\newlabel{thm:edge-suppression-4face}{{4.2}{8}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{5}{The face-monochromatic-pair conjecture and the Four Colour Theorem}}{9}{}\protected@file@percent }
\newlabel{sec:toward-4ct}{{5}{9}}
\newlabel{conj:face-monochromatic-pair-on-merged-kempe-cycle}{{5.1}{9}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces The recolouring used in the proof of Theorem\nonbreakingspace 4.2\hbox {}. Left: the $4$-face $f$ of $H$ under $\varphi $, with the forced colours $\varphi (e_0) = a$, $\varphi (e_1) = b$, $\varphi (e_2) = \varphi (e_3) = c$, $\varphi (w_0) = \varphi (w_1) = b$, and $\varphi (w_2) = \varphi (w_3) = a$. Right: the suppressed graph $H'$ under $\varphi '$. The smoothed-in edges $e_2', e_3'$ inherit the colour $b$ from $w_0, w_1$, and $e_1$ is recoloured from $b$ to $c$; every edge outside the face neighbourhood keeps its $\varphi $-colour (dotted in red: the five edges of $H$ removed by the suppression).}}{10}{}\protected@file@percent }
\newlabel{fig:thm-edge-suppression-4face}{{4}{10}}
\newlabel{rem:conj-3-6-empirical}{{5.2}{10}}
\newlabel{conj:face-monochromatic-pair-strengthened}{{5.3}{11}}
\newlabel{rem:conj-3-8-empirical}{{5.4}{11}}
\bibcite{AH77a}{1}
\bibcite{AHK77}{2}
\bibcite{RSST97}{3}
\bibcite{Gonthier08}{4}
\newlabel{tocindent-1}{0pt} \newlabel{tocindent-1}{0pt}
\newlabel{tocindent0}{0pt} \newlabel{tocindent0}{12.7778pt}
\newlabel{tocindent1}{17.77782pt} \newlabel{tocindent1}{17.77782pt}
\newlabel{tocindent2}{0pt} \newlabel{tocindent2}{0pt}
\newlabel{tocindent3}{0pt} \newlabel{tocindent3}{0pt}
\newlabel{rem:implication-4ct}{{4.5}{11}} \newlabel{rem:implication-4ct}{{5.5}{12}}
\gdef \@abspage@last{11} \@writefile{toc}{\contentsline {section}{\tocsection {}{}{References}}{12}{}\protected@file@percent }
\gdef \@abspage@last{12}
papers/dual_decomposition_minimal_counterexamples/paper.log
+63 -56
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 14:15 This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 14:32
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
%&-line parsing enabled. %&-line parsing enabled.
@@ -192,121 +192,128 @@ File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv
e e
)) ))
[1{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] [1{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (41.917pt too wide) in paragraph at lines 145--147 [2]
Overfull \hbox (41.917pt too wide) in paragraph at lines 233--235
[]\OT1/cmr/m/n/10 List the five degree-$2$ ver-tices in clock-wise or-der aroun []\OT1/cmr/m/n/10 List the five degree-$2$ ver-tices in clock-wise or-der aroun
d $\OML/cmm/m/it/10 F$ \OT1/cmr/m/n/10 as $\OML/cmm/m/it/10 A \OT1/cmr/m/n/10 = d $\OML/cmm/m/it/10 F$ \OT1/cmr/m/n/10 as $\OML/cmm/m/it/10 A \OT1/cmr/m/n/10 =
(\OML/cmm/m/it/10 A[]; A[]; A[]; A[]; A[]\OT1/cmr/m/n/10 )$. (\OML/cmm/m/it/10 A[]; A[]; A[]; A[]; A[]\OT1/cmr/m/n/10 )$.
[] []
<fig_reduced_dual_step1.png, id=17, 517.79329pt x 499.08812pt> <fig_reduced_dual_step1.png, id=28, 517.79329pt x 499.08812pt>
File: fig_reduced_dual_step1.png Graphic file (type png) File: fig_reduced_dual_step1.png Graphic file (type png)
<use fig_reduced_dual_step1.png> <use fig_reduced_dual_step1.png>
Package pdftex.def Info: fig_reduced_dual_step1.png used on input line 165. Package pdftex.def Info: fig_reduced_dual_step1.png used on input line 253.
(pdftex.def) Requested size: 172.79846pt x 166.55775pt. (pdftex.def) Requested size: 172.79846pt x 166.55775pt.
<fig_reduced_dual_step2.png, id=19, 490.16064pt x 483.35876pt> <fig_reduced_dual_step2.png, id=30, 490.16064pt x 483.35876pt>
File: fig_reduced_dual_step2.png Graphic file (type png) File: fig_reduced_dual_step2.png Graphic file (type png)
<use fig_reduced_dual_step2.png> <use fig_reduced_dual_step2.png>
Package pdftex.def Info: fig_reduced_dual_step2.png used on input line 166. Package pdftex.def Info: fig_reduced_dual_step2.png used on input line 254.
(pdftex.def) Requested size: 172.79846pt x 170.39505pt. (pdftex.def) Requested size: 172.79846pt x 170.39505pt.
<fig_reduced_dual_step3.png, id=20, 490.16064pt x 483.35876pt> <fig_reduced_dual_step3.png, id=31, 490.16064pt x 483.35876pt>
File: fig_reduced_dual_step3.png Graphic file (type png) File: fig_reduced_dual_step3.png Graphic file (type png)
<use fig_reduced_dual_step3.png> <use fig_reduced_dual_step3.png>
Package pdftex.def Info: fig_reduced_dual_step3.png used on input line 167. Package pdftex.def Info: fig_reduced_dual_step3.png used on input line 255.
(pdftex.def) Requested size: 172.79846pt x 170.39505pt. (pdftex.def) Requested size: 172.79846pt x 170.39505pt.
<fig_reduced_dual_step4.png, id=21, 490.16064pt x 486.3346pt> <fig_reduced_dual_step4.png, id=32, 490.16064pt x 486.3346pt>
File: fig_reduced_dual_step4.png Graphic file (type png) File: fig_reduced_dual_step4.png Graphic file (type png)
<use fig_reduced_dual_step4.png> <use fig_reduced_dual_step4.png>
Package pdftex.def Info: fig_reduced_dual_step4.png used on input line 168. Package pdftex.def Info: fig_reduced_dual_step4.png used on input line 256.
(pdftex.def) Requested size: 172.79846pt x 171.44409pt. (pdftex.def) Requested size: 172.79846pt x 171.44409pt.
LaTeX Warning: `h' float specifier changed to `ht'. LaTeX Warning: `h' float specifier changed to `ht'.
[2] [3 <./fig_reduced_dual_step1.png> <./fig_reduced_dual_step2.png> <./fig_red [3] [4 <./fig_reduced_dual_step1.png> <./fig_reduced_dual_step2.png> <./fig_red
uced_dual_step3.png> <./fig_reduced_dual_step4.png>] uced_dual_step3.png> <./fig_reduced_dual_step4.png>]
<fig_chord_apex_step1.png, id=34, 505.03976pt x 502.06393pt> <fig_chord_apex_step1.png, id=43, 505.03976pt x 502.06393pt>
File: fig_chord_apex_step1.png Graphic file (type png) File: fig_chord_apex_step1.png Graphic file (type png)
<use fig_chord_apex_step1.png> <use fig_chord_apex_step1.png>
Package pdftex.def Info: fig_chord_apex_step1.png used on input line 289. Package pdftex.def Info: fig_chord_apex_step1.png used on input line 377.
(pdftex.def) Requested size: 251.9989pt x 250.5104pt. (pdftex.def) Requested size: 251.9989pt x 250.5104pt.
<fig_chord_apex_step2.png, id=35, 490.16064pt x 499.51323pt> <fig_chord_apex_step2.png, id=44, 490.16064pt x 499.51323pt>
File: fig_chord_apex_step2.png Graphic file (type png) File: fig_chord_apex_step2.png Graphic file (type png)
<use fig_chord_apex_step2.png> <use fig_chord_apex_step2.png>
Package pdftex.def Info: fig_chord_apex_step2.png used on input line 290. Package pdftex.def Info: fig_chord_apex_step2.png used on input line 378.
(pdftex.def) Requested size: 172.79846pt x 176.08986pt. (pdftex.def) Requested size: 172.79846pt x 176.08986pt.
<fig_chord_apex_step3.png, id=36, 490.16064pt x 499.51323pt> <fig_chord_apex_step3.png, id=45, 490.16064pt x 499.51323pt>
File: fig_chord_apex_step3.png Graphic file (type png) File: fig_chord_apex_step3.png Graphic file (type png)
<use fig_chord_apex_step3.png> <use fig_chord_apex_step3.png>
Package pdftex.def Info: fig_chord_apex_step3.png used on input line 291. Package pdftex.def Info: fig_chord_apex_step3.png used on input line 379.
(pdftex.def) Requested size: 172.79846pt x 176.08986pt. (pdftex.def) Requested size: 172.79846pt x 176.08986pt.
LaTeX Warning: `h' float specifier changed to `ht'. LaTeX Warning: `h' float specifier changed to `ht'.
[4] [5 <./fig_chord_apex_step1.png> <./fig_chord_apex_step2.png> <./fig_chord_a [5] [6 <./fig_chord_apex_step1.png> <./fig_chord_apex_step2.png> <./fig_chord_a
pex_step3.png>] [6] pex_step3.png>] [7]
<fig_cubic_edge_contraction.png, id=49, 950.752pt x 203.159pt> <fig_cubic_edge_contraction.png, id=59, 950.752pt x 203.159pt>
File: fig_cubic_edge_contraction.png Graphic file (type png) File: fig_cubic_edge_contraction.png Graphic file (type png)
<use fig_cubic_edge_contraction.png> <use fig_cubic_edge_contraction.png>
Package pdftex.def Info: fig_cubic_edge_contraction.png used on input line 432 Package pdftex.def Info: fig_cubic_edge_contraction.png used on input line 522
. .
(pdftex.def) Requested size: 341.9989pt x 73.08138pt. (pdftex.def) Requested size: 341.9989pt x 73.08138pt.
[7 <./fig_cubic_edge_contraction.png>] [8 <./fig_cubic_edge_contraction.png>]
<fig_thm_cubic_contraction_4face.png, id=55, 916.223pt x 417.56pt> <fig_thm_cubic_contraction_4face.png, id=64, 916.223pt x 417.56pt>
File: fig_thm_cubic_contraction_4face.png Graphic file (type png) File: fig_thm_cubic_contraction_4face.png Graphic file (type png)
<use fig_thm_cubic_contraction_4face.png> <use fig_thm_cubic_contraction_4face.png>
Package pdftex.def Info: fig_thm_cubic_contraction_4face.png used on input lin Package pdftex.def Info: fig_thm_cubic_contraction_4face.png used on input lin
e 507. e 597.
(pdftex.def) Requested size: 352.79846pt x 160.78339pt. (pdftex.def) Requested size: 352.79846pt x 160.78339pt.
LaTeX Warning: `h' float specifier changed to `ht'. LaTeX Warning: `h' float specifier changed to `ht'.
[8] [9]
Underfull \vbox (badness 10000) has occurred while \output is active [] Underfull \vbox (badness 10000) has occurred while \output is active []
[9 <./fig_thm_cubic_contraction_4face.png>] [10 <./fig_thm_cubic_contraction_4face.png>]
Underfull \hbox (badness 1648) in paragraph at lines 638--644 Underfull \hbox (badness 1648) in paragraph at lines 721--727
\OT1/cmr/m/it/10 Remark \OT1/cmr/m/n/10 4.4\OT1/cmr/m/it/10 . \OT1/cmr/m/n/10 T \OT1/cmr/m/it/10 Remark \OT1/cmr/m/n/10 5.4\OT1/cmr/m/it/10 . \OT1/cmr/m/n/10 T
he strength-ened con-jec-ture was tested on the same chord- he strength-ened con-jec-ture was tested on the same chord-
[] []
Underfull \hbox (badness 1014) in paragraph at lines 638--644 Underfull \hbox (badness 1014) in paragraph at lines 721--727
\OT1/cmr/m/n/10 apex+Kempe colour-ings as Re-mark 4.2[]; for each colour-ing we \OT1/cmr/m/n/10 apex+Kempe colour-ings as Re-mark 5.2[]; for each colour-ing we
sought any sought any
[] []
[10] [11] (./paper.aux) ) [11] [12] (./paper.aux) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
3087 strings out of 478268 3097 strings out of 478268
44184 string characters out of 5846347 44287 string characters out of 5846347
350310 words of memory out of 5000000 350362 words of memory out of 5000000
21121 multiletter control sequences out of 15000+600000 21130 multiletter control sequences out of 15000+600000
478077 words of font info for 62 fonts, out of 8000000 for 9000 478386 words of font info for 63 fonts, out of 8000000 for 9000
1302 hyphenation exceptions out of 8191 1302 hyphenation exceptions out of 8191
69i,9n,76p,744b,373s stack positions out of 10000i,1000n,20000p,200000b,200000s 69i,9n,76p,745b,389s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2022/texmf-dist/fonts/type1/public </usr/local/texlive/2022/texmf-dist/fonts/type1/public
/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ /amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/
amsfonts/cm/cmcsc10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ amsfonts/cm/cmbx8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
amsfonts/cm/cmex10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/a sfonts/cm/cmcsc10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
msfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am sfonts/cm/cmex10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ams
sfonts/cm/cmmi7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf fonts/cmextra/cmex8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/
onts/cm/cmmi9.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfon amsfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/a
ts/cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts msfonts/cm/cmmi6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ams
/cm/cmr7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm fonts/cm/cmmi7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfo
/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cm nts/cm/cmmi8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfont
r9.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy1 s/cm/cmmi9.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/
0.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7. cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm
pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pf /cmr6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cm
b></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb r7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.
></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb>< pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pfb
/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></ ></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb>
usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pf </usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy6.pfb></
b> usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></us
Output written on paper.pdf (11 pages, 941265 bytes). r/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/
local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/lo
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 (12 pages, 1015233 bytes).
PDF statistics: PDF statistics:
144 PDF objects out of 1000 (max. 8388607) 183 PDF objects out of 1000 (max. 8388607)
78 compressed objects within 1 object stream 101 compressed objects within 2 object streams
0 named destinations out of 1000 (max. 500000) 0 named destinations out of 1000 (max. 500000)
46 words of extra memory for PDF output out of 10000 (max. 10000000) 46 words of extra memory for PDF output out of 10000 (max. 10000000)
papers/dual_decomposition_minimal_counterexamples/paper.pdf
BIN
View File
Binary file not shown.
papers/dual_decomposition_minimal_counterexamples/paper.tex
+162 -57
View File
@@ -45,12 +45,99 @@ graph, edge connectivity, cyclic edge cut, Tait colouring, $3$-edge-colouring}
\dedicatory{} \dedicatory{}
\begin{abstract} \begin{abstract}
% TODO: abstract. We propose the \emph{face-monochromatic-pair conjecture}, a structural
property of proper $3$-edge-colourings of cubic plane graphs that, if
true, implies the Four Colour Theorem. Working in the planar dual $G'$ of
a hypothetical minimal counterexample $G$ to 4CT, we delete a single
pentagonal face of $G'$ and rewire its five external vertices around a
new apex vertex and a chord; the resulting \emph{reduced dual}
$\widehat{G}'_{v,i}$ is a smaller cubic plane graph whose proper
$3$-edge-colourings, by the minimality of $G$, are constrained by a
chord-apex condition and a pair of Kempe-cycle conditions. The
face-monochromatic-pair conjecture, in its strengthened form, asserts the
existence in every such colouring of a face $F$ and two non-incident
same-coloured edges $e_1, e_2 \in \partial F$ whose subdivision-and-%
bridging produces a $4$-face $f_n$ whose boundary colouring places it
under the hypothesis of a $4$-face edge-suppression theorem; we use this
theorem to derive a proper $3$-edge-colouring of $G'$, contradicting
minimality. We verify the conjecture computationally on all
chord-apex+Kempe colourings of reduced duals with $|V(G)| \leq 20$
($142{,}812$ colourings, all pass); the weaker form is verified up to
$|V(G)| \leq 21$ ($535{,}182$ colourings, all pass).
\end{abstract} \end{abstract}
\maketitle \maketitle
\section{Introduction}
\label{sec:intro}
The Four Colour Theorem (4CT) --- that every loopless plane graph admits a
proper $4$-vertex-colouring --- has, since the late 1970s, only been proved
by computer-assisted case analysis on a discharging argument over a finite
set of unavoidable reducible configurations. Appel and Haken's original
proof~\cite{AH77a, AHK77}, the Robertson--Sanders--Seymour--Thomas
reworking~\cite{RSST97}, and Gonthier's machine-checked
version~\cite{Gonthier08} all share that structure.
This paper takes a different approach: rather than discharge over
configurations in the triangulation $G$, we work in its planar dual $G'$,
a cubic plane graph whose proper $3$-edge-colourings correspond by Tait's
theorem to proper $4$-vertex-colourings of $G$. Assuming $G$ is a minimal
counterexample to 4CT, we delete a single pentagonal face of $G'$ and
rewire its five external vertices, obtaining a smaller cubic plane graph
$\widehat{G}'_{v,i}$ --- the \emph{reduced dual} --- which by minimality
\emph{is} properly $3$-edge-colourable. Two structural lemmas constrain
every such colouring: a \emph{chord-apex} condition (Lemma~\ref{lem:chord-apex})
forcing two named edges to share a colour, and a pair of
\emph{Kempe-cycle} conditions (Lemma~\ref{lem:kempe-spike}) placing four
of the rewired edges on common bichromatic Kempe cycles. These constraints
are the starting point of the present development.
The main contribution of the paper is the
\emph{face-monochromatic-pair conjecture}
(Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}) and
its strengthening
(Conjecture~\ref{conj:face-monochromatic-pair-strengthened}), which we
show together imply the Four Colour Theorem. The supporting ingredients
are the chord-apex and Kempe-cycle lemmas on reduced-dual colourings, the
classical operation of \emph{edge suppression} (delete the edge and smooth
its two degree-$2$ endpoints; equivalently, simple-graph contraction in
the dual triangulation; recalled in Section~\ref{sec:edge-suppression}),
and an observation that suppression preserves $3$-edge-colourability when
applied across a $4$-face whose two opposite boundary edges carry
different colours (Theorem~\ref{thm:edge-suppression-4face}).
The strategy is to construct, from a putative minimal counterexample's
reduced-dual colouring, a $4$-face $f_n$ in a slightly modified graph
$\widehat{G}'^{+}$ to which the suppression theorem applies; the
suppression then produces a properly $3$-edge-coloured graph from which a
$3$-edge-colouring of $G'$ can be recovered, contradicting the
non-$4$-colourability of $G$. The face-monochromatic-pair conjecture
asserts the existence of the structural data ($F, e_1, e_2$) needed to
build $f_n$; the strengthening guarantees that $f_n$'s boundary colouring
falls under the suppression theorem's hypothesis. Both conjectures have
been verified computationally on all chord-apex+Kempe colourings of
reduced duals up to $|V(G)| \leq 20$, with the weaker form going up to
$|V(G)| \leq 21$.
\paragraph{Organization.} Section~\ref{sec:minimal} fixes the
minimal-counterexample framework: $G$ is a triangulation,
$\delta(G) \geq 5$, and every triangulation on fewer vertices is properly
$4$-colourable. Section~\ref{sec:reduced-dual} introduces the reduced dual
$\widehat{G}'_{v,i}$ and proves the chord-apex and Kempe-cycle lemmas.
Section~\ref{sec:edge-suppression} defines edge suppression and proves
its $4$-face $3$-edge-colourability theorem.
Section~\ref{sec:toward-4ct} states the two conjectures, reports the
empirical verification, and gives the implication to 4CT.
\paragraph{Companion paper.} An iterated version of the reduced-dual
construction --- producing a sequence $H_1, H_2, \dots$ of progressively
smaller cubic plane graphs and tracking an accumulating ``protected'' edge
set --- is the subject of a companion paper. The present paper does not
use that iteration.
\section{The minimal counterexample} \section{The minimal counterexample}
\label{sec:minimal}
Throughout, a \emph{triangulation} is a simple plane graph, with a fixed Throughout, a \emph{triangulation} is a simple plane graph, with a fixed
embedding, in which every face --- including the outer face --- is bounded by a embedding, in which every face --- including the outer face --- is bounded by a
@@ -118,6 +205,7 @@ Hence $\delta(G) \ge 5$.
\end{proof} \end{proof}
\section{The reduced dual} \section{The reduced dual}
\label{sec:reduced-dual}
Write $G'$ for the dual of $G$: since $G$ is a triangulation, $G'$ is a cubic Write $G'$ for the dual of $G$: since $G$ is a triangulation, $G'$ is a cubic
plane graph in which each vertex of $G$ corresponds to a face of $G'$, each face plane graph in which each vertex of $G$ corresponds to a face of $G'$, each face
@@ -393,61 +481,63 @@ distinct colours, contradicting Lemma~\ref{lem:chord-apex} applied to
$\varphi'$. $\varphi'$.
\end{proof} \end{proof}
\section{Cubic-graph edge contraction} \section{Edge suppression}
\label{sec:edge-suppression}
We introduce a cubic-preserving analogue of edge contraction which turns We recall the classical operation of \emph{edge suppression} on cubic
out --- under planar duality --- to coincide with simple-graph contraction plane graphs: delete the edge and smooth the two resulting degree-$2$
on the dual side. It will be the central tool in endpoints. Under planar duality this coincides with simple-graph
contraction on the dual side. It will be the central tool in
Section~\ref{sec:toward-4ct} below, where we formulate a sufficient Section~\ref{sec:toward-4ct} below, where we formulate a sufficient
condition for the Four Colour Theorem. condition for the Four Colour Theorem.
\begin{definition}[Cubic-graph edge contraction] \begin{definition}[Edge suppression]
\label{def:cubic-edge-contraction} \label{def:edge-suppression}
Let $H$ be a cubic plane graph and $e = uv$ an edge of $H$ with $u \neq v$ and Let $H$ be a cubic plane graph and $e = uv$ an edge of $H$ with $u \neq v$
no edge of $H$ parallel to $e$. The \emph{cubic-graph edge contraction} of $H$ and no edge of $H$ parallel to $e$. The \emph{edge suppression} of $H$ at
along $e$ is the graph $H'$ obtained in two steps: $e$ is the graph $H'$ obtained in two steps:
\begin{enumerate} \begin{enumerate}
\item \emph{Delete} the edge $e$; the endpoints $u$ and $v$ each drop to \item \emph{Delete} the edge $e$; the endpoints $u$ and $v$ each drop to
degree $2$. degree $2$.
\item \emph{Smooth} each of $u$ and $v$: at $u$, replace $u$ and its two \item \emph{Smooth} each of $u$ and $v$: at $u$, replace $u$ and its two
remaining incident edges $ua, ub$ by a single new edge $ab$; do the remaining incident edges $ua, ub$ by a single new edge $ab$; do
same at $v$. Both vertices $u$ and $v$ are removed, and two new edges the same at $v$. Both vertices $u$ and $v$ are removed, and two
are added in their place. new edges are added in their place.
\end{enumerate} \end{enumerate}
Provided the smoothings do not introduce a loop or parallel edge, $H'$ is Provided the smoothings do not introduce a loop or parallel edge, $H'$ is
again a cubic plane graph, with $|V(H')| = |V(H)| - 2$ and again a cubic plane graph, with $|V(H')| = |V(H)| - 2$ and
$|E(H')| = |E(H)| - 3$. $|E(H')| = |E(H)| - 3$.
Equivalently, $H'$ is the planar dual of $\mathrm{dual}(H) / e^{*}$, where Equivalently, $H'$ is the planar dual of $\mathrm{dual}(H) / e^{*}$,
$e^{*}$ is the edge of $\mathrm{dual}(H)$ crossing $e$ and the contraction where $e^{*}$ is the edge of $\mathrm{dual}(H)$ crossing $e$ and the
on the right-hand side is simple-graph contraction (loops removed, parallel contraction on the right-hand side is simple-graph contraction (loops
edges absorbed). Under planar duality, contracting $e^{*}$ in removed, parallel edges absorbed). Under planar duality, contracting
$\mathrm{dual}(H)$ merges the two triangular faces of $\mathrm{dual}(H)$ $e^{*}$ in $\mathrm{dual}(H)$ merges the two triangular faces of
incident to $e^{*}$, and the parallel-edge cleanup corresponds exactly to $\mathrm{dual}(H)$ incident to $e^{*}$, and the parallel-edge cleanup
the smoothing step on the primal side. corresponds exactly to the smoothing step on the primal side.
\end{definition} \end{definition}
\begin{figure}[h] \begin{figure}[h]
\centering \centering
\includegraphics[width=0.95\textwidth]{fig_cubic_edge_contraction.png} \includegraphics[width=0.95\textwidth]{fig_cubic_edge_contraction.png}
\caption{Cubic-graph edge contraction \caption{Edge suppression
(Definition~\ref{def:cubic-edge-contraction}). Left: a fragment of a cubic (Definition~\ref{def:edge-suppression}). Left: a fragment of a cubic
plane graph with the contracted edge $e = uv$ highlighted in red. Middle: plane graph with the suppressed edge $e = uv$ highlighted in red. Middle:
deleting $e$ leaves $u$ and $v$ of degree~$2$. Right: smoothing $u$ and $v$ deleting $e$ leaves $u$ and $v$ of degree~$2$. Right: smoothing $u$ and
replaces each pair of incident edges by a single new edge, removing $u, v$ $v$ replaces each pair of incident edges by a single new edge, removing
and giving a cubic plane graph again.} $u, v$ and giving a cubic plane graph again.}
\label{fig:cubic-edge-contraction} \label{fig:edge-suppression}
\end{figure} \end{figure}
\begin{theorem}[Cubic contraction across a 4-face preserves 3-edge-colourability] \begin{theorem}[Edge suppression across a 4-face preserves 3-edge-colourability]
\label{thm:cubic-contraction-4face} \label{thm:edge-suppression-4face}
Let $H$ be a cubic plane graph with a proper $3$-edge-colouring $\varphi$, Let $H$ be a cubic plane graph with a proper $3$-edge-colouring $\varphi$,
let $f$ be a face of $H$ with $|\partial f| = 4$, and let $e_0, e_1$ be the let $f$ be a face of $H$ with $|\partial f| = 4$, and let $e_0, e_1$ be
two edges of $\partial f$ sharing no endpoint (the opposite pair on the the two edges of $\partial f$ sharing no endpoint (the opposite pair on
$4$-cycle $\partial f$). If $\varphi(e_0) \neq \varphi(e_1)$ and the the $4$-cycle $\partial f$). If $\varphi(e_0) \neq \varphi(e_1)$ and the
cubic-graph edge contraction of $H$ along $e_0$ edge suppression of $H$ at $e_0$
(Definition~\ref{def:cubic-edge-contraction}) is well-defined (no loops or (Definition~\ref{def:edge-suppression}) is well-defined (no loops or
parallel edges are created), then the contracted graph admits a proper parallel edges are created), then the suppressed graph admits a proper
$3$-edge-colouring. $3$-edge-colouring.
\end{theorem} \end{theorem}
@@ -466,8 +556,8 @@ $\varphi(w_1) = b$ and $\varphi(w_2) = a$. Symmetrically $\varphi(e_3) = c$,
$\varphi(w_0) = b$, and $\varphi(w_3) = a$. In particular $\varphi(w_0) = b$, and $\varphi(w_3) = a$. In particular
$\varphi(w_0) = \varphi(w_1) = b$. $\varphi(w_0) = \varphi(w_1) = b$.
\emph{Construction of $\varphi'$.} Let $H'$ denote the cubic-graph edge \emph{Construction of $\varphi'$.} Let $H'$ denote the edge suppression
contraction of $H$ along $e_0$; its new edges are $e_3' := v_3 u_0$ of $H$ at $e_0$; its new edges are $e_3' := v_3 u_0$
(replacing $e_3$ and $w_0$ via the smoothing at $v_0$) and (replacing $e_3$ and $w_0$ via the smoothing at $v_0$) and
$e_2' := v_2 u_1$ (replacing $e_2$ and $w_1$ via the smoothing at $v_1$). $e_2' := v_2 u_1$ (replacing $e_2$ and $w_1$ via the smoothing at $v_1$).
Define $\varphi' \colon E(H') \to \{1, 2, 3\}$ by Define $\varphi' \colon E(H') \to \{1, 2, 3\}$ by
@@ -506,16 +596,16 @@ $\varphi'$ is proper.
\centering \centering
\includegraphics[width=0.98\textwidth]{fig_thm_cubic_contraction_4face.png} \includegraphics[width=0.98\textwidth]{fig_thm_cubic_contraction_4face.png}
\caption{The recolouring used in the proof of \caption{The recolouring used in the proof of
Theorem~\ref{thm:cubic-contraction-4face}. Left: the $4$-face $f$ of $H$ Theorem~\ref{thm:edge-suppression-4face}. Left: the $4$-face $f$ of $H$
under $\varphi$, with the forced colours $\varphi(e_0) = a$, under $\varphi$, with the forced colours $\varphi(e_0) = a$,
$\varphi(e_1) = b$, $\varphi(e_2) = \varphi(e_3) = c$, $\varphi(e_1) = b$, $\varphi(e_2) = \varphi(e_3) = c$,
$\varphi(w_0) = \varphi(w_1) = b$, and $\varphi(w_2) = \varphi(w_3) = a$. $\varphi(w_0) = \varphi(w_1) = b$, and $\varphi(w_2) = \varphi(w_3) = a$.
Right: the contracted graph $H'$ under $\varphi'$. The smoothed-in edges Right: the suppressed graph $H'$ under $\varphi'$. The smoothed-in edges
$e_2', e_3'$ inherit the colour $b$ from $w_0, w_1$, and $e_1$ is $e_2', e_3'$ inherit the colour $b$ from $w_0, w_1$, and $e_1$ is
recoloured from $b$ to $c$; every edge outside the face neighbourhood recoloured from $b$ to $c$; every edge outside the face neighbourhood
keeps its $\varphi$-colour (dotted in red: the five edges of $H$ removed keeps its $\varphi$-colour (dotted in red: the five edges of $H$ removed
by the contraction).} by the suppression).}
\label{fig:thm-cubic-contraction-4face} \label{fig:thm-edge-suppression-4face}
\end{figure} \end{figure}
\section{The face-monochromatic-pair conjecture and the Four Colour Theorem} \section{The face-monochromatic-pair conjecture and the Four Colour Theorem}
@@ -524,14 +614,7 @@ by the contraction).}
The following conjecture identifies a structural property of every proper The following conjecture identifies a structural property of every proper
$3$-edge-colouring of a reduced dual of a minimal counterexample. If true, $3$-edge-colouring of a reduced dual of a minimal counterexample. If true,
it implies the Four Colour Theorem via it implies the Four Colour Theorem via
Theorem~\ref{thm:cubic-contraction-4face}. Theorem~\ref{thm:edge-suppression-4face}.
The reduced-dual construction of Definition~\ref{def:reduced-dual} can also
be applied \emph{iteratively}, producing a sequence $H_1, H_2, \dots$ of
progressively smaller cubic plane graphs and tracking an accumulating set
of ``protected'' edges; that iterated reduction, with its termination
analysis and structural lemmas about spike/merged pairs at each stage, is
the subject of a companion paper and is not used below.
\begin{conjecture}[Face-monochromatic-pair conjecture] \begin{conjecture}[Face-monochromatic-pair conjecture]
\label{conj:face-monochromatic-pair-on-merged-kempe-cycle} \label{conj:face-monochromatic-pair-on-merged-kempe-cycle}
@@ -601,7 +684,7 @@ has no content there.
The following strengthening adds a fourth clause that arranges the new The following strengthening adds a fourth clause that arranges the new
$4$-face $f_n$ to satisfy the hypotheses of $4$-face $f_n$ to satisfy the hypotheses of
Theorem~\ref{thm:cubic-contraction-4face}. Theorem~\ref{thm:edge-suppression-4face}.
\begin{conjecture}[Strengthening of \begin{conjecture}[Strengthening of
Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}] Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}]
@@ -674,11 +757,11 @@ carry distinct $\varphi'$-colours, the cyclic colour pattern on
$\partial f_n$ must be $(c, a, c, b)$ up to rotation and relabelling, with $\partial f_n$ must be $(c, a, c, b)$ up to rotation and relabelling, with
the two $c$-edges opposite and the two remaining opposite edges carrying the two $c$-edges opposite and the two remaining opposite edges carrying
the distinct colours $a$ and $b$. Those two opposite edges therefore the distinct colours $a$ and $b$. Those two opposite edges therefore
satisfy the hypothesis of Theorem~\ref{thm:cubic-contraction-4face}: they satisfy the hypothesis of Theorem~\ref{thm:edge-suppression-4face}: they
lie on the $4$-face $f_n$, share no endpoint, and have different lie on the $4$-face $f_n$, share no endpoint, and have different
$\varphi'$-colours. Theorem~\ref{thm:cubic-contraction-4face} then produces $\varphi'$-colours. Theorem~\ref{thm:edge-suppression-4face} then produces
a proper $3$-edge-colouring of the cubic-graph edge contraction a proper $3$-edge-colouring of the edge suppression of
$\widehat{G}'^{+} \!\setminus\! e$ along the $a$-coloured one. $\widehat{G}'^{+}$ at the $a$-coloured one.
Case~(ii) of clause~(4) is conjecturally reducible to case~(i) by a single Case~(ii) of clause~(4) is conjecturally reducible to case~(i) by a single
Kempe swap on the $\{b, c\}$-cycle through $X_1 X_2$: by hypothesis that Kempe swap on the $\{b, c\}$-cycle through $X_1 X_2$: by hypothesis that
@@ -688,9 +771,9 @@ $\partial f_n$ unchanged --- placing $\partial f_n$ into the three-colour
pattern of case~(i). pattern of case~(i).
\smallskip\noindent\emph{Consequence.} \smallskip\noindent\emph{Consequence.}
Theorem~\ref{thm:cubic-contraction-4face} now produces a proper Theorem~\ref{thm:edge-suppression-4face} now produces a proper
$3$-edge-colouring of the cubic-graph edge contraction of $3$-edge-colouring of the edge suppression of $\widehat{G}'^{+}$ at the
$\widehat{G}'^{+}$ along the chosen edge of $f_n$. Combined with the chosen edge of $f_n$. Combined with the
chord-apex and Kempe-cycle structure of $\widehat{G}'_{v,i}$ chord-apex and Kempe-cycle structure of $\widehat{G}'_{v,i}$
(Lemmas~\ref{lem:chord-apex} and~\ref{lem:kempe-spike}), this yields a (Lemmas~\ref{lem:chord-apex} and~\ref{lem:kempe-spike}), this yields a
proper $3$-edge-colouring of $G'$, and by Tait's correspondence a proper proper $3$-edge-colouring of $G'$, and by Tait's correspondence a proper
@@ -700,4 +783,26 @@ Conjecture~\ref{conj:face-monochromatic-pair-strengthened} implies the
Four Colour Theorem. Four Colour Theorem.
\end{remark} \end{remark}
\begin{thebibliography}{9}
\bibitem{AH77a}
K.~Appel and W.~Haken,
\emph{Every planar map is four colorable. Part~I: Discharging},
Illinois J.~Math. \textbf{21} (1977), 429--490.
\bibitem{AHK77}
K.~Appel, W.~Haken, and J.~Koch,
\emph{Every planar map is four colorable. Part~II: Reducibility},
Illinois J.~Math. \textbf{21} (1977), 491--567.
\bibitem{RSST97}
N.~Robertson, D.~P.~Sanders, P.~Seymour, and R.~Thomas,
\emph{The four-colour theorem},
J.~Combin. Theory Ser.~B \textbf{70} (1997), 2--44.
\bibitem{Gonthier08}
G.~Gonthier,
\emph{Formal proof---the four-color theorem},
Notices Amer. Math. Soc. \textbf{55} (2008), no.~11, 1382--1393.
\end{thebibliography}
\end{document} \end{document}