\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz}
\usepackage{hyperref}
\usepackage{enumitem}

\theoremstyle{definition}
\newtheorem{definition}{Definition}
\newtheorem{conjecture}{Conjecture}
\newtheorem{question}{Question}

\theoremstyle{plain}
\newtheorem{proposition}{Proposition}
\newtheorem{observation}{Observation}

\title{Level Resolutions of Maximal Planar Graphs:\\
A Proof Strategy for the Four Color Theorem and\\
Computational Investigation of Surjectivity}

\author{Didericis\\\small{(with computational verification by Claude)}}

\date{\today}

\begin{document}
\maketitle

\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 (verified for all triangulations and sources at
$n \leq 10$), 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}

\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{proposition}
\label{prop:outerplanar}
For every plane triangulation $G$ and every level source $S$ of $G$, each
level subgraph $L_k$ is outerplanar.
\end{proposition}

A planar embedding witnessing outerplanarity is inherited from $G$: in the
planar embedding $\Pi_G$, the vertices at distance $\leq k - 1$ from the
source lie strictly on one side of the boundary of $L_k$, so all $L_k$
vertices can be placed on a common face of $L_k$. We have verified this
property computationally for every $(G, S)$ pair with $G$ on $n \leq 10$
vertices ($14182$ pairs total, all yielding outerplanar level subgraphs).

The combinatorial significance of Proposition~\ref{prop: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:impl}.

\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
      (Proposition~\ref{prop: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}

\begin{question}
Given that each $L_k$ is outerplanar, can the odd cycles of each $L_k$ in
$G$ be broken by a globally consistent choice of flips? Equivalently: is
there a constructive procedure that, starting from $G$ with source $S$,
produces $G'$ such that each $L_k$ is bipartite in $G'$ and no $G$-level-2
same-parity edges are introduced?
\end{question}

\begin{question}
Outerplanarity of $L_k$ has been verified at $n \leq 10$ for every
$(G, S)$. Does it hold for all $n$? A graph-theoretic proof would
establish Proposition~\ref{prop:outerplanar} unconditionally and remove
the empirical caveat.
\end{question}

\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}
