\documentclass[11pt]{article}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{graphicx}
\usepackage{geometry}
\usepackage{booktabs}
\usepackage{tikz}
\usetikzlibrary{backgrounds}
\geometry{margin=1in}

\title{Birkhoff's condition: minimum 4CT counterexamples are
internally $6$-connected}
\author{}
\date{}

\newtheorem*{defn}{Definition}
\newtheorem*{thm}{Theorem}
\newtheorem*{lem}{Lemma}
\newtheorem*{rem}{Remark}

\begin{document}
\maketitle

\section*{The condition}

\begin{defn}[Internally $6$-connected]
A planar triangulation $G$ is \emph{internally $6$-connected} if
every vertex cut of $G$ of size $\le 5$ either fails to separate
$G$, or is a $5$-cut whose two sides have one side equal to a
single vertex.

Equivalently: $G$ has no separating triangle (3-cycle), no
separating quadrilateral (4-cycle), and any separating pentagon
(5-cycle) isolates exactly one vertex on one side.
\end{defn}

\begin{thm}[Birkhoff 1913]
If a minimum $4$-colour counterexample (= minimum planar
triangulation requiring more than $4$ colours for a proper vertex
colouring) exists, it must be internally $6$-connected.
\end{thm}

The idea behind the proof: if $G$ has a separating $k$-cycle for
$k \in \{3, 4, 5\}$ with $\ge 2$ vertices on each side, one can
$4$-colour each side independently and patch the colourings along
the cycle, contradicting minimality.  Only the $5$-cycle isolating
$1$ vertex is irreducible by this argument.

\section*{Cases at a glance}

\begin{center}
\begin{tikzpicture}[scale=1.1]
  \node[anchor=west] at (0, 4.3) {\textbf{Internally $6$-connected $=$ all four below:}};
  % All status labels right-aligned at the same column (x = 11), well
  % clear of the longest bullet text.
  \node[anchor=west] at (0, 3.6) {\textbullet\, no separating $3$-cycle};
  \node[red, anchor=east] at (11, 3.6) {FORBIDDEN};
  \node[anchor=west] at (0, 2.9) {\textbullet\, no separating $4$-cycle};
  \node[red, anchor=east] at (11, 2.9) {FORBIDDEN};
  \node[anchor=west] at (0, 2.2) {\textbullet\, no separating $5$-cycle isolating $\ge 2$ on either side};
  \node[red, anchor=east] at (11, 2.2) {FORBIDDEN};
  \node[anchor=west] at (0, 1.5) {\textbullet\, separating $5$-cycle isolating $1$ vertex};
  \node[green!50!black, anchor=east] at (11, 1.5) {ALLOWED};
  % Schematic: a 5-cycle with 1 isolated vertex on one side --- placed
  % below the bullet list so it doesn't collide with the case labels.
  \begin{scope}[shift={(5.5, -0.6)}, scale=0.55]
    \node[circle, fill=red!80!black, inner sep=2pt] (c) at (0, 0) {};
    \foreach \i in {0,...,4} {
      \pgfmathsetmacro{\ang}{72*\i+90}
      \node[circle, fill=blue!80!black, inner sep=1.8pt] (n\i) at (\ang:1.4) {};
      \draw[blue, thick] (c) -- (n\i);
    }
    \foreach \i in {0,...,4} {
      \pgfmathtruncatemacro{\j}{mod(\i+1,5)}
      \draw[blue, very thick] (n\i) -- (n\j);
    }
    \node[red] at (0, -1.95) {\small allowed case};
  \end{scope}
\end{tikzpicture}
\end{center}

The right-hand schematic shows the only permitted case: a vertex
(red) surrounded by its $5$ neighbours (blue) which form a $5$-cycle.
Removing the $5$ blue vertices isolates the red one.  This is what
the next section's picture shows in the icosahedron.

\section*{Icosahedron: the smallest example}

The icosahedral graph (the $1$-skeleton of the regular icosahedron)
has $12$ vertices, all of degree $5$, and is a planar triangulation.
Every vertex's $5$ neighbours form a $5$-cycle (the ``link'' of the
vertex); removing them isolates the vertex.  This is the only kind
of small cut: the icosahedron is internally $6$-connected.

\begin{center}
\includegraphics[width=\textwidth]{icosahedron_internally_6_connected.pdf}
\end{center}

On the left, the icosahedron's planar (Schlegel) embedding: the red
vertex (here vertex $0$) is removed from the graph by the $5$-cut
consisting of its $5$ blue neighbours $\{1, 5, 7, 8, 11\}$.  The
blue $5$-cycle is the separator; on one side is the isolated red
vertex, on the other are the remaining $6$ vertices.  This is the
allowed Birkhoff configuration.

\section*{Internally $6$-connected vs.\ cyclic edge connectivity}

Birkhoff's condition rules out small \emph{cuts} but does not
force any specific separating \emph{cycle} to exist.  In the cubic
dual $G^*$, the dictionary is:
\begin{itemize}
\item $k$-vertex cut in $G$ $\leftrightarrow$ $k$-edge cut in $G^*$.
\item separating $k$-cycle in $G$ (with $\ge 2$ vertices on each
      side) $\leftrightarrow$ $k$-edge cut in $G^*$ separating $G^*$
      into two pieces \emph{each containing a cycle}
      (= \emph{cyclic} edge cut).
\end{itemize}

So $G$ internally $6$-connected $\iff$ $G^*$ has \emph{cyclic edge
connectivity} $\ge 6$.  Whether it is \emph{exactly} $6$ (= some
separating $6$-cycle in $G$ exists with both sides $\ge 2$
vertices) is an additional question.

\paragraph{Hidden assumption in the cut-tire framework.}  Our
chain-DP framework
(\texttt{chain\_half\_analysis.tex}, \texttt{boundary\_cut\_tire.tex})
operates on $6$-edge cuts of the cubic dual.  It therefore has
nontrivial content on $G$ only when $G^*$ has cyclic edge
connectivity \emph{exactly} $6$ --- i.e.\ when $G$ has a
separating $6$-cycle with $\ge 2$ vertices on each side.  Birkhoff
gives ``$\ge 6$''; we need ``$= 6$''.

This is a real \emph{a priori} restriction: if a minimum $4$CT
counterexample turned out to have $G^*$ with cyclic edge
connectivity $\ge 7$ (= no separating $6$-cycle in $G$), our
framework would be empty on it.

\paragraph{Empirically.}  All graphs in the test suite
(icosahedron / dodecahedron, pentakis dodecahedron / Buckyball,
Holton--McKay $\#0$ through $\#5$) have many $6$-edge cuts in
their cubic duals --- i.e.\ all known internally $6$-connected
triangulations of moderate size have plenty of separating
$6$-cycles.  Whether a hypothetical minimum $4$CT counterexample
\emph{must} have one is a structural question discussed in the
next note.

\section*{Why this matters for the framework}

For our cut-tire chain DP framework, we test on graphs whose primal
triangulation is internally $6$-connected:
\begin{itemize}
\item \textbf{Icosahedron} ($V = 12$): smallest example.  Its
      cubic dual = dodecahedron ($V = 20$).
\item \textbf{Pentakis dodecahedron} ($V = 32$): icosahedron with
      each face subdivided.  Cubic dual = truncated icosahedron =
      ``Buckminsterfullerene'' ($V = 60$).
\item \textbf{Holton--McKay graphs} ($V = 21$ primal triangulation,
      $V = 38$ cubic dual): the smallest non-Hamiltonian
      internally-$6$-connected cubic plane graphs, candidates for
      a minimum counterexample in Tait's reduction even though all
      are $3$-edge-colourable.
\end{itemize}

If our framework's claims hold for all internally $6$-connected
triangulations, then a minimum $4$CT counterexample (if it existed)
would be in the framework's domain --- and any structural obstruction
the framework finds would refute the counterexample's existence.

\section*{Sanity check}

Sage verification (in
\texttt{experiments/draw\_internally\_6\_connected.py}):
\begin{verbatim}
Vertex 0 has 5 neighbors: [1, 5, 7, 8, 11]
Induced subgraph on neighbors: 5 edges, is_cycle=True
After removing the 5 neighbors: 2 components, sizes=[1, 6]
\end{verbatim}

So vertex $0$'s neighbourhood is indeed a $5$-cycle, removing it
isolates vertex $0$ from the other $6$ vertices.  By symmetry the
same holds at every vertex of the icosahedron.

\end{document}
