diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.aux b/papers/dual_decomposition_minimal_counterexamples/paper.aux index f615b7e..3a68a03 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.aux +++ b/papers/dual_decomposition_minimal_counterexamples/paper.aux @@ -1,35 +1,51 @@ \relax -\@writefile{toc}{\contentsline {section}{\tocsection {}{1}{The minimal counterexample}}{1}{}\protected@file@percent } -\newlabel{lem:triangulate}{{1.1}{1}} -\newlabel{def:minimal}{{1.2}{1}} -\newlabel{lem:mindeg}{{1.4}{1}} -\@writefile{toc}{\contentsline {section}{\tocsection {}{2}{The reduced dual}}{2}{}\protected@file@percent } -\newlabel{def:reduced-dual}{{2.1}{2}} -\newlabel{def:edge-names}{{2.3}{2}} -\@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 } -\newlabel{fig:reduced-dual-steps}{{1}{3}} -\newlabel{lem:pentagonal-externals}{{2.4}{3}} -\newlabel{lem:chord-apex}{{2.6}{4}} -\@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{fig:chord-apex-proof}{{2}{5}} -\newlabel{lem:kempe-spike}{{2.7}{6}} -\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{Cubic-graph edge contraction}}{7}{}\protected@file@percent } -\newlabel{def:cubic-edge-contraction}{{3.1}{7}} -\@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 } -\newlabel{fig:cubic-edge-contraction}{{3}{7}} -\newlabel{thm:cubic-contraction-4face}{{3.2}{7}} -\@writefile{toc}{\contentsline {section}{\tocsection {}{4}{The face-monochromatic-pair conjecture and the Four Colour Theorem}}{8}{}\protected@file@percent } -\newlabel{sec:toward-4ct}{{4}{8}} -\newlabel{conj:face-monochromatic-pair-on-merged-kempe-cycle}{{4.1}{8}} -\@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:thm-cubic-contraction-4face}{{4}{9}} -\newlabel{rem:conj-3-6-empirical}{{4.2}{9}} -\newlabel{conj:face-monochromatic-pair-strengthened}{{4.3}{10}} -\newlabel{rem:conj-3-8-empirical}{{4.4}{10}} +\citation{AH77a} +\citation{AHK77} +\citation{RSST97} +\citation{Gonthier08} +\@writefile{toc}{\contentsline {section}{\tocsection {}{1}{Introduction}}{1}{}\protected@file@percent } +\newlabel{sec:intro}{{1}{1}} +\@writefile{toc}{\contentsline {paragraph}{\tocparagraph {}{}{Organization.}}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{\tocparagraph {}{}{Companion paper.}}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\tocsection {}{2}{The minimal counterexample}}{2}{}\protected@file@percent } +\newlabel{sec:minimal}{{2}{2}} +\newlabel{lem:triangulate}{{2.1}{2}} +\newlabel{def:minimal}{{2.2}{2}} +\newlabel{lem:mindeg}{{2.4}{3}} +\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{The reduced dual}}{3}{}\protected@file@percent } +\newlabel{sec:reduced-dual}{{3}{3}} +\newlabel{def:reduced-dual}{{3.1}{3}} +\@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:reduced-dual-steps}{{1}{4}} +\newlabel{def:edge-names}{{3.3}{4}} +\newlabel{lem:pentagonal-externals}{{3.4}{4}} +\newlabel{lem:chord-apex}{{3.6}{5}} +\@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 } +\newlabel{fig:chord-apex-proof}{{2}{6}} +\newlabel{lem:kempe-spike}{{3.7}{7}} +\@writefile{toc}{\contentsline {section}{\tocsection {}{4}{Edge suppression}}{8}{}\protected@file@percent } +\newlabel{sec:edge-suppression}{{4}{8}} +\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{tocindent0}{0pt} +\newlabel{tocindent0}{12.7778pt} \newlabel{tocindent1}{17.77782pt} \newlabel{tocindent2}{0pt} \newlabel{tocindent3}{0pt} -\newlabel{rem:implication-4ct}{{4.5}{11}} -\gdef \@abspage@last{11} +\newlabel{rem:implication-4ct}{{5.5}{12}} +\@writefile{toc}{\contentsline {section}{\tocsection {}{}{References}}{12}{}\protected@file@percent } +\gdef \@abspage@last{12} diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.log b/papers/dual_decomposition_minimal_counterexamples/paper.log index 2761a81..9c74678 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.log +++ b/papers/dual_decomposition_minimal_counterexamples/paper.log @@ -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 restricted \write18 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 )) [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 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 )$. [] - + File: fig_reduced_dual_step1.png Graphic file (type 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. - + File: fig_reduced_dual_step2.png Graphic file (type 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. - + File: fig_reduced_dual_step3.png Graphic file (type 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. - + File: fig_reduced_dual_step4.png Graphic file (type 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. 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>] - + File: fig_chord_apex_step1.png Graphic file (type 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. - + File: fig_chord_apex_step2.png Graphic file (type 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. - + File: fig_chord_apex_step3.png Graphic file (type 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. LaTeX Warning: `h' float specifier changed to `ht'. -[4] [5 <./fig_chord_apex_step1.png> <./fig_chord_apex_step2.png> <./fig_chord_a -pex_step3.png>] [6] - +[5] [6 <./fig_chord_apex_step1.png> <./fig_chord_apex_step2.png> <./fig_chord_a +pex_step3.png>] [7] + File: fig_cubic_edge_contraction.png Graphic file (type 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. - [7 <./fig_cubic_edge_contraction.png>] - + [8 <./fig_cubic_edge_contraction.png>] + File: fig_thm_cubic_contraction_4face.png Graphic file (type png) 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. LaTeX Warning: `h' float specifier changed to `ht'. -[8] +[9] Underfull \vbox (badness 10000) has occurred while \output is active [] - [9 <./fig_thm_cubic_contraction_4face.png>] -Underfull \hbox (badness 1648) in paragraph at lines 638--644 -\OT1/cmr/m/it/10 Remark \OT1/cmr/m/n/10 4.4\OT1/cmr/m/it/10 . \OT1/cmr/m/n/10 T + [10 <./fig_thm_cubic_contraction_4face.png>] +Underfull \hbox (badness 1648) in paragraph at lines 721--727 +\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- [] -Underfull \hbox (badness 1014) in paragraph at lines 638--644 -\OT1/cmr/m/n/10 apex+Kempe colour-ings as Re-mark 4.2[]; for each colour-ing we +Underfull \hbox (badness 1014) in paragraph at lines 721--727 +\OT1/cmr/m/n/10 apex+Kempe colour-ings as Re-mark 5.2[]; for each colour-ing we sought any [] -[10] [11] (./paper.aux) ) +[11] [12] (./paper.aux) ) Here is how much of TeX's memory you used: - 3087 strings out of 478268 - 44184 string characters out of 5846347 - 350310 words of memory out of 5000000 - 21121 multiletter control sequences out of 15000+600000 - 478077 words of font info for 62 fonts, out of 8000000 for 9000 + 3097 strings out of 478268 + 44287 string characters out of 5846347 + 350362 words of memory out of 5000000 + 21130 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,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/amsfonts/cm/cmtt10.pfb> -Output written on paper.pdf (11 pages, 941265 bytes). +amsfonts/cm/cmbx8.pfb> + +Output written on paper.pdf (12 pages, 1015233 bytes). PDF statistics: - 144 PDF objects out of 1000 (max. 8388607) - 78 compressed objects within 1 object stream + 183 PDF objects out of 1000 (max. 8388607) + 101 compressed objects within 2 object streams 0 named destinations out of 1000 (max. 500000) 46 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.pdf b/papers/dual_decomposition_minimal_counterexamples/paper.pdf index f9da3a8..911b115 100644 Binary files a/papers/dual_decomposition_minimal_counterexamples/paper.pdf and b/papers/dual_decomposition_minimal_counterexamples/paper.pdf differ diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.tex b/papers/dual_decomposition_minimal_counterexamples/paper.tex index 9806a5f..a9ed411 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.tex +++ b/papers/dual_decomposition_minimal_counterexamples/paper.tex @@ -45,12 +45,99 @@ graph, edge connectivity, cyclic edge cut, Tait colouring, $3$-edge-colouring} \dedicatory{} \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} \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} +\label{sec:minimal} 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 @@ -118,6 +205,7 @@ Hence $\delta(G) \ge 5$. \end{proof} \section{The reduced dual} +\label{sec:reduced-dual} 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 @@ -393,61 +481,63 @@ distinct colours, contradicting Lemma~\ref{lem:chord-apex} applied to $\varphi'$. \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 -out --- under planar duality --- to coincide with simple-graph contraction -on the dual side. It will be the central tool in +We recall the classical operation of \emph{edge suppression} on cubic +plane graphs: delete the edge and smooth the two resulting degree-$2$ +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 condition for the Four Colour Theorem. -\begin{definition}[Cubic-graph edge contraction] -\label{def:cubic-edge-contraction} -Let $H$ be a cubic plane graph and $e = uv$ an edge of $H$ with $u \neq v$ and -no edge of $H$ parallel to $e$. The \emph{cubic-graph edge contraction} of $H$ -along $e$ is the graph $H'$ obtained in two steps: +\begin{definition}[Edge suppression] +\label{def:edge-suppression} +Let $H$ be a cubic plane graph and $e = uv$ an edge of $H$ with $u \neq v$ +and no edge of $H$ parallel to $e$. The \emph{edge suppression} of $H$ at +$e$ is the graph $H'$ obtained in two steps: \begin{enumerate} \item \emph{Delete} the edge $e$; the endpoints $u$ and $v$ each drop to degree $2$. \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 - same at $v$. Both vertices $u$ and $v$ are removed, and two new edges - are added in their place. + remaining incident edges $ua, ub$ by a single new edge $ab$; do + the same at $v$. Both vertices $u$ and $v$ are removed, and two + new edges are added in their place. \end{enumerate} 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 $|E(H')| = |E(H)| - 3$. -Equivalently, $H'$ is the planar dual of $\mathrm{dual}(H) / e^{*}$, where -$e^{*}$ is the edge of $\mathrm{dual}(H)$ crossing $e$ and the contraction -on the right-hand side is simple-graph contraction (loops removed, parallel -edges absorbed). Under planar duality, contracting $e^{*}$ in -$\mathrm{dual}(H)$ merges the two triangular faces of $\mathrm{dual}(H)$ -incident to $e^{*}$, and the parallel-edge cleanup corresponds exactly to -the smoothing step on the primal side. +Equivalently, $H'$ is the planar dual of $\mathrm{dual}(H) / e^{*}$, +where $e^{*}$ is the edge of $\mathrm{dual}(H)$ crossing $e$ and the +contraction on the right-hand side is simple-graph contraction (loops +removed, parallel edges absorbed). Under planar duality, contracting +$e^{*}$ in $\mathrm{dual}(H)$ merges the two triangular faces of +$\mathrm{dual}(H)$ incident to $e^{*}$, and the parallel-edge cleanup +corresponds exactly to the smoothing step on the primal side. \end{definition} \begin{figure}[h] \centering \includegraphics[width=0.95\textwidth]{fig_cubic_edge_contraction.png} -\caption{Cubic-graph edge contraction -(Definition~\ref{def:cubic-edge-contraction}). 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~$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.} -\label{fig:cubic-edge-contraction} +\caption{Edge suppression +(Definition~\ref{def:edge-suppression}). 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~$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.} +\label{fig:edge-suppression} \end{figure} -\begin{theorem}[Cubic contraction across a 4-face preserves 3-edge-colourability] -\label{thm:cubic-contraction-4face} +\begin{theorem}[Edge suppression across a 4-face preserves 3-edge-colourability] +\label{thm:edge-suppression-4face} 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 -two edges of $\partial f$ sharing no endpoint (the opposite pair on the -$4$-cycle $\partial f$). If $\varphi(e_0) \neq \varphi(e_1)$ and the -cubic-graph edge contraction of $H$ along $e_0$ -(Definition~\ref{def:cubic-edge-contraction}) is well-defined (no loops or -parallel edges are created), then the contracted graph admits a proper +let $f$ be a face of $H$ with $|\partial f| = 4$, and let $e_0, e_1$ be +the two edges of $\partial f$ sharing no endpoint (the opposite pair on +the $4$-cycle $\partial f$). If $\varphi(e_0) \neq \varphi(e_1)$ and the +edge suppression of $H$ at $e_0$ +(Definition~\ref{def:edge-suppression}) is well-defined (no loops or +parallel edges are created), then the suppressed graph admits a proper $3$-edge-colouring. \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) = \varphi(w_1) = b$. -\emph{Construction of $\varphi'$.} Let $H'$ denote the cubic-graph edge -contraction of $H$ along $e_0$; its new edges are $e_3' := v_3 u_0$ +\emph{Construction of $\varphi'$.} Let $H'$ denote the edge suppression +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 $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 @@ -506,16 +596,16 @@ $\varphi'$ is proper. \centering \includegraphics[width=0.98\textwidth]{fig_thm_cubic_contraction_4face.png} \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$, $\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 +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 contraction).} -\label{fig:thm-cubic-contraction-4face} +by the suppression).} +\label{fig:thm-edge-suppression-4face} \end{figure} \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 $3$-edge-colouring of a reduced dual of a minimal counterexample. If true, it implies the Four Colour Theorem via -Theorem~\ref{thm:cubic-contraction-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. +Theorem~\ref{thm:edge-suppression-4face}. \begin{conjecture}[Face-monochromatic-pair conjecture] \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 $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 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 the two $c$-edges opposite and the two remaining opposite edges carrying 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 -$\varphi'$-colours. Theorem~\ref{thm:cubic-contraction-4face} then produces -a proper $3$-edge-colouring of the cubic-graph edge contraction -$\widehat{G}'^{+} \!\setminus\! e$ along the $a$-coloured one. +$\varphi'$-colours. Theorem~\ref{thm:edge-suppression-4face} then produces +a proper $3$-edge-colouring of the edge suppression of +$\widehat{G}'^{+}$ at the $a$-coloured one. 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 @@ -688,9 +771,9 @@ $\partial f_n$ unchanged --- placing $\partial f_n$ into the three-colour pattern of case~(i). \smallskip\noindent\emph{Consequence.} -Theorem~\ref{thm:cubic-contraction-4face} now produces a proper -$3$-edge-colouring of the cubic-graph edge contraction of -$\widehat{G}'^{+}$ along the chosen edge of $f_n$. Combined with the +Theorem~\ref{thm:edge-suppression-4face} now produces a proper +$3$-edge-colouring of the edge suppression of $\widehat{G}'^{+}$ at the +chosen edge of $f_n$. Combined with the chord-apex and Kempe-cycle structure of $\widehat{G}'_{v,i}$ (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 @@ -700,4 +783,26 @@ Conjecture~\ref{conj:face-monochromatic-pair-strengthened} implies the Four Colour Theorem. \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}