%% filename: amsart-template.tex
%% version: 1.1
%% date: 2014/07/24
%%
%% American Mathematical Society
%% Technical Support
%% Publications Technical Group
%% 201 Charles Street
%% Providence, RI 02904
%% USA
%% tel: (401) 455-4080
%%      (800) 321-4267 (USA and Canada only)
%% fax: (401) 331-3842
%% email: tech-support@ams.org
%%
%% Copyright 2008-2010, 2014 American Mathematical Society.
%%
%% This work may be distributed and/or modified under the
%% conditions of the LaTeX Project Public License, either version 1.3c
%% of this license or (at your option) any later version.
%% The latest version of this license is in
%%   http://www.latex-project.org/lppl.txt
%% and version 1.3c or later is part of all distributions of LaTeX
%% version 2005/12/01 or later.
%%
%% This work has the LPPL maintenance status `maintained'.
%%
%% The Current Maintainer of this work is the American Mathematical
%% Society.
%%
%% ====================================================================

%     AMS-LaTeX v.2 template for use with amsart
%
%     Remove any commented or uncommented macros you do not use.

\documentclass{amsart}

\usepackage{hyperref}
\usepackage{enumitem}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{xca}[theorem]{Exercise}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{question}[theorem]{Question}
\newtheorem{observation}[theorem]{Observation}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\numberwithin{equation}{section}

\begin{document}

\title{Level Resolutions of Maximal Planar Graphs}

%    Remove any unused author tags.

%    author one information
\author{Eric Bauerfeld}
\address{}
\curraddr{}
\email{}
\thanks{}


\subjclass[2010]{Primary }

\keywords{}

\date{}

\dedicatory{}

\begin{abstract}
We propose a structural reformulation of the four color theorem in terms
of \emph{level resolutions} of maximal planar graphs. A level structure on a
plane graph $G$ is defined by BFS from a chosen level source (either a face
or a degree-3 vertex), partitioning vertices into levels. A triangulation
$G'$ on the same vertex set is a \emph{level resolution} of $G$ from this
source if the subgraphs of $G'$ induced by even- and odd-level vertices are
both bipartite. By construction, any level resolution admits an explicit
4-coloring obtained by 2-coloring each parity subgraph independently. The
structural foundation of this approach is that each level subgraph $L_k$
of $G$ is outerplanar, and outerplanar graphs are 3-chromatic; the level-resolution
problem is precisely to flip edges of $G$ to reduce each $L_k$ from
chromatic number $3$ to $2$. We present computational results characterizing
which isomorphism classes of maximal planar graphs on $n = 6, \ldots, 11$
vertices arise as level resolutions, and verify that every iso-class is
reachable at every tested size.
\end{abstract}

\maketitle

\section{Introduction}

The four color theorem (4CT) asserts that every planar graph is 4-colorable.
Equivalently, every maximal planar graph (triangulation) is 4-colorable.
The Appel--Haken proof~\cite{appelhaken} and subsequent
Robertson--Sanders--Seymour--Thomas refinement~\cite{rsst} rely on
discharging arguments and computer-verified reducible configurations.
Human-readable proofs remain elusive.

We propose a different structural approach. Given a plane triangulation $G$
and a choice of \emph{level source}, BFS from the source partitions the
vertices into levels. A triangulation $G'$ on the same vertex set is a
\emph{level resolution} of $G$ if, when its vertices are labelled by the
parity of their $G$-levels, the subgraph of $G'$ induced by even-parity
vertices and the subgraph induced by odd-parity vertices are both
bipartite. The 4-coloring of $G'$ then follows by definition: 2-color each
parity subgraph and identify the four resulting classes with four distinct
colors.

The remaining question is when level resolutions exist. We conjecture:
\begin{enumerate}[label=(\roman*)]
\item every plane triangulation $G'$ is a level resolution of some
      plane triangulation $G$ via some level source; or, in a restricted
      form,
\item every plane triangulation of minimum degree at least 4 is a level
      resolution of some plane triangulation.
\end{enumerate}

This paper formalizes the definitions and presents computational evidence
bearing on (i)--(ii) for small vertex counts.

\section{Definitions}

Throughout, $G = (V, E)$ is a plane maximal planar graph (a triangulation)
with a fixed planar embedding $\Pi_G$. We write $|V| = n$, so $|E| = 3n - 6$
and $G$ has $2n - 4$ triangular faces.

\begin{definition}[Level source]
A \emph{level source} of $G$ is either:
\begin{itemize}
\item a face $F$ of $G$ (all vertices of $F$ are level-0 sources), or
\item a vertex $v$ of degree 3 (the singleton $\{v\}$ is a level-0 source).
\end{itemize}
\end{definition}

\begin{definition}[Levels]
Given a level source $S \subseteq V$, the \emph{level} of $v \in V$ is
$\ell_G(v) = \mathrm{dist}_G(v, S)$, the graph distance from $v$ to the nearest
source vertex.
\end{definition}

\begin{definition}[Parity subgraph]
Let $G$ be a triangulation with level source $S$, and let $G'$ be a triangulation
on the same vertex set as $G$. The \emph{even parity subgraph} $E_{G,S}(G')$ is
the subgraph of $G'$ induced by $\{v \in V : \ell_G(v) \equiv 0 \pmod 2\}$. The
\emph{odd parity subgraph} is defined analogously for odd $\ell_G$.
\end{definition}

\begin{definition}[Level resolution]
\label{def:resolution}
A triangulation $G'$ on the same vertex set as $G$ is a \emph{level resolution}
of $G$ from level source $S$ if both the even and odd parity subgraphs
$E_{G,S}(G')$ and $O_{G,S}(G')$ are bipartite.
\end{definition}

By construction, when $G'$ is a level resolution of $G$ via $S$, an explicit
proper 4-coloring of $G'$ is obtained by 2-coloring each parity subgraph
independently (e.g., via BFS) and assigning the four resulting classes to
distinct colors: even vertices receive red/blue, odd vertices receive
yellow/green. The edges of $G'$ partition into (i) edges within a parity
subgraph, properly colored by the bipartition of that subgraph; and
(ii) edges between an even-parity and odd-parity vertex, which connect
disjoint color sets and so are properly colored.

\section{Structural foundation: outerplanarity of level subgraphs}
\label{sec:outerplanar}

For each integer $k \geq 0$ and each $(G, S)$, write $L_k$ for the subgraph
of $G$ induced by the level-$k$ vertices.

\begin{theorem}
\label{thm:outerplanar}
For every plane triangulation $G$ and every level source $S$ of $G$, each
level subgraph $L_k$ is outerplanar.
\end{theorem}

\begin{proof}
For $k = 0$, $L_0$ is either a single vertex (when $S$ is a degree-3
vertex) or the triangle bounding the source face (when $S$ is a face),
both outerplanar. Fix $k \geq 1$ and suppose, for contradiction, that
$L_k$ is not outerplanar.

Let $D_k$ denote the planar drawing of $L_k$ inherited from $\Pi_G$:
that is, the set of points and curves in the plane representing the
vertices and edges of $L_k$ exactly as they appear in the embedding
$\Pi_G$. Since $L_k$ is not outerplanar, no face of $D_k$ has every
vertex of $L_k$ on its boundary.

Let $F^\ast$ be the face of $D_k$ containing the source: when
$S = \{v\}$, the face containing the point $v$; when $S$ is a face $F$
of $G$, the face containing the open region of $F$ together with its
three bounding vertices. The latter is well defined because each
vertex of $F$ lies at level $0$ (hence is not a vertex of $L_k$) and
each edge of $F$ joins two level-$0$ vertices (hence is not an edge of
$L_k$), so $F$ and its boundary lie in a single component of
$\mathbb{R}^2 \setminus D_k$. By assumption there exists $u \in L_k$
with $u \notin \partial F^\ast$.

Choose a BFS path $P : v_0, v_1, \ldots, v_k = u$ with $v_0 \in S$ and
$v_i \in L_i$. For $0 \leq i \leq k - 1$, $v_i$ lies in $L_i$ and so is
not a vertex of $L_k$; for $1 \leq i \leq k$, the edge $v_{i-1} v_i$
joins $L_{i-1}$ to $L_i$ and so is not an edge of $L_k$. Hence, viewed
as a curve in the plane, $P$ meets the drawing $D_k$ only at its
endpoint $u$.

The complement $\mathbb{R}^2 \setminus D_k$ is open, and $P \setminus
\{u\}$ is its continuous image of a connected set, hence lies in a
single face of $D_k$. Since $v_0 \in F^\ast$, in fact
$P \setminus \{u\} \subseteq F^\ast$, so $u \in \overline{F^\ast}$ and
therefore $u \in \partial F^\ast$, contradicting the choice of $u$.
\end{proof}

The combinatorial significance of Theorem~\ref{thm:outerplanar} is
that outerplanar graphs are $3$-chromatic~\cite{chartrand}: their chromatic
number is at most $3$. Hence each $L_k$ admits an independent 3-coloring,
giving an immediate (but suboptimal) coloring of $G$ using at most
$3 \cdot \mathrm{depth}(G, S)$ colors when levels are colored
independently. To recover a $4$-coloring of $G'$ via the
parity-2-coloring strategy, what is required is to reduce each $L_k$'s
chromatic number from $3$ to $2$, equivalently to remove every odd cycle
from each $L_k$:

\begin{proposition}
\label{prop:bipartite-suffices}
If $G'$ is a triangulation on the same vertex set as $G$ such that for
every $k$, the subgraph of $G'$ induced by the level-$k$ vertices of
$(G, S)$ is bipartite, and $G'$ contains no edge between vertices at
$G$-levels of equal parity and differing by exactly $2$, then $G'$ is a
level resolution of $G$ via $S$.
\end{proposition}

\begin{proof}
The even parity subgraph $E_{G,S}(G')$ is the disjoint union of the
even-level subgraphs of $G'$ (since by hypothesis no edge of $G'$ joins
two even levels), each of which is bipartite. A disjoint union of
bipartite graphs is bipartite. The same argument applies to the odd
parity subgraph.
\end{proof}

This is the form of level resolution we seek to realize constructively:
flips applied to $G$ that break every odd cycle in every $L_k$ without
introducing cross-parity edges of distance~$2$.

\section{The four-color conjecture via level resolutions}

\begin{conjecture}[Resolution preimage]
\label{conj:preimage}
Every plane triangulation $G'$ on $n$ vertices is a level resolution of
some plane triangulation $G$ on $n$ vertices.
\end{conjecture}

If Conjecture~\ref{conj:preimage} holds, the 4-coloring of any triangulation
$G'$ follows from the definition: exhibit a level-resolution preimage $G$,
compute the BFS levels in $G$ from the witness source, and 4-color $G'$ via
the parity 2-coloring.

\section{Computational evidence}

We enumerated all non-isomorphic triangulations on $n \in \{6, \ldots, 11\}$
via vertex insertion followed by edge-flip closure (see
\texttt{triangulation\_gen.py} and the faster
\texttt{triangulation\_gen\_fast.py} for $n \geq 11$). For each isomorphism
class, we computed the full set of iso-classes reachable as level
resolutions across all valid level sources.

\subsection{Coverage at $n = 6, \ldots, 11$}

Table~\ref{tab:coverage} lists the resolution behavior for each iso-class.
A class $T_i$ is \emph{covered} if it appears as the resolution iso-class of
some triangulation.

\begin{table}[h]
\centering
\begin{tabular}{rrl}
\hline
$n$ & Iso-classes & Reachable as level resolutions \\
\hline
6  & 2    & all 2  \\
7  & 5    & all 5  \\
8  & 14   & all 14 \\
9  & 50   & all 50 \\
10 & 233  & all 233 \\
11 & 1249 & all 1249 \\
\hline
\end{tabular}
\caption{Iso-class coverage under the level-resolution definition.}
\label{tab:coverage}
\end{table}

\begin{observation}
\label{obs:preimage}
For every $n \in \{6, \ldots, 11\}$, every plane-triangulation iso-class on
$n$ vertices is a level resolution of some plane triangulation on the same
vertex set.
\end{observation}

\paragraph{Equivalence to 4-colorability.}
A 2-partition $V = V_0 \sqcup V_1$ for which both $G'[V_0]$ and $G'[V_1]$
are bipartite induces a proper 4-coloring of $G'$ (combine the bipartition
of $V_0$ into colors $\{R, B\}$ and that of $V_1$ into $\{Y, G\}$), and
conversely, any proper 4-coloring grouped pairwise produces such a
partition. Hence by Definition~\ref{def:resolution}, $G'$ is a level
resolution of some $(G, S)$ if and only if $G'$ admits a bipartite
2-partition of cardinality realizable as $(|V_e|, |V_o|)$ for some level
source. Surjectivity at a given $n$ is therefore equivalent to
$4$-colorability of every triangulation on $n$ vertices together with
realizability of the partition cardinality by some BFS. Our computational
verification of Observation~\ref{obs:preimage} does not invoke 4CT: we
enumerate vertex partitions directly and check bipartiteness of the
induced subgraphs.

\subsection{Surjectivity at $n = 12$: the icosahedron}

The icosahedron is the unique 5-regular triangulation on 12 vertices and a
natural test case at $n = 12$ since it has no degree-3 vertex (so the
$\mathrm{md}_4$ restriction is irrelevant) and high symmetry constrains the
achievable parity-cardinality splits to $(6, 6)$ from any source. We verify
directly that the icosahedron admits a bipartite 2-partition of cardinality
$(6, 6)$: with vertices labelled as in the standard icosahedral graph, the
partition $\{0, 1, 2, 3, 4, 7\} \mid \{5, 6, 8, 9, 10, 11\}$ has both
classes inducing bipartite subgraphs (each is a 6-cycle). By
Definition~\ref{def:resolution}, the icosahedron is therefore a level
resolution of some plane triangulation on 12 vertices.

\begin{observation}
\label{obs:icosa}
The icosahedron is a level resolution of some plane triangulation on 12
vertices.
\end{observation}

\subsection{Restatement of the resolution-preimage conjecture}

In light of Observations~\ref{obs:preimage} and~\ref{obs:icosa}, we
restate Conjecture~\ref{conj:preimage} more confidently:

\begin{conjecture}[$\mathrm{md}_4$ surjectivity]
\label{conj:md4}
For every $n \geq 6$, every minimum-degree-4 plane triangulation on $n$
vertices is a level resolution of some plane triangulation on $n$ vertices.
\end{conjecture}

By the equivalence noted in Section~3, this is equivalent to a $4$-coloring
statement: every minimum-degree-4 plane triangulation admits a proper
$4$-coloring whose color-class cardinalities, grouped pairwise, match some
BFS-level parity cardinality on the same vertex set. Since the
unrestricted preimage conjecture also appears to hold at every tested $n$,
the $\mathrm{md}_4$ restriction may be unnecessary; we retain it here as
the form most amenable to the constructive techniques explored in
Section~\ref{sec:flip-algorithm}.

\section{An edge-flip resolution algorithm}
\label{sec:flip-algorithm}

We describe an iterative edge-flip procedure aimed at producing, for a given
$(G, S)$, a triangulation $G'$ on the same vertex set whose simple level
cycles (with respect to the $G$-levels from $S$) are all even.

\subsection{Apex classification of $L_k$-edges}

Let $k \geq 1$. For each $uv \in E(L_k)$, the two triangles of $G$ bounding
$uv$ have third vertices $w, x$, called the \emph{apexes} of $uv$, with
$\ell_G(w), \ell_G(x) \in \{k-1, k, k+1\}$ by BFS. We call $uv$
\emph{intra-level} when $\ell_G(w) = \ell_G(x) = k$, and \emph{cross-level}
otherwise.

\begin{lemma}
\label{lem:bridge-apex}
If both apexes of $uv \in E(L_k)$ are at level $k - 1$, then $uv$ is a
bridge of $L_k$.
\end{lemma}

\begin{proof}[Proof sketch]
In a plane triangulation, the neighbors of $u$ in $G$ at level $\leq k - 1$
form a contiguous arc in the cyclic order around $u$. If both apexes $w, x$
of $uv$ lie at level $k - 1$ on opposite sides of $uv$, then $v$ lies in the
complementary cyclic arc, which contains no other level-$k$ neighbor of $u$.
The symmetric statement around $v$ gives that $u$ is $v$'s only level-$k$
neighbor in the corresponding arc, so $uv$ is a bridge of $L_k$.
\end{proof}

In particular every edge on a cycle of $L_k$ has at least one apex at level
$k$ or $k+1$.

\begin{proposition}
\label{prop:flip-target}
Flipping $uv \in E(L_k)$ with apexes $w, x$ replaces $uv$ with $wx$ in $G$.
The new edge $wx$ belongs to $L_k$ iff $\ell_G(w) = \ell_G(x) = k$, and to
$L_{k+1}$ iff $\ell_G(w) = \ell_G(x) = k + 1$; otherwise $wx$ is cross-parity
and lies in no level subgraph. In all cases $uv$ is removed from $L_k$.
\end{proposition}

\subsection{Facial depth and isolated faces}

\begin{definition}[Facial depth]
\label{def:facial-depth}
Let $L_k$ be drawn with the outerplanar embedding inherited from $\Pi_G$,
let $D$ be the dual graph of this drawing with the outer face removed, and
let $\mathcal{B}$ be the set of inner faces incident to at least two edges
of the outer face of $L_k$. The \emph{facial depth} of an inner face $F$ of
$L_k$ is
\[
  \mathrm{depth}(F) \;=\; \min_{F' \in \mathcal{B}} \mathrm{dist}_D(F, F'),
\]
with the convention $\mathrm{depth}(F) = \infty$ if no such $F'$ exists.
An inner face is \emph{isolated} if $\mathrm{depth}(F) \geq 1$.
\end{definition}

The seed set $\mathcal{B}$ consists of the inner faces that already have
two outer-face edges available as flip targets; Phase~2 below handles
these directly. Phase~1 uses facial depth as a potential to push isolated
odd faces toward $\mathcal{B}$.

A cycle that is \emph{tricky-everywhere}, meaning every edge is
intra-level, is necessarily isolated: an outer-face edge of $L_k$ has a
level-$(k-1)$ apex on its outer side and is therefore cross-level, so a
tricky-everywhere cycle shares no edge with the outer face. Hence the
tricky-everywhere cycles are a subset of the isolated odd cycles.

\subsection{Phase 1: interior faces}

\noindent\textbf{Procedure.} While some $L_k$ contains an odd simple cycle
whose corresponding inner face has facial depth $\geq 1$ and shares no
edge with the outer face, repeat:
\begin{enumerate}[label=(\arabic*)]
\item compute facial depths for all simple level cycles of $L_k$;
\item among interior odd faces (depth $\geq 1$, no outer-face edges) of
      maximum facial depth, pick one $C$; even-parity interior faces of
      depth $\geq 1$ may also be selected as $C$;
\item find the inner face $F'$ incident to $C$ of minimum facial depth,
      and flip the edge shared between $C$ and $F'$.
\end{enumerate}

The restriction to faces with no outer-face edge in step~(2) means that
every edge of $C$ borders another inner face, so a unique shared-edge
flip target exists for each neighbor $F'$. The depth-guided choice of
$F'$ in step~(3) progressively pushes the residual odd-face structure
toward the seed set $\mathcal{B}$ (depth~$0$). Even-face flips are
optional restructuring moves that expand the reachable configuration
space; the loop's termination is gated only by interior odd faces.

\subsection{Phase 2: outer-incident faces}

After Phase~1, every remaining odd simple cycle of $L_k$ shares at least
one edge with the outer face, whose apex pair includes a level-$(k-1)$
vertex and is therefore cross-level.

\noindent\textbf{Procedure.}
For each $L_k$:
\begin{itemize}
\item every odd simple cycle $C \subseteq L_k$ incident to the outer
face \emph{must} have exactly one of its outer-face edges flipped;
\item every even simple cycle of $L_k$ incident to the outer face
\emph{may} have at most one of its outer-face edges flipped (an optional
restructuring move).
\end{itemize}
For the source-face level ($k = 0$ with face source $S$), the $L_0$
source triangle is itself an odd cycle whose three edges all bound the
outer face; we treat $L_0$ uniformly with higher levels, with the option
of leaving the triangle intact when the resulting parity-subgraph
configuration on $G'$ permits.

Each flip is permitted even if the apex edge $wx$ already exists in $G$,
in which case $G'$ is a multigraph; this does not affect bipartiteness
of the parity subgraphs of $G'$, since a duplicated edge is bipartite-
equivalent to a single edge.

\subsection{Simple level resolutions}

\begin{definition}[Simple level resolution]
\label{def:simple-level-resolution}
A plane triangulation $G'$ is a \emph{simple level resolution} of a plane
triangulation $G$ if there exists a level source $S$ of $G$ such that
the algorithm of Sections~\ref{sec:flip-algorithm}--Phase~1 and~Phase~2
applied to $(G, S)$, under some sequence of optional-move choices,
produces $G'$ as a simple-graph triangulation whose parity subgraphs are
bipartite.
\end{definition}

\subsection{Empirical status}

\begin{observation}
\label{obs:empirical-lk-bipartite}
For every plane triangulation $G$ on $n \in \{9, 10, 11\}$ vertices, every
level source $S$, and every $k$ such that $L_k$ contains an odd simple
cycle, the algorithm produces a $G'$ whose corresponding $L_k$ is
bipartite (in the underlying simple-graph view). Across the $29640$ such
$(G, S, k)$ triples — $4645$ at $n \leq 10$ and $24995$ at $n = 11$ —
Phase~1 always terminates and Phase~2 always succeeds.
\end{observation}

\paragraph{Coverage test for Conjecture~\ref{conj:simple-md4}.} For each
$n \in \{6, \ldots, 11\}$ we enumerate all plane-triangulation iso-classes
on $n$ vertices. For each iso-class $G$, each level source $S$ of $G$,
and each branching choice within the algorithm — Phase~1 ties on which
deepest interior face and which lowest-depth neighbor to flip, Phase~2
choices of which outer-face edge to flip for each odd or even
outer-incident cycle (including the option to leave even cycles
untouched), and the option to skip the source-triangle break when $S$ is
a face — we run Phase~1 to termination and then Phase~2, recording the
algorithm's output $G'$ as a labelled simple graph. We check three
properties: (a) $G'$ is a triangulation (no multi-edge survived the
Phase~2 flips), (b) the parity subgraphs $E_{G, S}(G')$ and
$O_{G, S}(G')$ are both bipartite, and (c) the iso-class of $G'$.
Aggregating over all $(G, S, \text{branch-choices})$ triples yields the
set of iso-classes attainable as algorithm outputs satisfying (a)+(b);
we compare this set against the minimum-degree-$4$ iso-classes at each
$n$.

\begin{observation}
\label{obs:md4-simple-resolution}
For every $n \in \{6, 7, 8, 9, 10, 11\}$, every plane triangulation
iso-class on $n$ vertices with minimum degree at least $4$ is a simple
level resolution of some plane triangulation on $n$ vertices. Concretely,
the counts of minimum-degree-$4$ iso-classes — $1, 1, 2, 5, 12, 34$ at
$n = 6, \ldots, 11$ — are all reached by the algorithm with bipartite
parity subgraphs (Definition~\ref{def:simple-level-resolution}).
\end{observation}

\begin{conjecture}[Simple-resolution $\mathrm{md}_4$ surjectivity]
\label{conj:simple-md4}
For every $n \geq 6$, every minimum-degree-$4$ plane triangulation on $n$
vertices is a simple level resolution of some plane triangulation on $n$
vertices.
\end{conjecture}

The minimum-degree-$4$ restriction in Conjecture~\ref{conj:simple-md4} is
necessary: at $n = 8$, the unique iso-class with three degree-$3$
vertices is not reachable by the algorithm; at $n = 10$, two further
iso-classes with four degree-$3$ vertices and high-degree hubs fail to
appear among algorithm outputs.

\subsection{Towards a proof: a contraction--lift strategy}
\label{sec:contraction-lift}

We sketch an inductive strategy for Conjecture~\ref{conj:simple-md4}
that we have verified empirically at small $n$ and offer here as a
roadmap for further work.

Let $T$ be a plane triangulation with minimum degree at least $4$, and
let $v \in V(T)$ be a degree-$4$ vertex with cyclic neighbors
$a, b, c, d$ (in the cyclic order inherited from $T$'s planar
embedding). Removing $v$ from $T$ exposes the $4$-cycle $abcd$, which we
retriangulate by adding one of the two diagonals $(a, c)$ or $(b, d)$.
We call this operation \emph{contraction at $v$ along diagonal
$(a, c)$}, denoted $T_{v, (a, c)}$. The contraction is \emph{valid} when
the chosen diagonal is not already an edge of $T$.

\begin{lemma}[Good contraction]
\label{lem:good-contraction}
Let $T$ be a plane triangulation on $n \geq 7$ vertices with minimum
degree at least $4$. Then there exist a degree-$4$ vertex $v \in V(T)$,
with cyclic neighbors $a, b, c, d$, and an unordered pair
$\{a, c\}$ such that:
\begin{enumerate}
\item $(a, c) \not\in E(T)$;
\item $\deg_T(b) \geq 5$ and $\deg_T(d) \geq 5$.
\end{enumerate}
Under these conditions $T_{v, (a, c)}$ is a plane triangulation on
$n - 1$ vertices with minimum degree at least $4$.
\end{lemma}

The conditions of Lemma~\ref{lem:good-contraction} ensure that the
contraction is valid (1) and md$_4$-preserving (2): the only vertices
whose degree changes under $T \to T_{v, (a, c)}$ are $a, b, c, d$, with
$\deg(a)$ and $\deg(c)$ unchanged (each loses the edge to $v$ but gains
the edge from the diagonal), while $\deg(b)$ and $\deg(d)$ each decrease
by $1$.

The lemma is empirically true at $n = 7, \ldots, 11$ for every md$_4$
iso-class; we conjecture it holds for all $n \geq 7$. The $n = 6$ case
is excluded: the unique md$_4$ iso-class is the octahedron, in which
every vertex has all four cyclic neighbors at degree $4$ and so no
contraction preserves md$_4$. The octahedron is therefore the base case
of the proposed induction.

\begin{lemma}[Lift]
\label{lem:lift}
Let $T$ be a plane triangulation with minimum degree at least $4$, and
suppose Lemma~\ref{lem:good-contraction} applies via vertex $v$ and
diagonal $(a, c)$ with $T_{v, (a, c)}$ the resulting contraction. Let
$H$ be a plane triangulation on $V(T_{v, (a, c)}) = V(T) \setminus \{v\}$
and $S$ a level source of $H$ such that the algorithm of
Section~\ref{sec:flip-algorithm} applied to $(H, S)$ produces
$T_{v, (a, c)}$ as a labelled simple graph. Define the \emph{lift}
$G \;:=\; H[a, b, c, d, v]$ by:
\begin{itemize}
\item adding vertex $v$ to $V(H)$;
\item removing the edge $(a, c)$ from $E(H)$;
\item adding the four edges $(v, a), (v, b), (v, c), (v, d)$.
\end{itemize}
Then $G$ is a plane triangulation on $|V(T)|$ vertices, and the
algorithm of Section~\ref{sec:flip-algorithm} applied to $(G, S)$
produces $T$.
\end{lemma}

Lemma~\ref{lem:lift} requires that $(a, c) \in E(H)$ and that the two
triangles of $H$ bordering $(a, c)$ have boundary
$\{a, b, c, d\}$. When these conditions hold, the lift restores a
degree-$4$ vertex $v$ inserted into the quadrilateral $abcd$; when they
fail, the lift is undefined and a different labelled preimage $H$ must
be chosen.

\paragraph{Inductive scheme.}
Conjecture~\ref{conj:simple-md4} would follow from
Lemmas~\ref{lem:good-contraction} and~\ref{lem:lift} together with the
existence at each step of a labelled preimage $H$ satisfying the lift's
side conditions. The base case is the octahedron at $n = 6$, which is
empirically a simple level resolution
(Observation~\ref{obs:md4-simple-resolution}). The inductive step takes
an md$_4$ target $T$ on $n$ vertices, applies
Lemma~\ref{lem:good-contraction} to obtain an md$_4$ contraction
$T_{v, (a, c)}$ on $n - 1$ vertices, invokes the inductive hypothesis to
produce a labelled preimage $H$, and applies Lemma~\ref{lem:lift} to
lift $H$ to $G$ with $\mathrm{alg}(G, S) = T$.

We have verified the entire scheme by hand for the unique md$_4$
iso-class at $n = 7$: contraction at $v = 2$ along diagonal $(4, 3)$
yields the octahedron on six vertices labelled $\{0, 1, 3, 4, 5, 6\}$;
a labelled preimage $H$ exists with source $S = \{0, 1, 6\}$; lifting
along $(4, 3, v = 2)$ produces a triangulation $G$ on seven vertices on
which the algorithm with source $S$ recovers $T$ exactly. The principal
remaining work is a proof of Lemma~\ref{lem:good-contraction} for all
$n \geq 7$, a proof of Lemma~\ref{lem:lift} (which involves analysing
how the algorithm's depth-guided flips interact with the added vertex
$v$), and a guarantee that a label-faithful preimage $H$ always
exists.

\begin{question}
\label{q:terminate-all-n}
Does Phase~1 terminate for all $(G, S)$? Equivalently, is there an
explicit monovariant on $L_k$'s face structure that strictly decreases
on every Phase~1 flip?
\end{question}

\section{Discussion and open questions}

The computational results suggest the following:

\begin{enumerate}
\item Conjecture~\ref{conj:preimage} (resolution preimage) holds at every
      tested size: all iso-classes on $n \in \{6, \ldots, 11\}$ vertices
      arise as level resolutions, and the icosahedron does at $n = 12$
      (Observations~\ref{obs:preimage} and~\ref{obs:icosa}).
\item Each level subgraph $L_k$ of $G$ is outerplanar
      (Theorem~\ref{thm:outerplanar}), so each $L_k$ is 3-chromatic
      classically and independently of 4CT. The level-resolution problem
      reduces to flipping edges of $G$ so that each $L_k$'s chromatic
      number drops from $3$ to $2$, while avoiding creation of $G$-level-2
      same-parity edges (Proposition~\ref{prop:bipartite-suffices}).
\item Under Definition~\ref{def:resolution}, being a level resolution is
      equivalent to admitting a proper 4-coloring whose color cardinalities
      group pairwise to a BFS-realizable parity split. The structural
      framing through outerplanarity refines this: a constructive
      4-coloring of $G'$ is obtained via independent 2-colorings of each
      $L_k$ in $G'$, and the proof obligation is purely about removing odd
      cycles within outerplanar graphs by local edge flips, an operation
      that does not invoke 4CT.
\end{enumerate}

The algorithm of Section~\ref{sec:flip-algorithm} is the candidate
constructive answer. Phase~1 iteratively flips the shared edge between
the deepest interior odd face and its lowest-depth neighbor, pushing the
residual odd-face structure toward the seed set $\mathcal{B}$ at
depth~$0$, with optional even-face restructuring moves along the way;
Phase~2 disposes of the remaining outer-incident odd cycles by flipping
an outer-face edge each (and optionally an even outer-incident face),
accepting a multigraph if the apex edge already exists.
Observation~\ref{obs:empirical-lk-bipartite} records that the algorithm
terminates and succeeds at the level-bipartiteness layer on all $29640$
tested $(G, S, k)$ triples at $n \in \{9, 10, 11\}$.
Observation~\ref{obs:md4-simple-resolution} records that every
minimum-degree-$4$ iso-class on $n \leq 11$ vertices is reached as a
simple level resolution; Conjecture~\ref{conj:simple-md4} extends this
to all $n$.
Question~\ref{q:terminate-all-n} asks whether Phase~1 terminates in
general.

\section{Implementation}
\label{sec:impl}

The code accompanying this paper consists of the following modules:
\begin{itemize}
\item \texttt{level\_cycles.py}: core library for levels, level cycles,
      flip candidates, and resolution enumeration.
\item \texttt{triangulation\_gen.py}: enumeration of all non-isomorphic
      triangulations on $n$ vertices via vertex-insertion plus flip closure.
\item \texttt{coverage.py}: iso-class coverage reports with optional source
      and target filters.
\item \texttt{balanced\_layout.py}: a planar drawing routine that starts
      from a Tutte embedding and uses random-search optimization to
      equalize interior face areas while maintaining planarity.
\item \texttt{four\_color.py}: 4-coloring of $G'$ via independent
      BFS 2-colorings of parity subgraphs.
\item Visualization scripts: \texttt{plot\_oct.py}, \texttt{n7\_examples.py},
      \texttt{four\_color\_viz.py}.
\end{itemize}

\begin{thebibliography}{9}
\bibitem{appelhaken}
K.\ Appel and W.\ Haken,
\emph{Every Planar Map Is Four Colorable},
Contemporary Mathematics, vol.~98, AMS, 1989.

\bibitem{rsst}
N.\ Robertson, D.\ Sanders, P.\ Seymour, and R.\ Thomas,
``The four-colour theorem'',
\emph{Journal of Combinatorial Theory, Series B}, vol.~70, pp.~2--44, 1997.

\bibitem{tutte}
W.~T.\ Tutte,
``How to draw a graph'',
\emph{Proc.\ London Math.\ Soc.}, vol.~13, pp.~743--767, 1963.

\bibitem{chartrand}
G.~Chartrand and F.~Harary,
``Planar permutation graphs'',
\emph{Annales de l'Institut Henri Poincar\'e Section B}, vol.~3,
pp.~433--438, 1967.
\end{thebibliography}

\end{document}

%-----------------------------------------------------------------------
% End of amsart-template.tex
%-----------------------------------------------------------------------