diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/draw_iterated_reduction.py b/papers/dual_decomposition_iterated_reduction/experiments/draw_iterated_reduction.py similarity index 100% rename from papers/dual_decomposition_minimal_counterexamples/experiments/draw_iterated_reduction.py rename to papers/dual_decomposition_iterated_reduction/experiments/draw_iterated_reduction.py diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/draw_iterated_reduction_n14.py b/papers/dual_decomposition_iterated_reduction/experiments/draw_iterated_reduction_n14.py similarity index 100% rename from papers/dual_decomposition_minimal_counterexamples/experiments/draw_iterated_reduction_n14.py rename to papers/dual_decomposition_iterated_reduction/experiments/draw_iterated_reduction_n14.py diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step0.png b/papers/dual_decomposition_iterated_reduction/fig_alg_step0.png similarity index 100% rename from papers/dual_decomposition_minimal_counterexamples/fig_alg_step0.png rename to papers/dual_decomposition_iterated_reduction/fig_alg_step0.png diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1.png b/papers/dual_decomposition_iterated_reduction/fig_alg_step1.png similarity index 100% rename from papers/dual_decomposition_minimal_counterexamples/fig_alg_step1.png rename to papers/dual_decomposition_iterated_reduction/fig_alg_step1.png diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step2.png b/papers/dual_decomposition_iterated_reduction/fig_alg_step2.png similarity index 100% rename from papers/dual_decomposition_minimal_counterexamples/fig_alg_step2.png rename to papers/dual_decomposition_iterated_reduction/fig_alg_step2.png diff --git a/papers/dual_decomposition_iterated_reduction/paper.aux b/papers/dual_decomposition_iterated_reduction/paper.aux new file mode 100644 index 0000000..37d80d5 --- /dev/null +++ b/papers/dual_decomposition_iterated_reduction/paper.aux @@ -0,0 +1,34 @@ +\relax +\citation{parent} +\citation{parent} +\citation{parent} +\@writefile{toc}{\contentsline {section}{\tocsection {}{1}{Setup and background}}{1}{}\protected@file@percent } +\newlabel{sec:background}{{1}{1}} +\@writefile{toc}{\contentsline {section}{\tocsection {}{2}{The iterated reduction}}{1}{}\protected@file@percent } +\newlabel{sec:iterated-reduction}{{2}{1}} +\newlabel{alg:iterated-reduction}{{2.1}{1}} +\citation{parent} +\citation{parent} +\citation{parent} +\citation{parent} +\citation{parent} +\newlabel{rem:alg-invariants}{{2.2}{2}} +\newlabel{rem:alg-chord-apex}{{2.3}{2}} +\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{Structural lemmas on the algorithm's output}}{2}{}\protected@file@percent } +\newlabel{sec:structural-lemmas}{{3}{2}} +\newlabel{lem:exactly-one-match}{{3.1}{2}} +\citation{parent} +\citation{parent} +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Algorithm\nonbreakingspace 2.1\hbox {} on $G'=\mathrm {dual}(G)$, where $G$ is the first min-degree-$5$ plantri triangulation on $14$ vertices and $\varphi _1$ is a specific proper $3$-edge-colouring of $H_1$ that satisfies both the chord-apex and Kempe-cycle conditions of\nonbreakingspace \cite {parent}, found by \texttt {experiments/search\_kempe\_property.py}. \emph {Left:} $G'$ ($24$ vertices, $36$ edges) with the chosen pentagonal face shaded. \emph {Centre:} $H_1$ ($20$ vertices, $30$ edges) after step\nonbreakingspace (1) with $i_1 = 1$, $3$-edge-coloured by $\varphi _1$; the four edges around $v_n^{(1)}$ in $E$ are drawn thicker, and the spike and merged edges share the colour green. \emph {Right:} $H_2$ ($16$ vertices, $24$ edges) after step\nonbreakingspace (3) with $i_t = 3$; eight edges are protected, and the algorithm terminates one step later (no remaining safe pentagonal face in $H_2$). The generating script is \texttt {experiments/draw\_iterated\_reduction\_n14.py}; layouts are Tutte barycentric embeddings with the outer face picked to keep $v_n^{(1)}, v_n^{(2)}$ in the interior.}}{3}{}\protected@file@percent } +\newlabel{fig:iterated-reduction-trace}{{1}{3}} +\newlabel{lem:all-distinct-exists}{{3.2}{3}} +\citation{parent} +\citation{parent} +\bibcite{parent}{1} +\newlabel{tocindent-1}{0pt} +\newlabel{tocindent0}{12.7778pt} +\newlabel{tocindent1}{17.77782pt} +\newlabel{tocindent2}{0pt} +\newlabel{tocindent3}{0pt} +\@writefile{toc}{\contentsline {section}{\tocsection {}{}{References}}{4}{}\protected@file@percent } +\gdef \@abspage@last{4} diff --git a/papers/dual_decomposition_iterated_reduction/paper.log b/papers/dual_decomposition_iterated_reduction/paper.log new file mode 100644 index 0000000..d7abe64 --- /dev/null +++ b/papers/dual_decomposition_iterated_reduction/paper.log @@ -0,0 +1,247 @@ +This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 13:51 +entering extended mode + restricted \write18 enabled. + %&-line parsing enabled. +**paper.tex +(./paper.tex +LaTeX2e <2021-11-15> patch level 1 +L3 programming layer <2022-02-24> +(/usr/local/texlive/2022/texmf-dist/tex/latex/amscls/amsart.cls +Document Class: amsart 2020/05/29 v2.20.6 +\linespacing=\dimen138 +\normalparindent=\dimen139 +\normaltopskip=\skip47 +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsmath.sty +Package: amsmath 2021/10/15 v2.17l AMS math features +\@mathmargin=\skip48 + +For additional information on amsmath, use the `?' option. +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amstext.sty +Package: amstext 2021/08/26 v2.01 AMS text + +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsgen.sty +File: amsgen.sty 1999/11/30 v2.0 generic functions +\@emptytoks=\toks16 +\ex@=\dimen140 +)) +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsbsy.sty +Package: amsbsy 1999/11/29 v1.2d Bold Symbols +\pmbraise@=\dimen141 +) +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsopn.sty +Package: amsopn 2021/08/26 v2.02 operator names +) +\inf@bad=\count185 +LaTeX Info: Redefining \frac on input line 234. +\uproot@=\count186 +\leftroot@=\count187 +LaTeX Info: Redefining \overline on input line 399. +\classnum@=\count188 +\DOTSCASE@=\count189 +LaTeX Info: Redefining \ldots on input line 496. +LaTeX Info: Redefining \dots on input line 499. +LaTeX Info: Redefining \cdots on input line 620. +\Mathstrutbox@=\box50 +\strutbox@=\box51 +\big@size=\dimen142 +LaTeX Font Info: Redeclaring font encoding OML on input line 743. +LaTeX Font Info: Redeclaring font encoding OMS on input line 744. +\macc@depth=\count190 +\c@MaxMatrixCols=\count191 +\dotsspace@=\muskip16 +\c@parentequation=\count192 +\dspbrk@lvl=\count193 +\tag@help=\toks17 +\row@=\count194 +\column@=\count195 +\maxfields@=\count196 +\andhelp@=\toks18 +\eqnshift@=\dimen143 +\alignsep@=\dimen144 +\tagshift@=\dimen145 +\tagwidth@=\dimen146 +\totwidth@=\dimen147 +\lineht@=\dimen148 +\@envbody=\toks19 +\multlinegap=\skip49 +\multlinetaggap=\skip50 +\mathdisplay@stack=\toks20 +LaTeX Info: Redefining \[ on input line 2938. +LaTeX Info: Redefining \] on input line 2939. +) +LaTeX Font Info: Trying to load font information for U+msa on input line 397 +. + +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsa.fd +File: umsa.fd 2013/01/14 v3.01 AMS symbols A +) +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amsfonts.sty +Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support +\symAMSa=\mathgroup4 +\symAMSb=\mathgroup5 +LaTeX Font Info: Redeclaring math symbol \hbar on input line 98. +LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' +(Font) U/euf/m/n --> U/euf/b/n on input line 106. +) +\copyins=\insert199 +\abstractbox=\box52 +\listisep=\skip51 +\c@part=\count197 +\c@section=\count198 +\c@subsection=\count266 +\c@subsubsection=\count267 +\c@paragraph=\count268 +\c@subparagraph=\count269 +\c@figure=\count270 +\c@table=\count271 +\abovecaptionskip=\skip52 +\belowcaptionskip=\skip53 +\captionindent=\dimen149 +\thm@style=\toks21 +\thm@bodyfont=\toks22 +\thm@headfont=\toks23 +\thm@notefont=\toks24 +\thm@headpunct=\toks25 +\thm@preskip=\skip54 +\thm@postskip=\skip55 +\thm@headsep=\skip56 +\dth@everypar=\toks26 +) +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amssymb.sty +Package: amssymb 2013/01/14 v3.01 AMS font symbols +) +(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphicx.sty +Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2014/10/28 v1.15 key=value parser (DPC) +\KV@toks@=\toks27 +) +(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphics.sty +Package: graphics 2021/03/04 v1.4d Standard LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/trig.sty +Package: trig 2021/08/11 v1.11 sin cos tan (DPC) +) +(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration +) +Package graphics Info: Driver file: pdftex.def on input line 107. + +(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-def/pdftex.def +File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex +)) +\Gin@req@height=\dimen150 +\Gin@req@width=\dimen151 +) +\c@theorem=\count272 + +(/usr/local/texlive/2022/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def +File: l3backend-pdftex.def 2022-02-07 L3 backend support: PDF output (pdfTeX) +\l__color_backend_stack_int=\count273 +\l__pdf_internal_box=\box53 +) +(./paper.aux) +\openout1 = `paper.aux'. + +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 27. +LaTeX Font Info: ... okay on input line 27. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 27. +LaTeX Font Info: ... okay on input line 27. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 27. +LaTeX Font Info: ... okay on input line 27. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 27. +LaTeX Font Info: ... okay on input line 27. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 27. +LaTeX Font Info: ... okay on input line 27. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 27. +LaTeX Font Info: ... okay on input line 27. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 27. +LaTeX Font Info: ... okay on input line 27. +LaTeX Font Info: Trying to load font information for U+msa on input line 27. + + (/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsa.fd +File: umsa.fd 2013/01/14 v3.01 AMS symbols A +) +LaTeX Font Info: Trying to load font information for U+msb on input line 27. + + +(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsb.fd +File: umsb.fd 2013/01/14 v3.01 AMS symbols B +) +(/usr/local/texlive/2022/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +[Loading MPS to PDF converter (version 2006.09.02).] +\scratchcounter=\count274 +\scratchdimen=\dimen152 +\scratchbox=\box54 +\nofMPsegments=\count275 +\nofMParguments=\count276 +\everyMPshowfont=\toks28 +\MPscratchCnt=\count277 +\MPscratchDim=\dimen153 +\MPnumerator=\count278 +\makeMPintoPDFobject=\count279 +\everyMPtoPDFconversion=\toks29 +) (/usr/local/texlive/2022/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty +Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf +Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4 +85. + +(/usr/local/texlive/2022/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +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}] + +File: fig_alg_step0.png Graphic file (type png) + +Package pdftex.def Info: fig_alg_step0.png used on input line 170. +(pdftex.def) Requested size: 115.20264pt x 132.48134pt. + +File: fig_alg_step1.png Graphic file (type png) + +Package pdftex.def Info: fig_alg_step1.png used on input line 171. +(pdftex.def) Requested size: 115.20264pt x 132.48134pt. + +File: fig_alg_step2.png Graphic file (type png) + +Package pdftex.def Info: fig_alg_step2.png used on input line 172. +(pdftex.def) Requested size: 115.20264pt x 132.48134pt. + + +LaTeX Warning: `h' float specifier changed to `ht'. + +[2] [3 <./fig_alg_step0.png> <./fig_alg_step1.png> <./fig_alg_step2.png>] +[4] (./paper.aux) ) +Here is how much of TeX's memory you used: + 3022 strings out of 478268 + 42273 string characters out of 5846347 + 343206 words of memory out of 5000000 + 21067 multiletter control sequences out of 15000+600000 + 475834 words of font info for 54 fonts, out of 8000000 for 9000 + 1302 hyphenation exceptions out of 8191 + 69i,7n,76p,1399b,294s stack positions out of 10000i,1000n,20000p,200000b,200000s + + +Output written on paper.pdf (4 pages, 387470 bytes). +PDF statistics: + 109 PDF objects out of 1000 (max. 8388607) + 62 compressed objects within 1 object stream + 0 named destinations out of 1000 (max. 500000) + 16 words of extra memory for PDF output out of 10000 (max. 10000000) + diff --git a/papers/dual_decomposition_iterated_reduction/paper.pdf b/papers/dual_decomposition_iterated_reduction/paper.pdf new file mode 100644 index 0000000..7de74e7 Binary files /dev/null and b/papers/dual_decomposition_iterated_reduction/paper.pdf differ diff --git a/papers/dual_decomposition_iterated_reduction/paper.tex b/papers/dual_decomposition_iterated_reduction/paper.tex new file mode 100644 index 0000000..62bf5a7 --- /dev/null +++ b/papers/dual_decomposition_iterated_reduction/paper.tex @@ -0,0 +1,308 @@ +%% filename: amsart-template.tex +%% American Mathematical Society +%% AMS-LaTeX v.2 template for use with amsart +%% ==================================================================== + +\documentclass{amsart} + +\usepackage{amssymb} +\usepackage{graphicx} + +\newtheorem{theorem}{Theorem}[section] +\newtheorem{lemma}[theorem]{Lemma} +\newtheorem{corollary}[theorem]{Corollary} +\newtheorem{proposition}[theorem]{Proposition} +\newtheorem{conjecture}[theorem]{Conjecture} + +\theoremstyle{definition} +\newtheorem{definition}[theorem]{Definition} +\newtheorem{example}[theorem]{Example} +\newtheorem{algorithm}[theorem]{Algorithm} + +\theoremstyle{remark} +\newtheorem{remark}[theorem]{Remark} + +\numberwithin{equation}{section} + +\begin{document} + +\title{Iterated Reduction of Dual Minimal Counterexamples} + +\author{Eric Bauerfeld} +\address{} +\curraddr{} +\email{} +\thanks{} + +\subjclass[2010]{Primary } + +\keywords{four colour theorem, plane triangulation, dual graph, cubic planar +graph, edge connectivity, cyclic edge cut, Tait colouring, +$3$-edge-colouring} + +\date{} + +\dedicatory{} + +\begin{abstract} +% TODO: abstract. +\end{abstract} + +\maketitle + +\section{Setup and background} +\label{sec:background} + +This paper is a follow-up to \emph{Dual Decomposition of Minimal +Counterexamples}~\cite{parent}, which introduced the reduced-dual +construction: given a minimal counterexample $G$ to the Four Colour +Theorem, a degree-$5$ vertex $v$ of $G$ (equivalently a pentagonal face +$F_v$ of $G' = \mathrm{dual}(G)$), and an index $i \in \{0,1,2,3,4\}$, the +\emph{reduced dual} $\widehat{G}'_{v,i}$ is the cubic plane graph obtained +from $G'$ by deleting the five boundary vertices of $F_v$, listing the +resulting five degree-$2$ vertices clockwise as $A_0,\dots,A_4$ along the +new face $F$, attaching a new apex vertex $v_n$ to $A_i, A_{i+1}, A_{i+2}$ +by three new edges, and adding the chord $A_{i+3} A_{i+4}$. The four edges +added by steps~(3) and~(4) are named the \emph{side-$0$ edge} +($v_n A_i$), the \emph{spike edge} ($v_n A_{i+1}$), the \emph{side-$1$ +edge} ($v_n A_{i+2}$), and the \emph{merged edge} ($A_{i+3} A_{i+4}$). The +parent paper also proves two structural lemmas about every proper +$3$-edge-colouring $\varphi$ of $\widehat{G}'_{v,i}$: +\begin{itemize} + \item the \emph{chord-apex lemma}, asserting + $\varphi(\mathrm{spike}) = \varphi(\mathrm{merged})$; + \item the \emph{Kempe-cycle lemma}, asserting that + the spike and merged edge lie on a common + $\{\varphi(\mathrm{spike}), \varphi(\mathrm{side-}j)\}$-Kempe + cycle through the side-$j$ edge for both $j = 0, 1$. +\end{itemize} +We refer the reader to~\cite{parent} for the precise definitions, proofs, +and the pentagonal-externals lemma we will reuse below. + +\section{The iterated reduction} +\label{sec:iterated-reduction} + +The reduced-dual construction can be iterated: starting from a proper +$3$-edge-colouring $\varphi_1$ of a reduced dual $\widehat{G}'_{v,i}$, we +apply the construction again to that graph at a pentagonal face whose ten +incident edges avoid the four named edges from the first reduction, +extending $\varphi_1$ across the new reduction. The protected edges +accumulate into a set $E$ that grows by four per iteration, and the +process terminates when $E$ has blocked every pentagonal face. + +\begin{algorithm}[Iterated reduction with protected edges] +\label{alg:iterated-reduction} +Let $G$ be a triangulation we assume to be a minimal counterexample to the +Four Colour Theorem. The algorithm produces a sequence $H_1, H_2, \dots$ of +cubic plane graphs, proper $3$-edge-colourings $\varphi_t$ of $H_t$, and a +growing set $E$ of protected edges. + +\begin{enumerate} + \item[(0)] Form $G' := \mathrm{dual}(G)$, a cubic plane graph. + + \item[(1)] Choose a degree-$5$ vertex $v$ of $G$ (equivalently a + pentagonal face $F_v$ of $G'$) and an index + $i_1 \in \{0, \dots, 4\}$. Apply the reduced-dual construction + of~\cite{parent} to form $H_1 := \widehat{G'}_{v, i_1}$, and fix + any proper $3$-edge-colouring $\varphi_1$ of $H_1$ (one exists + by the minimality of $G$). + + \item[(2)] Initialise + $E := \{\text{spike}, \text{side-}0, \text{side-}1, + \text{merged}\}$, the four named edges of the reduction in~(1). + + \item[(3)] (Iterate.) At step $t \geq 2$, given $H_{t-1}$, + $\varphi_{t-1}$, and $E \subseteq E(H_{t-1})$: + \begin{enumerate} + \item[(a)] Find a pentagonal face $F$ of $H_{t-1}$ whose ten + incident edges --- the five boundary edges of $\partial F$ + and the five external edges at $\partial F$ --- are all + outside $E$. If no such $F$ exists, terminate. + \item[(b)] By the pentagonal-externals lemma of~\cite{parent} + applied to $H_{t-1}$ at $F$ under $\varphi_{t-1}$, the + external vector has shape $(a, b, c, c, c)$ up to cyclic + rotation. Choose an index $i_t$ for which + $\varphi_{t-1}(f_{i_t + 3}) = \varphi_{t-1}(f_{i_t + 4})$ + and $\varphi_{t-1}(f_{i_t})$, $\varphi_{t-1}(f_{i_t + 1})$, + $\varphi_{t-1}(f_{i_t + 2})$ are three distinct colours. + \item[(c)] Apply the reduced-dual construction + of~\cite{parent} to $H_{t-1}$ at $(F, i_t)$ to form $H_t$. + \item[(d)] Extend $\varphi_{t-1}$ to a proper + $3$-edge-colouring $\varphi_t$ of $H_t$: every surviving + edge keeps its $\varphi_{t-1}$-colour, and each new edge + takes the unique colour completing the palette at its + endpoint (consistent across both endpoints of the chord + by the choice of $i_t$). + \item[(e)] Add the four named edges of the step-$t$ reduction + to $E$. + \end{enumerate} + + \item[(4)] Repeat (3) until termination. +\end{enumerate} +\end{algorithm} + +\begin{remark} +\label{rem:alg-invariants} +At each iteration, $|V(H_t)| = |V(H_{t-1})| - 4$ and +$|E(H_t)| = |E(H_{t-1})| - 6$, so $H_t$ shrinks at a fixed rate; the +protected set $|E|$ grows by exactly four; and every protected edge +survives all subsequent reductions. Since the graph is finite, +termination is guaranteed. By the pentagonal-externals lemma +of~\cite{parent}, step~(b) never fails: some valid $i_t$ always exists +for any pentagonal face under any proper colouring. Termination is +therefore combinatorial: it occurs precisely when $E$ touches every +pentagonal face of $H_{t-1}$. +\end{remark} + +\begin{remark} +\label{rem:alg-chord-apex} +The chord-apex lemma of~\cite{parent} applies only at $t = 1$, when $H_1$ +is a reduced dual of $G'$. For $t \geq 2$, $H_t$ is a reduced dual of +$H_{t-1}$ rather than of $G'$, and $H_{t-1}$ is itself +$3$-edge-colourable, so the non-$3$-edge-colourability argument that +drives the chord-apex lemma does not carry over. Whether the constraints +accumulated in $E$ propagate any further structure to $\varphi_t$ for +$t \geq 2$ is left open. +\end{remark} + +\begin{figure}[h] +\centering +\includegraphics[width=0.32\textwidth]{fig_alg_step0.png}\hfill +\includegraphics[width=0.32\textwidth]{fig_alg_step1.png}\hfill +\includegraphics[width=0.32\textwidth]{fig_alg_step2.png} +\caption{Algorithm~\ref{alg:iterated-reduction} on +$G'=\mathrm{dual}(G)$, where $G$ is the first min-degree-$5$ plantri +triangulation on $14$ vertices and $\varphi_1$ is a specific proper +$3$-edge-colouring of $H_1$ that satisfies both the chord-apex and +Kempe-cycle conditions of~\cite{parent}, found by +\texttt{experiments/search\_kempe\_property.py}. \emph{Left:} $G'$ +($24$ vertices, $36$ edges) with the chosen pentagonal face shaded. +\emph{Centre:} $H_1$ ($20$ vertices, $30$ edges) after step~(1) with +$i_1 = 1$, $3$-edge-coloured by $\varphi_1$; the four edges around +$v_n^{(1)}$ in $E$ are drawn thicker, and the spike and merged edges +share the colour green. \emph{Right:} $H_2$ ($16$ vertices, $24$ edges) +after step~(3) with $i_t = 3$; eight edges are protected, and the +algorithm terminates one step later (no remaining safe pentagonal face +in $H_2$). The generating script is +\texttt{experiments/draw\_iterated\_reduction\_n14.py}; layouts are +Tutte barycentric embeddings with the outer face picked to keep +$v_n^{(1)}, v_n^{(2)}$ in the interior.} +\label{fig:iterated-reduction-trace} +\end{figure} + +\section{Structural lemmas on the algorithm's output} +\label{sec:structural-lemmas} + +\begin{lemma}[Exactly one matching pair in the algorithm's output] +\label{lem:exactly-one-match} +Let $G$ be a minimal counterexample to the Four Colour Theorem, and let +$(H_{t^*}, \varphi_{t^*})$ be the final graph-and-colouring produced by +some terminating execution of +Algorithm~\ref{alg:iterated-reduction} on $G$, with named pairs +$(\mathrm{spike}_t, \mathrm{merged}_t)$ for $t = 1, \dots, t^*$. Then +there is exactly one $t$ with +$\varphi_{t^*}(\mathrm{spike}_t) = \varphi_{t^*}(\mathrm{merged}_t)$, and +it is $t = 1$. +\end{lemma} + +\begin{proof} +The algorithm never re-colours an existing edge: at each iteration +step~(3d) every surviving edge keeps its $\varphi_{t-1}$-colour, and the +four new edges receive fresh colours forced by propriety. Hence for every +$1 \leq k \leq t \leq t^*$, +\[ + \varphi_t(\mathrm{spike}_k) = \varphi_k(\mathrm{spike}_k), + \qquad + \varphi_t(\mathrm{merged}_k) = \varphi_k(\mathrm{merged}_k); +\] +the colours of the step-$k$ named edges, once written, are permanent. It +suffices to compare $\varphi_k(\mathrm{spike}_k)$ and +$\varphi_k(\mathrm{merged}_k)$ at the step where each pair is introduced. + +\textbf{Case $k = 1$.} Since $G$ is a minimal counterexample, $H_1$ is a +reduced dual of $G'$. The chord-apex lemma of~\cite{parent} applied to +$\varphi_1$ gives +$\varphi_1(\mathrm{spike}_1) = \varphi_1(\mathrm{merged}_1)$. + +\textbf{Case $k \geq 2$.} At step $k$ the algorithm picks an index $i_k$ +for which $f_{i_k+3} = f_{i_k+4}$ (chord consistency) and +$f_{i_k}, f_{i_k+1}, f_{i_k+2}$ are pairwise distinct (propriety at the +new $v_n$), where $f$ is the external vector of the chosen pentagonal +face of $H_{k-1}$ under $\varphi_{k-1}$. Step~(3d) then assigns +\[ + \varphi_k(\mathrm{spike}_k) = f_{i_k+1}, + \qquad + \varphi_k(\mathrm{merged}_k) = f_{i_k+3}. +\] +By the pentagonal-externals lemma of~\cite{parent}, $f$ has the $(2,2,1)$ +pattern: a block of three consecutive positions $\{p, p+1, p+2\}$ +(mod $5$) on which it is constantly some colour $c$, while the remaining +two positions $\{p+3, p+4\}$ hold the two non-$c$ colours, one each. The +condition $f_{i_k+3} = f_{i_k+4}$ forces $(i_k+3, i_k+4)$ to be either +$(p, p+1)$ or $(p+1, p+2)$ --- the two consecutive pairs inside the +block --- and correspondingly $i_k + 1 \in \{p+3, p+4\}$, +\emph{outside} the block. So $f_{i_k+1}$ is not $c$, whereas +$f_{i_k+3} = c$, and hence +$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$. + +Combining the two cases, exactly one $t \in \{1, \dots, t^*\}$ --- namely +$t = 1$ --- has $\varphi_{t^*}(\mathrm{spike}_t) = +\varphi_{t^*}(\mathrm{merged}_t)$. +\end{proof} + +\begin{lemma}[All-distinct colouring exists on a 4-colourable graph] +\label{lem:all-distinct-exists} +Let $G$ be a $4$-colourable maximal planar graph of minimum degree +$\geq 5$ (equivalently, a maximal planar graph that is \emph{not} a +minimal counterexample to the Four Colour Theorem). Then there is an +execution of Algorithm~\ref{alg:iterated-reduction} on $G$ whose final +colouring $\varphi_{t^*}$ satisfies +$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ +for every $t \in \{1, \dots, t^*\}$. In particular, there exists a proper +$3$-edge-colouring of $H_{t^*}$ under which every spike-merged pair has +distinct colours. +\end{lemma} + +\begin{proof} +The argument mirrors Lemma~\ref{lem:exactly-one-match}, but extends a +colouring \emph{downward} from $G'$ rather than carrying one forward from +$H_1$. + +Since $G$ is $4$-colourable, by Tait's theorem +$G' = \mathrm{dual}(G)$ admits a proper $3$-edge-colouring $\xi$. Apply +the pentagonal-externals lemma of~\cite{parent} to $\xi$ at the +pentagonal face $F_v$ selected in step~(1): the external vector +$f = (f_0, \dots, f_4)$ at $F_v$ under $\xi$ has the $(3,1,1)$ +cyclic-consecutive shape, with a block of three consecutive positions +$\{p, p+1, p+2\}$ (mod $5$) holding a common colour $c$, and the +remaining two positions $\{p+3, p+4\}$ holding the two non-$c$ colours, +one each. The algorithm's choice of $i_1$ forces $\{i_1+3, i_1+4\}$ +inside the $c$-block (so the chord is consistently coloured) and the +three positions $\{i_1, i_1+1, i_1+2\}$ pairwise distinct; in particular +$i_1+1$ lies \emph{outside} the $c$-block. + +Choose $\varphi_1$ to be the proper $3$-edge-colouring of $H_1$ that +agrees with $\xi$ on every surviving edge and assigns each new edge at +$A_j$ the unique third colour at $A_j$. Then +$\varphi_1(\mathrm{spike}_1) = f_{i_1+1}$, a value not equal to $c$, +while $\varphi_1(\mathrm{merged}_1) = f_{i_1+3} = c$, so +$\varphi_1(\mathrm{spike}_1) \neq \varphi_1(\mathrm{merged}_1)$. + +The same argument repeats at every step $k \geq 2$: the external vector +at the chosen pentagonal face under $\varphi_{k-1}$ has the $(3,1,1)$ +cyclic-consecutive shape (pentagonal-externals lemma of~\cite{parent}), +the algorithm's index choice $i_k$ puts $i_k+3, i_k+4$ inside the colour +block and $i_k+1$ outside, and step~(3d) thus assigns +$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$. The +algorithm preserves these colours through every later step, so +$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ +for every $t \in \{1, \dots, t^*\}$. +\end{proof} + +\begin{thebibliography}{9} +\bibitem{parent} +E.~Bauerfeld, \emph{Dual Decomposition of Minimal Counterexamples}. +Companion paper. +\end{thebibliography} + +\end{document} diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.aux b/papers/dual_decomposition_minimal_counterexamples/paper.aux index 1c3ebee..85baaab 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.aux +++ b/papers/dual_decomposition_minimal_counterexamples/paper.aux @@ -13,30 +13,23 @@ \@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}{An iterated reduction}}{7}{}\protected@file@percent } -\newlabel{alg:iterated-reduction}{{3.1}{7}} -\newlabel{rem:alg-invariants}{{3.2}{7}} -\newlabel{rem:alg-chord-apex}{{3.3}{7}} -\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Algorithm\nonbreakingspace 3.1\hbox {} on $G'=\mathrm {dual}(G)$, where $G$ is the first min-degree-$5$ plantri triangulation on $14$ vertices and $\varphi _1$ is a specific proper $3$-edge-colouring of $H_1$ that satisfies both the chord-apex condition (Lemma\nonbreakingspace 2.6\hbox {}) and the Kempe-cycle condition (Lemma\nonbreakingspace 2.7\hbox {}), found by \texttt {experiments/search\_kempe\_property.py}. \emph {Left:} $G'$ ($24$ vertices, $36$ edges) with the chosen pentagonal face shaded. \emph {Centre:} $H_1$ ($20$ vertices, $30$ edges) after step\nonbreakingspace (1) with $i_1 = 1$, $3$-edge-coloured by $\varphi _1$; the four edges around $v_n^{(1)}$ in $E$ are drawn thicker, and the spike and merged edges share the colour green. \emph {Right:} $H_2$ ($16$ vertices, $24$ edges) after step\nonbreakingspace (3) with $i_t = 3$; eight edges are protected, and the algorithm terminates one step later (no remaining safe pentagonal face in $H_2$). The generating script is \texttt {experiments/draw\_iterated\_reduction\_n14.py}; layouts are Tutte barycentric embeddings with the outer face picked to keep $v_n^{(1)}, v_n^{(2)}$ in the interior.}}{8}{}\protected@file@percent } -\newlabel{fig:iterated-reduction-trace}{{3}{8}} -\newlabel{lem:exactly-one-match}{{3.4}{8}} -\newlabel{lem:all-distinct-exists}{{3.5}{9}} -\newlabel{conj:face-monochromatic-pair-on-merged-kempe-cycle}{{3.6}{9}} -\newlabel{rem:conj-3-6-empirical}{{3.7}{10}} -\newlabel{def:cubic-edge-contraction}{{3.8}{10}} -\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Cubic-graph edge contraction (Definition\nonbreakingspace 3.8\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.}}{11}{}\protected@file@percent } -\newlabel{fig:cubic-edge-contraction}{{4}{11}} -\newlabel{thm:cubic-contraction-4face}{{3.9}{11}} -\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces The recolouring used in the proof of Theorem\nonbreakingspace 3.9\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).}}{12}{}\protected@file@percent } -\newlabel{fig:thm-cubic-contraction-4face}{{5}{12}} -\@writefile{toc}{\contentsline {section}{\tocsection {}{4}{The Four Colour Theorem from a strengthened conjecture}}{12}{}\protected@file@percent } -\newlabel{sec:toward-4ct}{{4}{12}} -\newlabel{conj:face-monochromatic-pair-strengthened}{{4.1}{12}} +\@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}} +\newlabel{rem:implication-4ct}{{4.5}{10}} \newlabel{tocindent-1}{0pt} \newlabel{tocindent0}{0pt} \newlabel{tocindent1}{17.77782pt} \newlabel{tocindent2}{0pt} \newlabel{tocindent3}{0pt} -\newlabel{rem:conj-3-8-empirical}{{4.2}{13}} -\newlabel{rem:implication-4ct}{{4.3}{13}} -\gdef \@abspage@last{14} +\gdef \@abspage@last{11} diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.log b/papers/dual_decomposition_minimal_counterexamples/paper.log index a10361e..de287e5 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 13:42 +This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 14:04 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -244,119 +244,69 @@ 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] -Overfull \hbox (4.76643pt too wide) in paragraph at lines 433--440 -\OT1/cmr/m/n/10 which $\OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[ -]\OT1/cmr/m/n/10 ) = \OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\ -OT1/cmr/m/n/10 )$ and $\OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[ -]\OT1/cmr/m/n/10 )\OML/cmm/m/it/10 ; '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\O -T1/cmr/m/n/10 )\OML/cmm/m/it/10 ; '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\OT1/ -cmr/m/n/10 )$ - [] - - -File: fig_alg_step0.png Graphic file (type png) - -Package pdftex.def Info: fig_alg_step0.png used on input line 479. -(pdftex.def) Requested size: 115.20264pt x 132.48134pt. - -File: fig_alg_step1.png Graphic file (type png) - -Package pdftex.def Info: fig_alg_step1.png used on input line 480. -(pdftex.def) Requested size: 115.20264pt x 132.48134pt. - -File: fig_alg_step2.png Graphic file (type png) - -Package pdftex.def Info: fig_alg_step2.png used on input line 481. -(pdftex.def) Requested size: 115.20264pt x 132.48134pt. - -Underfull \hbox (badness 4391) in paragraph at lines 498--498 -\OT1/cmr/m/sc/10 Figure 3.\OT1/cmr/m/n/10 Algorithm 3.1[] on $\OML/cmm/m/it/10 -G[] \OT1/cmr/m/n/10 = [](\OML/cmm/m/it/10 G\OT1/cmr/m/n/10 )$, where $\OML/cmm/ -m/it/10 G$ - [] - - -Underfull \hbox (badness 3623) in paragraph at lines 498--498 -\OT1/cmr/m/n/10 is the first min-degree-$5$ plantri tri-an-gu-la-tion on $14$ v -er- - [] - - -Underfull \hbox (badness 3179) in paragraph at lines 498--498 -\OT1/cmr/m/n/10 tices and $\OML/cmm/m/it/10 '[]$ \OT1/cmr/m/n/10 is a spe-cific - proper $3$-edge-colouring of $\OML/cmm/m/it/10 H[]$ - [] - - -Underfull \hbox (badness 3209) in paragraph at lines 498--498 -\OT1/cmr/m/n/10 that sat-is-fies both the chord-apex con-di-tion (Lemma 2.6[]) - [] - - -Underfull \hbox (badness 6094) in paragraph at lines 498--498 -\OT1/cmr/m/n/10 and the Kempe-cycle con-di-tion (Lemma 2.7[]), found by - [] - -[7] [8 <./fig_alg_step0.png> <./fig_alg_step1.png> <./fig_alg_step2.png>] -[9] [10] - + File: fig_cubic_edge_contraction.png Graphic file (type png) -Package pdftex.def Info: fig_cubic_edge_contraction.png used on input line 702 +Package pdftex.def Info: fig_cubic_edge_contraction.png used on input line 432 . (pdftex.def) Requested size: 341.9989pt x 73.08138pt. - [11 <./fig_cubic_edge_contraction.png>] - + [7 <./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 777. +e 507. (pdftex.def) Requested size: 352.79846pt x 160.78339pt. - [12 <./fig_thm_cubic_contraction_4face.png>] -Underfull \hbox (badness 1648) in paragraph at lines 837--842 -\OT1/cmr/m/it/10 Remark \OT1/cmr/m/n/10 4.2\OT1/cmr/m/it/10 . \OT1/cmr/m/n/10 T + + +LaTeX Warning: `h' float specifier changed to `ht'. + +[8] +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 he strength-ened con-jec-ture was tested on the same chord- [] -Underfull \hbox (badness 1014) in paragraph at lines 837--842 -\OT1/cmr/m/n/10 apex+Kempe colour-ings as Re-mark 3.7[]; for each colour-ing we +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 sought any [] -[13] [14] (./paper.aux) ) +[10] [11] (./paper.aux) ) Here is how much of TeX's memory you used: - 3114 strings out of 478268 - 44776 string characters out of 5846347 - 346374 words of memory out of 5000000 - 21145 multiletter control sequences out of 15000+600000 + 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 1302 hyphenation exceptions out of 8191 - 69i,9n,76p,1306b,326s stack positions out of 10000i,1000n,20000p,200000b,200000s + 69i,9n,76p,744b,373s stack positions out of 10000i,1000n,20000p,200000b,200000s < -/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb> -Output written on paper.pdf (14 pages, 1148116 bytes). +sfonts/cm/cmmi7.pfb>< +/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb> +Output written on paper.pdf (11 pages, 941151 bytes). PDF statistics: - 175 PDF objects out of 1000 (max. 8388607) - 94 compressed objects within 1 object stream + 144 PDF objects out of 1000 (max. 8388607) + 78 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) - 61 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) diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.pdf b/papers/dual_decomposition_minimal_counterexamples/paper.pdf index ee61828..f076eee 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 f79f6ec..9a30bc3 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.tex +++ b/papers/dual_decomposition_minimal_counterexamples/paper.tex @@ -393,281 +393,11 @@ distinct colours, contradicting Lemma~\ref{lem:chord-apex} applied to $\varphi'$. \end{proof} -\section{An iterated reduction} +\section{Cubic-graph edge contraction} -The reduced-dual construction in Definition~\ref{def:reduced-dual} can be -iterated: starting from a proper $3$-edge-colouring $\varphi_1$ of a reduced -dual $\widehat{G}'_{v,i}$, we apply the construction again to that graph at -a pentagonal face whose ten incident edges avoid the four named edges from -the first reduction, extending $\varphi_1$ across the new reduction. The -protected edges accumulate into a set $E$ that grows by four per iteration, -and the process terminates when $E$ has blocked every pentagonal face. - -\begin{algorithm}[Iterated reduction with protected edges] -\label{alg:iterated-reduction} -Let $G$ be a triangulation we assume to be a minimal counterexample to the -Four Colour Theorem. The algorithm produces a sequence $H_1, H_2, \dots$ of -cubic plane graphs, proper $3$-edge-colourings $\varphi_t$ of $H_t$, and a -growing set $E$ of protected edges. - -\begin{enumerate} - \item[(0)] Form $G' := \mathrm{dual}(G)$, a cubic plane graph. - - \item[(1)] Choose a degree-$5$ vertex $v$ of $G$ (equivalently a pentagonal - face $F_v$ of $G'$) and an index $i_1 \in \{0, \dots, 4\}$. Apply - Definition~\ref{def:reduced-dual} to form - $H_1 := \widehat{G'}_{v, i_1}$, and fix any proper - $3$-edge-colouring $\varphi_1$ of $H_1$ (one exists by the minimality - of $G$). - - \item[(2)] Initialise $E := \{\text{spike}, \text{side-}0, \text{side-}1, - \text{merged}\}$, the four named edges of the reduction in (1). - - \item[(3)] (Iterate.) At step $t \geq 2$, given $H_{t-1}$, $\varphi_{t-1}$, - and $E \subseteq E(H_{t-1})$: - \begin{enumerate} - \item[(a)] Find a pentagonal face $F$ of $H_{t-1}$ whose ten - incident edges --- the five boundary edges of $\partial F$ - and the five external edges at $\partial F$ --- are all - outside $E$. If no such $F$ exists, terminate. - \item[(b)] By Lemma~\ref{lem:pentagonal-externals} applied to - $H_{t-1}$ at $F$ under $\varphi_{t-1}$, the external vector - has shape $(a, b, c, c, c)$ up to cyclic rotation. Choose an - index $i_t$ for which - $\varphi_{t-1}(f_{i_t + 3}) = \varphi_{t-1}(f_{i_t + 4})$ and - $\varphi_{t-1}(f_{i_t}), \varphi_{t-1}(f_{i_t + 1}), - \varphi_{t-1}(f_{i_t + 2})$ are three distinct colours. - \item[(c)] Apply Definition~\ref{def:reduced-dual} to $H_{t-1}$ at - $(F, i_t)$ to form $H_t$. - \item[(d)] Extend $\varphi_{t-1}$ to a proper $3$-edge-colouring - $\varphi_t$ of $H_t$: every surviving edge keeps its - $\varphi_{t-1}$-colour, and each new edge takes the unique - colour completing the palette at its endpoint (consistent - across both endpoints of the chord by the choice of $i_t$). - \item[(e)] Add the four named edges of the step-$t$ reduction to - $E$. - \end{enumerate} - - \item[(4)] Repeat (3) until termination. -\end{enumerate} -\end{algorithm} - -\begin{remark} -\label{rem:alg-invariants} -At each iteration, $|V(H_t)| = |V(H_{t-1})| - 4$ and -$|E(H_t)| = |E(H_{t-1})| - 6$, so $H_t$ shrinks at a fixed rate; the -protected set $|E|$ grows by exactly four; and every protected edge survives -all subsequent reductions. Since the graph is finite, termination is -guaranteed. By Lemma~\ref{lem:pentagonal-externals}, step~(b) never fails: -some valid $i_t$ always exists for any pentagonal face under any proper -colouring. Termination is therefore combinatorial: it occurs precisely when -$E$ touches every pentagonal face of $H_{t-1}$. -\end{remark} - -\begin{remark} -\label{rem:alg-chord-apex} -Lemma~\ref{lem:chord-apex} applies only at $t = 1$, when $H_1$ is a reduced -dual of $G'$. For $t \geq 2$, $H_t$ is a reduced dual of $H_{t-1}$ rather than -of $G'$, and $H_{t-1}$ is itself $3$-edge-colourable, so the -non-$3$-edge-colourability argument that drives Lemma~\ref{lem:chord-apex} -does not carry over. Whether the constraints accumulated in $E$ propagate -any further structure to $\varphi_t$ for $t \geq 2$ is left open. -\end{remark} - -\begin{figure}[h] -\centering -\includegraphics[width=0.32\textwidth]{fig_alg_step0.png}\hfill -\includegraphics[width=0.32\textwidth]{fig_alg_step1.png}\hfill -\includegraphics[width=0.32\textwidth]{fig_alg_step2.png} -\caption{Algorithm~\ref{alg:iterated-reduction} on $G'=\mathrm{dual}(G)$, where -$G$ is the first min-degree-$5$ plantri triangulation on $14$ vertices and -$\varphi_1$ is a specific proper $3$-edge-colouring of $H_1$ that satisfies -both the chord-apex condition (Lemma~\ref{lem:chord-apex}) and the Kempe-cycle -condition (Lemma~\ref{lem:kempe-spike}), found by -\texttt{experiments/search\_kempe\_property.py}. \emph{Left:} $G'$ -($24$ vertices, $36$ edges) with the chosen pentagonal face shaded. -\emph{Centre:} $H_1$ ($20$ vertices, $30$ edges) after step~(1) with -$i_1 = 1$, $3$-edge-coloured by $\varphi_1$; the four edges around -$v_n^{(1)}$ in $E$ are drawn thicker, and the spike and merged edges share -the colour green. \emph{Right:} $H_2$ ($16$ vertices, $24$ edges) after -step~(3) with $i_t = 3$; eight edges are protected, and the algorithm -terminates one step later (no remaining safe pentagonal face in $H_2$). -The generating script is -\texttt{experiments/draw\_iterated\_reduction\_n14.py}; layouts are Tutte -barycentric embeddings with the outer face picked to keep $v_n^{(1)}, -v_n^{(2)}$ in the interior.} -\label{fig:iterated-reduction-trace} -\end{figure} - -\begin{lemma}[Exactly one matching pair in the algorithm's output] -\label{lem:exactly-one-match} -Let $G$ be a minimal counterexample to the Four Colour Theorem, and let -$(H_{t^*}, \varphi_{t^*})$ be the final graph-and-colouring produced by some -terminating execution of Algorithm~\ref{alg:iterated-reduction} on $G$, with -named pairs $(\mathrm{spike}_t, \mathrm{merged}_t)$ for $t = 1, \dots, t^*$. -Then there is exactly one $t$ with -$\varphi_{t^*}(\mathrm{spike}_t) = \varphi_{t^*}(\mathrm{merged}_t)$, and it -is $t = 1$. -\end{lemma} - -\begin{proof} -The algorithm never re-colours an existing edge: at each iteration -step~(3d) every surviving edge keeps its $\varphi_{t-1}$-colour, and the -four new edges receive fresh colours forced by propriety. Hence for every -$1 \leq k \leq t \leq t^*$, -\[ - \varphi_t(\mathrm{spike}_k) = \varphi_k(\mathrm{spike}_k), - \qquad - \varphi_t(\mathrm{merged}_k) = \varphi_k(\mathrm{merged}_k); -\] -the colours of the step-$k$ named edges, once written, are permanent. It -suffices to compare $\varphi_k(\mathrm{spike}_k)$ and -$\varphi_k(\mathrm{merged}_k)$ at the step where each pair is introduced. - -\textbf{Case $k = 1$.} Since $G$ is a minimal counterexample, $H_1$ is a -reduced dual of $G'$. Lemma~\ref{lem:chord-apex} applied to $\varphi_1$ gives -$\varphi_1(\mathrm{spike}_1) = \varphi_1(\mathrm{merged}_1)$. - -\textbf{Case $k \geq 2$.} At step $k$ the algorithm picks an index $i_k$ for -which $f_{i_k+3} = f_{i_k+4}$ (chord consistency) and $f_{i_k}, f_{i_k+1}, -f_{i_k+2}$ are pairwise distinct (propriety at the new $v_n$), where $f$ is -the external vector of the chosen pentagonal face of $H_{k-1}$ under -$\varphi_{k-1}$. Step~(3d) then assigns -\[ - \varphi_k(\mathrm{spike}_k) = f_{i_k+1}, - \qquad - \varphi_k(\mathrm{merged}_k) = f_{i_k+3}. -\] -By Lemma~\ref{lem:pentagonal-externals}, $f$ has the $(2,2,1)$ pattern: a -block of three consecutive positions $\{p, p+1, p+2\}$ (mod $5$) on which it -is constantly some colour $c$, while the remaining two positions -$\{p+3, p+4\}$ hold the two non-$c$ colours, one each. The condition -$f_{i_k+3} = f_{i_k+4}$ forces $(i_k+3, i_k+4)$ to be either $(p, p+1)$ or -$(p+1, p+2)$ --- the two consecutive pairs inside the block --- and -correspondingly $i_k + 1 \in \{p+3, p+4\}$, \emph{outside} the block. So -$f_{i_k+1}$ is not $c$, whereas $f_{i_k+3} = c$, and hence -$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$. - -Combining the two cases, exactly one $t \in \{1, \dots, t^*\}$ --- namely -$t = 1$ --- has $\varphi_{t^*}(\mathrm{spike}_t) = -\varphi_{t^*}(\mathrm{merged}_t)$. -\end{proof} - -\begin{lemma}[All-distinct colouring exists on a 4-colourable graph] -\label{lem:all-distinct-exists} -Let $G$ be a $4$-colourable maximal planar graph of minimum degree $\geq 5$ -(equivalently, a maximal planar graph that is \emph{not} a minimal -counterexample to the Four Colour Theorem). Then there is an execution of -Algorithm~\ref{alg:iterated-reduction} on $G$ whose final colouring -$\varphi_{t^*}$ satisfies -$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ for -every $t \in \{1, \dots, t^*\}$. In particular, there exists a proper -$3$-edge-colouring of $H_{t^*}$ under which every spike-merged pair has -distinct colours. -\end{lemma} - -\begin{proof} -The argument mirrors Lemma~\ref{lem:exactly-one-match}, but extends a -colouring \emph{downward} from $G'$ rather than carrying one forward from -$H_1$. - -Since $G$ is $4$-colourable, by Tait's theorem -$G' = \mathrm{dual}(G)$ admits a proper $3$-edge-colouring $\xi$. Apply -Lemma~\ref{lem:pentagonal-externals} to $\xi$ at the pentagonal face $F_v$ -selected in step~(1): the external vector $f = (f_0, \dots, f_4)$ at $F_v$ -under $\xi$ has the $(3,1,1)$ cyclic-consecutive shape, with a block of -three consecutive positions $\{p, p+1, p+2\}$ (mod $5$) holding a common -colour $c$, and the remaining two positions $\{p+3, p+4\}$ holding the two -non-$c$ colours, one each. The algorithm's choice of $i_1$ forces -$\{i_1+3, i_1+4\}$ inside the $c$-block (so the chord is consistently -coloured) and the three positions $\{i_1, i_1+1, i_1+2\}$ pairwise distinct; -in particular $i_1+1$ lies \emph{outside} the $c$-block. - -Choose $\varphi_1$ to be the proper $3$-edge-colouring of $H_1$ that agrees -with $\xi$ on every surviving edge and assigns each new edge at $A_j$ the -unique third colour at $A_j$. Then -$\varphi_1(\mathrm{spike}_1) = f_{i_1+1}$, a value not equal to $c$, while -$\varphi_1(\mathrm{merged}_1) = f_{i_1+3} = c$, so -$\varphi_1(\mathrm{spike}_1) \neq \varphi_1(\mathrm{merged}_1)$. - -The same argument repeats at every step $k \geq 2$: the external vector at -the chosen pentagonal face under $\varphi_{k-1}$ has the $(3,1,1)$ -cyclic-consecutive shape (Lemma~\ref{lem:pentagonal-externals}), the -algorithm's index choice $i_k$ puts $i_k+3, i_k+4$ inside the colour block -and $i_k+1$ outside, and step~(3d) thus assigns -$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$. The -algorithm preserves these colours through every later step, so -$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ for -every $t \in \{1, \dots, t^*\}$. -\end{proof} - -\begin{conjecture} -\label{conj:face-monochromatic-pair-on-merged-kempe-cycle} -Let $G$ be a minimal counterexample to the Four Colour Theorem, and let -$\widehat{G}'_{v,i}$ be a reduced dual of $G' = \mathrm{dual}(G)$. Then for -every proper $3$-edge-colouring $\varphi$ of $\widehat{G}'_{v,i}$ there exist -a face $F$ of $\widehat{G}'_{v,i}$ and two distinct edges -$e_1, e_2 \in \partial F$, with neither $e_1$ nor $e_2$ equal to the merged -edge, such that -\begin{enumerate} - \item $\varphi(e_1) = \varphi(e_2)$, - \item $e_1$, $e_2$, and the merged edge all lie on a common - $\{a, b\}$-Kempe cycle of $\varphi$, and - \item exactly one edge of $\partial F$ lies between $e_1$ and $e_2$ along - one of the two arcs of $\partial F$; equivalently, subdividing $e_1$ - and $e_2$ by new vertices $X_1, X_2$ and joining them by a new edge - $X_1 X_2$ inside $F$ creates a new face bounded by exactly $4$ - edges (the new edge, the two subdivision halves adjacent to it, and - the single $\partial F$-edge between $e_1$ and $e_2$). -\end{enumerate} -\end{conjecture} - -\begin{remark} -\label{rem:conj-3-6-empirical} -The conjecture cannot be tested on actual minimal counterexamples (none exist -by the Four Colour Theorem), but its conclusion is checkable on the -structural surrogates: proper $3$-edge-colourings of reduced duals that -satisfy both the chord-apex condition (Lemma~\ref{lem:chord-apex}) and the -Kempe-cycle conditions (Lemma~\ref{lem:kempe-spike}), since a counterexample's -reduced dual is forced to admit such colourings under any proper colouring. -For every min-degree-$5$ triangulation $G$ with $|V(G)| \leq 21$, every -pentagonal face $F$ of $G'$, and every reduction index -$i \in \{0,\dots,4\}$, we enumerated all such colourings and tested the -three clauses of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} -(see \texttt{experiments/check\_conj\_face\_kempe\_scaled.py}); $n = 22$ -ran past a $1800$\,s budget after $641{,}700$ colourings (all pass), but -did not finish the full set of $651$ triangulations: -\begin{center} -\small -\renewcommand{\arraystretch}{1.15} -\begin{tabular}{r|r|r|r|l} -$n$ & \#tri & \#col.\ tested & \#sat.\ & status \\ -\hline -$12$ & $1$ & $0$ & --- & vacuous (icosahedron) \\ -$13$ & $0$ & --- & --- & no min-deg-$5$ tri \\ -$14$ & $1$ & $216$ & $216$ & all pass \\ -$15$ & $1$ & $0$ & --- & vacuous \\ -$16$ & $3$ & $864$ & $864$ & all pass \\ -$17$ & $4$ & $4{,}650$ & $4{,}650$ & all pass \\ -$18$ & $12$ & $8{,}070$ & $8{,}070$ & all pass \\ -$19$ & $23$ & $21{,}138$ & $21{,}138$ & all pass \\ -$20$ & $73$ & $107{,}874$ & $107{,}874$ & all pass \\ -$21$ & $192$ & $392{,}370$ & $392{,}370$ & all pass \\ -$22$ (part.) & $651$ & $641{,}700$ & $641{,}700$ & timeout \\ -\hline -total ($n \le 21$) & $311$ & $535{,}182$ & $535{,}182$ & \\ -\end{tabular} -\end{center} -\noindent The vacuous rows ($n = 12, 15$) are those where the relevant -reduced duals admit no proper $3$-edge-colouring satisfying chord-apex + -both Kempe-cycle conditions, so the conjecture has no content there. On -every $(G, F, i, \varphi)$ with content, all three clauses of the -conjecture hold simultaneously. -\end{remark} - -The next definition records 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 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 Section~\ref{sec:toward-4ct} below, where we formulate a sufficient condition for the Four Colour Theorem. @@ -788,39 +518,110 @@ by the contraction).} \label{fig:thm-cubic-contraction-4face} \end{figure} -\section{The Four Colour Theorem from a strengthened conjecture} +\section{The face-monochromatic-pair conjecture and the Four Colour Theorem} \label{sec:toward-4ct} -The next conjecture strengthens -Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} by adding -a clause that arranges the new $4$-edge face $f_n$ to satisfy the hypotheses -of Theorem~\ref{thm:cubic-contraction-4face}. The strengthening, if true, -would imply the Four Colour Theorem. +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}. -\begin{conjecture}[Strengthening of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}] +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] +\label{conj:face-monochromatic-pair-on-merged-kempe-cycle} +Let $G$ be a minimal counterexample to the Four Colour Theorem, and let +$\widehat{G}'_{v,i}$ be a reduced dual of $G' = \mathrm{dual}(G)$. Then +for every proper $3$-edge-colouring $\varphi$ of $\widehat{G}'_{v,i}$ +there exist a face $F$ of $\widehat{G}'_{v,i}$ and two distinct edges +$e_1, e_2 \in \partial F$, with neither $e_1$ nor $e_2$ equal to the +merged edge, such that: +\begin{enumerate} + \item $\varphi(e_1) = \varphi(e_2)$. Write + $a := \varphi(e_1) = \varphi(e_2)$. + \item $e_1$, $e_2$, and the merged edge all lie on a common + $\{a, b\}$-Kempe cycle of $\varphi$, for some colour $b \neq a$. + \item Exactly one edge of $\partial F$ lies between $e_1$ and $e_2$ + along one of the two arcs of $\partial F$. Equivalently, + subdividing $e_1, e_2$ by new vertices $X_1, X_2$ and joining + them by a new edge $X_1 X_2$ inside $F$ creates a new face $f_n$ + bounded by exactly $4$ edges (the new edge $X_1 X_2$, the two + subdivision halves adjacent to it, and the single + $\partial F$-edge between $e_1$ and $e_2$). +\end{enumerate} +\end{conjecture} + +\begin{remark} +\label{rem:conj-3-6-empirical} +\sloppy +The conjecture cannot be tested on actual minimal counterexamples (none +exist by the Four Colour Theorem), but its conclusion is checkable on the +structural surrogates: proper $3$-edge-colourings of reduced duals that +satisfy both the chord-apex condition (Lemma~\ref{lem:chord-apex}) and +the Kempe-cycle conditions (Lemma~\ref{lem:kempe-spike}), since a minimal +counterexample's reduced dual is forced to admit such colourings. For +every min-degree-$5$ triangulation $G$ with $|V(G)| \leq 21$, every +pentagonal face $F$ of $G'$, and every reduction index +$i \in \{0,\dots,4\}$, we enumerated all such colourings and verified the +three clauses of +Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} (see +\texttt{experiments/check\_conj\_face\_kempe\_scaled.py}); $n = 22$ ran +past a $1800$\,s budget after $641{,}700$ colourings (all pass) without +finishing the full set of $651$ triangulations. +\begin{center} +\small +\renewcommand{\arraystretch}{1.15} +\begin{tabular}{r|r|r|r|l} +$n$ & \#tri & \#col.\ tested & \#sat. & status \\ +\hline +$12$ & $1$ & $0$ & --- & vacuous (icosahedron) \\ +$13$ & $0$ & --- & --- & no min-deg-$5$ tri \\ +$14$ & $1$ & $216$ & $216$ & all pass \\ +$15$ & $1$ & $0$ & --- & vacuous \\ +$16$ & $3$ & $864$ & $864$ & all pass \\ +$17$ & $4$ & $4{,}650$ & $4{,}650$ & all pass \\ +$18$ & $12$ & $8{,}070$ & $8{,}070$ & all pass \\ +$19$ & $23$ & $21{,}138$ & $21{,}138$ & all pass \\ +$20$ & $73$ & $107{,}874$ & $107{,}874$ & all pass \\ +$21$ & $192$ & $392{,}370$ & $392{,}370$ & all pass \\ +$22$ (part.) & $651$ & $641{,}700$ & $641{,}700$ & timeout \\ +\hline +total ($n \le 21$) & $311$ & $535{,}182$ & $535{,}182$ & \\ +\end{tabular} +\end{center} +\noindent The vacuous rows ($n = 12, 15$) are those where the relevant +reduced duals admit no chord-apex+Kempe colourings, so the conjecture +has no content there. +\end{remark} + +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}. + +\begin{conjecture}[Strengthening of + Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}] \label{conj:face-monochromatic-pair-strengthened} Let $G$, $\widehat{G}'_{v,i}$, $\varphi$ be as in Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}. Then -there exist $F$, $e_1$, $e_2$ satisfying clauses (1)--(3) of that -conjecture, and the following additional clause holds. - -Let $X_1, X_2$ be the new vertices subdividing $e_1, e_2$, joined by a new -edge $X_1 X_2$ inside $F$; write $\widehat{G}'^{+}$ for the resulting -modified graph (which has $|V(\widehat{G}'_{v,i})|+2$ vertices and -$|E(\widehat{G}'_{v,i})|+3$ edges, is again cubic and plane, and admits a -proper $3$-edge-colouring). Let $\varphi'$ be the proper -$3$-edge-colouring of $\widehat{G}'^{+}$ obtained from $\varphi$ by -swapping the two colours along the (subdivided) $\{a, b\}$-Kempe cycle of -clause~(2) and assigning the new edge $X_1 X_2$ the remaining (third) -colour. In particular $\varphi'$ agrees with $\varphi$ on every edge of -$\widehat{G}'_{v,i}$ outside that Kempe cycle, and at $X_1$ and $X_2$ the -two subdivision halves take the colours $\{a, b\}$ in the order forced by -propriety. Write $a := \varphi(e_1) = \varphi(e_2)$, -$c := \varphi'(X_1 X_2)$, and let $b$ be the third colour. Let $f_n$ be -the new $4$-edge face of $\widehat{G}'^{+}$ incident to $X_1 X_2$. Then: +there exist $F$, $e_1$, $e_2$ satisfying clauses~(1)--(3) of that +conjecture, together with the following additional clause. \begin{enumerate} \setcounter{enumi}{3} - \item either + \item Let $\widehat{G}'^{+}$ be the modified graph obtained from + $\widehat{G}'_{v,i}$ by the modification of clause~(3), and let + $\varphi'$ be the proper $3$-edge-colouring of $\widehat{G}'^{+}$ + obtained from $\varphi$ by swapping the two colours along the + (subdivided) $\{a, b\}$-Kempe cycle of clause~(2) and assigning + the new edge $X_1 X_2$ the remaining (third) colour $c$. + (Equivalently: $\varphi'$ agrees with $\varphi$ on every edge of + $\widehat{G}'_{v,i}$ outside that Kempe cycle, and at $X_1, X_2$ + the two subdivision halves take the colours $\{a, b\}$ in the + order forced by propriety.) Then either \begin{enumerate} \item[(i)] $\partial f_n$ uses all three colours under $\varphi'$, or @@ -836,30 +637,29 @@ the new $4$-edge face of $\widehat{G}'^{+}$ incident to $X_1 X_2$. Then: \sloppy The strengthened conjecture was tested on the same chord-apex+Kempe colourings as Remark~\ref{rem:conj-3-6-empirical}; for each colouring we -sought any Conjecture-3.6-witness $(F, e_1, e_2)$ whose accompanying -$f_n$ satisfies clause~(4) (see +sought any +Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}-witness +$(F, e_1, e_2)$ whose accompanying $f_n$ satisfies clause~(4) (see \texttt{experiments/check\_conj\_3\_8\_scaled.py}): \begin{center} \small \renewcommand{\arraystretch}{1.15} \begin{tabular}{r|r|r|r|l} -$n$ & \#tri & \#col.\ tested & \#sat.\ & status \\ +$n$ & \#tri & \#col.\ tested & \#sat. & status \\ \hline -$12$ & $1$ & $0$ & --- & vacuous \\ -$13$ & $0$ & --- & --- & no min-deg-$5$ tri \\ -$14$ & $1$ & $216$ & $216$ & all pass \\ -$15$ & $1$ & $0$ & --- & vacuous \\ -$16$ & $3$ & $864$ & $864$ & all pass \\ -$17$ & $4$ & $4{,}650$ & $4{,}650$ & all pass \\ -$18$ & $12$ & $8{,}070$ & $8{,}070$ & all pass \\ +$14$ & $1$ & $216$ & $216$ & all pass \\ +$16$ & $3$ & $864$ & $864$ & all pass \\ +$17$ & $4$ & $4{,}650$ & $4{,}650$ & all pass \\ +$18$ & $12$ & $8{,}070$ & $8{,}070$ & all pass \\ \hline -total & $23$ & $13{,}800$ & $13{,}800$ & \\ +total ($n \le 18$) & $20$ & $13{,}800$ & $13{,}800$ & \\ \end{tabular} \end{center} -\noindent A subtlety: only about half of the Conjecture-3.6-witnesses -individually satisfy clause (4) on each colouring, but in every case some -witness does. The conjecture is therefore an existential statement at the -witness level, not a property of every witness. +\noindent A subtlety: only about half of the +Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}-witnesses +individually satisfy clause~(4) on each colouring, but in every case +\emph{some} witness does. Clause~(4) is therefore an existential statement +at the witness level, not a property of every witness. \end{remark} \begin{remark}[The implication to the Four Colour Theorem]