# A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

Christian Doczkal

► To cite this version:

Christian Doczkal. A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome, Italy. pp.17:1-17:17. hal-03142192v2

HAL Id: hal-03142192

https://hal.science/hal-03142192v2

Submitted on 2 Feb 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

Christian Doczkal

Université Côte d'Azur, Inria Sophia Antipolis Méditerranée (STAMP), France

## Abstract

Wagner's theorem states that a graph is planar (i.e., it can be embedded in the real plane without crossing edges) iff it contains neither $K_5$ nor $K_{3,3}$ as a minor. We provide a combinatorial representation of embeddings in the plane that abstracts from topological properties of plane embeddings (e.g., angles or distances), representing only the combinatorial properties (e.g., arities of faces or the clockwise order of the outgoing edges of a vertex). The representation employs combinatorial hypermaps as used by Gonthier in the proof of the four-color theorem. We then give a formal proof that for every simple graph containing neither $K_5$ nor $K_{3,3}$ as a minor, there exists such a combinatorial plane embedding. Together with the formal proof of the four-color theorem, we obtain a formal proof that all graphs without $K_5$ and $K_{3,3}$ minors are four-colorable. The development is carried out in Coq, building on the mathematical components library, the formal proof of the four-color theorem, and a general-purpose graph library developed previously.

**2012 ACM Subject Classification** Mathematics of computing → Graphs and surfaces; Theory of computation → Logic and verification

**Keywords and phrases** Coq, MathComp, Graph-Theory, Hypermaps, Planarity

**Digital Object Identifier** 10.4230/LIPIcs.ITP.2021.17

**Supplementary Material** All proofs in this paper have been formalized using the Coq interactive theorem prover and are included in version 0.9 of the coq-community/graph-theory library:

*Software (Code Repository): https://github.com/coq-community/graph-theory*

archived at swh:1:dir:81966a945703d0e2a85fe34e920f4fe9a46b6e03

**Funding** Christian Doczkal: This work was supported by the French Agence Nationale de la Recherche (ANR) within the program Investissements d'Avenir UCA JEDI (ANR-15-IDEX-01).

# 1 Introduction

Despite the importance of graph theory in mathematics and computer science, formalizations of graph theory results, as opposed to verified graph algorithms, remain few and spread between different systems. This includes early works in HOL4 [3, 2] and Mizar [12], as well as some landmark results such as the formalization of the four-color theorem [10] in Coq or the formal proof of the Kepler conjecture [11] in HOL Light and Isabelle. Unfortunately, none of these has lead to the development of a widely-used general-purpose graph theory library. Since we started to develop such a general-purpose library in 2017 [6, 7, 8], there has been some renewed interest in the formalization of graph theory [14, 15]. In [8], one of the main results is a formal proof that the graphs of treewidth at most two are precisely those that do not include $K_4$, the complete graph with four vertices, as a minor. Other classes of graphs can also be described in terms of excluded minors, and this paper is concerned with the characterization of planar graphs as those that contain neither $K_5$ nor $K_{3,3}$ (cf. Figure 1) as a minor. This is known as Wagner's theorem.

The textbook definition (e.g. in [5]) of a graph being planar is that there exists a drawing (or embedding) in the real plane without crossing edges. However, much of the information provided by such a drawing (e.g., the precise location of vertices or the angles at which an edge leaves a vertex) are irrelevant for most proofs about planar graphs as they can be changed almost at will by shifting or deforming the drawing. A more abstract alternative

<figure><img src="image_2.png" /></figure>

© Christian Doczkal;

licensed under Creative Commons License CC-BY 4.0

12th International Conference on Interactive Theorem Proving (ITP 2021).

Editors: Liron Cohen and Cezary Kaliszyk; Article No. 17; pp. 17:1–17:17

<figure><img src="image_3.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
17:2 A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

would be to take the characterization in terms of excluded minors as the definition of planarity.
However, this would not provide any geometric information at all. In particular, a graph
can have multiple embeddings that differ in their combinatorial properties. For instance,
consider the following two drawings of the same graph:

<figure><img src="image_4.png" /></figure>

On the left, the (inner) faces have arities 5, 3, and 3, while the arities on the right are 4, 3, and 4. Some proofs about planar graphs crucially rely on these kinds of combinatorial properties of a given plane embedding. For instance, this is the case for the proof of the four-color theorem (FCT), and the formal proof of the FCT in Coq [9, 10] represents drawings of graphs using a structure called combinatorial hypermaps [4, 17]. This representation is quite far away from the ordinary representations of graphs as a collection of vertices and edges, instead representing vertices and edges as permutations on more primitive objects called “darts”.

In this paper, we use combinatorial hypermaps to represent embeddings of simple graphs,
and then give a formal and constructive proof that every simple graph containing neither $K_5$
nor $K_{3,3}$ as a minor can be represented by a planar hypermap.<fnref n="1" /> This corresponds to one
direction of Wagner's theorem, the direction that's mathematically more interesting.<fnref n="2" /> In
particular, we bridge the gap between the hypermap representation of graphs used in [9, 10]
and the more standard representation of simple graphs as a finite type of vertices with an
edge relation. The latter representation is used pervasively in the graph theory library we
developed previously [8] and on which we base the parts of the argument that deal with
structural properties like minors and separators. As it comes to hypermaps, we build on the
formalization used in the proof of the four color theorem [9, 10]. Thus, as a corollary of this
work, we obtain a formal proof of a “structural” four-color theorem, i.e., a proof that every
graph not containing the aforementioned minors is four-colorable. This theorem does not
mention hypermaps in its statement. Hence, the question whether planar hypermaps are
a faithful representation of plane embeddings is secondary. What is important is that this
representation allows for machine-checked proofs of interesting properties.

2 Graph Theory Preliminaries

In this section we review some standard notions from graph theory that are used in the
proof of Wagner’s theorem. We mostly use the conventions and terminology from previous
work [8].

A (*simple*) graph is a pair $(G, -)$ where $G$ is a finite type of objects called *vertices* and “-”
is an irreflexive and symmetric relation on $G$. We use single capital letters $F, G, \dots$ to denote
graphs as well as their underlying type of vertices. That is, we write $x, y : G$ to denote that
$x$ and $y$ are vertices of $G$. We also write $x-y$ to say that $x$ and $y$ are linked by an edge and
$N(x) := \{y \mid x-y\}$ for the *open neighborhood* of $x$. If $x, y : G$, we write $G + xy$ for $G$ with
an additional $xy$-edge. For a set of vertices $V$, we write $G[V]$ for the subgraph induced by $V$,
$G - V := G[\bar{V}]$ for the subgraph induced by the complement of $V$, and $G - x := G[\{x\}]$ for
the graph that results from deleting the vertex $x$ (and any incident edges) from $G$.<fnref n="3" />

<footnote n="1">¹ For technical reasons, we also exclude graphs with isolated vertices (cf. Remark 21).</footnote>

<footnote n="2">² We briefly comment on what would be required to prove the converse direction in Section 10.</footnote>

<footnote n="3">³ Technically, the vertices of $G[V]$ are dependent pairs of vertices $x:G$ and proofs $x \in V$, but we will ignore this in the mathematical presentation (cf. [8]).</footnote>
<figure><img src="image_5.png" /><figcaption>Figure 1 $K_4$ (left), $K_5$ (middle), and $K_{3,3}$ (right).</figcaption></figure>

We write $|G|$ for the size of $G$, i.e. the number of vertices of $G$. We write $G/xy$ for the graph that results from merging the vertices $x$ and $y$ in $G$, which is implemented by removing the vertex $y$ and attaching its neighbors to $x$. We write $K_n$ for the complete graph with $n$ vertices and $K_{3,3}$ for the complete bipartite graph with two times three vertices (cf. Figure 1).

A *path* (in some graph $G$) is a nonempty sequence of vertices with subsequent vertices linked by the edge relation, and an *$xy$-path* is a path starting at $x$ and ending at $y$. A *cycle* is an $xy$-path for some $x, y : G$ such that $x \to y$. If $\pi_1$ and $\pi_2$ are paths, we write $\pi_1 + \pi_2$ for their concatenation. A set of vertices $A$ is *connected*, if any two vertices in $A$ are connected by a path contained in $A$. Two sets of vertices $A$ and $B$ are *neighboring*, if there exist vertices $x \in A$ and $y \in B$ such that $x \to y$.

A set of vertices $S$ separates $x$ and $y$, if $x, y \notin S$ and every $xy$-path contains a vertex from $S$. A set that separates any two vertices, i.e. whose removal would disconnect the graph, is called a (*vertex separator*). In particular, $\emptyset$ is a separator iff $G$ has multiple disconnected components. A graph $G$ is $k$-connected if $k < |G|$ and every separator has size at least $k$. In particular, $K_{k+1}$ is $k$-connected, since there are no separators in a complete graph. A separation of $G$ is a pair $(V_1, V_2)$ of sets of vertices such that $V_1 \cup V_2$ covers $G$ and there is no edge from $\bar{V_1}$ to $\bar{V_2}$. A separation $(V_1, V_2)$ is proper, if both $\bar{V_1}$ and $\bar{V_2}$ are nonempty.

**Fact 1.** Let $G$ be a simple graph. Every separator $S$ of $G$ can be extended into a proper separation $(V_1, V_2)$ of $G$ such that $S = V_1 \cap V_2$.

We are interested in the characterization of planar graphs through excluded minors. Intuitively, a minor of a graph is a graph that can be obtained from the original graph through a series of edge deletions, vertex deletions, and edge contractions. Following our previous work [8], we define the minor relation using functions we call minor maps:

**Definition 2.** Let $G$ and $H$ be simple graphs. A function $\phi : H \to 2^G$ is called a minor map if:

M1. $\phi(x)$ is nonempty and connected for all $x : H$,

M2. $\phi(x) \cap \phi(y) = \emptyset$ whenever $x \neq y$ for all $x, y : H$.

M3. $\phi(x)$ neighbors $\phi(y)$ for all $x, y : H$ such that $x \to y$.

$H$ is a minor of $G$, written $H \prec G$ if there exists a minor map $\phi : H \to 2^G$.

If $\phi : H \to 2^G$ is a minor map, then $\phi(x)$ is the set of vertices being collapsed to $x$ (by contracting all the edges in $\phi(x)$) when exhibiting $H$ as a minor of $G$.

**Fact 3.** $\prec$ is transitive.

**Definition 4.** A graph $G$ is called $H$-free, if $H$ is not a minor of $G$.

Note that if $G$ is $H$-free, then, by transitivity, so is every minor of $G$. Also note that if $x \to y$, then $G/xy$ corresponds to an edge contraction. Hence, we have the following lemma.

**Lemma 5.** If $x \to y$, then $G/xy \prec G$
17:4 A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

It is easy to see that $G[V] \prec G$, for any set $V$ of vertices of $G$, and thus $G[V]$ is $H$-free whenever $G$ is. However, when $V$ is one of the two sides of a separation arising from a separator $\{x, y\}$, we can even add an $xy$-edge, as shown below.

**Lemma 6.** Let $(V_1, V_2)$ be a proper separation of $G$ with $V_1 \cap V_2 = \{x, y\}$ with $x \neq y$ and $\{x, y\}$ a smallest separator. Then every minor of $(G + xy)[V_1]$ is also a minor of $G$.

**Proof.** If the $xy$-edge is used to justify $H \prec (G+xy)[V_1]$ for some $H$, the $xy$-edge can always be replaced by a path through $V_2 \setminus V_1$, which is not otherwise needed to establish $H \prec G$. ◀

3 Wagner's Theorem

Before we turn to the formal proof of Wagner's theorem using combinatorial hypermaps, we first sketch the proof relying on an informal notion of plane embedding (i.e., drawings of the graph without crossing edges), leaving the technical details of the modeling to Section 6.

The proof of Wagner's theorem consists of two parts. The main induction deals with the case for 3-connected graphs. This is then extended to the general case though a number of comparatively straightforward combinations of plane embeddings for subgraphs. Below, we sketch the two arguments, including forward references to two types of lemmas: those that are interesting from a mathematical point of view (marked with "★") and those that depend on the modeling of plane embeddings using hypermaps (marked with "†"). The proofs are inspired by those in [1, 5].

**Proposition 7.** Let $G$ be 3-connected, $K_5$-free, and $K_{3,3}$-free. Then $G$ can be embedded in the plane.

**Proof sketch.** The proof proceeds by induction on $|G|$.

1. Since $G$ is 3-connected, we have $4 \le |G|$. If $|G| = 4$, then $G$ is $K_4$, which can easily be embedded in the plane (Figure 1, Proposition 22$^\dagger$). Hence, we can assume $5 \le |G|$.

2. Thus, we obtain $x, y : G$ such that $x \neq y$ and $G/xy$ is again 3-connected (Theorem 11$^*$).

3. Since $|G/xy| < |G|$, we obtain a plane embedding for $G/xy$ by induction (Lemma 5). Let $v_{xy}$ be the vertex resulting from the contraction of the $xy$-edge and set $H := G/xy - v_{xy}$. Let $X$ (resp. $Y$) be the set of vertices in $H$ that are neighbors of $x$ (resp. $y$) in $G$.

4. Since $G/xy$ is 3-connected and since all vertices in $X \cup Y$ are neighbors of $v_{xy}$, removing $v_{xy}$ and all incident edges from the plane embedding of $G/xy$ yields a plane embedding $\hat{H}$ of $H$ with a face whose boundary contains all vertices from $X$ and $Y$ (Lemma 28$^{*\dagger}$).

5. Since $G/xy$ is 3-connected, we have that $H$ is 2-connected. Hence, the face of $\hat{H}$ whose boundary contains $X$ and $Y$ is bounded by a (duplicate-free) cycle $C$ (Theorem 25$^{*\dagger}$).

6. Splitting $C$ at the elements of $X$ yields a number of segments where every segment overlaps with each of its two neighboring segments in exactly one element of $X$ (unless there are only two segments). Since $K_5 \not\subset G$ and $K_{3,3} \not\subset G$, all elements of $Y$ must be contained in one of the segments of $C$; call this segment $C_y$ (Lemma 12$^*$)

7. Adding a vertex $x'$ to $\hat{H}$ inside $C$ and making it adjacent to all vertices in $X$ yields a graph with an embedding that has a face containing $x'$ and $C_y$. Thus, we can place a vertex $y'$ within this face and add edges to $x'$ and all vertices in $Y$ as shown below:

<figure><img src="image_6.png" /></figure>

This yields a plane embedding of $G$.

◀
It remains to take care of the cases where $G$ is not 3-connected.

**▶ Theorem 8.** Let $G$ be $K_5$-free, and $K_{3,3}$-free. Then $G$ can be embedded in the real plane.

**Proof.** By induction on $|G|$. By Propositions 7 and 22, we can assume that $5 \le |G|$ and that $G$ has a smallest separator $S$ with $|S| \le 2$. We obtain a proper separation $(V_1, V_2)$ with $V_1 \cap V_2 = S$. If $S = \{x, y\}$, we set $H := G + xy$ and have that neither $H[V_1]$ nor $H[V_2]$ contains $K_5$ or $K_{3,3}$ as a minor (Lemma 6), allowing us to obtain plane embeddings of $H[V_1]$ and $H[V_2]$ by induction. Due to the added $xy$-edge, both embeddings must have a face with $x$ and $y$ adjacent on the boundary of some face. Without loss of generality, we can assume that this is the (unbounded) outer face. By stretching and scaling, we can “glue” together the two embeddings along these outer edges, obtaining a plane embedding of $H$ (Lemma 30*). Removing the $xy$ edge (or keeping it if it was present in $G$), provides a plane embedding of $G$. The cases for $S = \emptyset$ and $S = \{x\}$ are similar, but do not require the use of a “marker” edge. ◀

Note that the proof of Theorem 8 makes reference to intuitive operations such as stretching and scaling. In particular, the fact that one can turn an arbitrary face into the outer face is usually argued using a stereographic projection to the sphere and back to the plane [1]. All of these will be no-ops for our representation of plane embeddings using hypermaps.

## 4 The Combinatorial Part

This section is concerned with the purely combinatorial part of the proof of Proposition 7, justifying steps (2) and (6). The former amounts to locating an edge in a 3-connected graph such that contracting this edge yields a smaller 3-connected graph. The latter is about justifying (using the names from the proof of Proposition 7) that in the cycle $C$ all the neighbors of $y$ are contained in a segment spanned by two successive neighbors of $x$. This is the part of the proof where assumptions of $K_5$-freeness and $K_{3,3}$-freeness are used. Both arguments are combinatorial in the sense that neither argument makes any reference to plane embeddings.

For step (2), the argument is based on smallest separators, and we repeatedly use the following property:

**Proposition 9.** If $S$ is a smallest separator of $G$, then $S$ neighbors every maximal component of $G-S$.

Recall that $G/xy$ is implemented by removing $y$ and updating the edge relation accordingly.

**Lemma 10.** Let $G$ be 3-connected with $5 \le |G|$, and let $x, y : G$ such that $x-y$ and $G/xy$ is not 3-connected. Then there exists some $z : G$ such that $\{x, y, z\}$ is a separator.

**Proof.** Since $G$ is 3-connected, we have that $G/xy$ is 2-connected. Moreover, $G/xy$ is not 3-connected by assumption. Hence, $G/xy$ has a smallest separator $S$ with $|S| = 2$. We have that $x \in S$, because otherwise $S$ would be a 2-separator of $G$. Thus, $S = \{x, z\}$ for some $z$, and $\{x, y, z\}$ is a separator of $G$. ◀

**Theorem 11.** If $G$ is 3-connected and $5 \le |G|$, then there exists an $xy$-edge such that $G/xy$ is 3-connected.
<figure><img src="image_7.png" /><figcaption>Figure 2 Objects from the proof of Theorem 11 (cf. [1, Theorem 9.10]).</figcaption></figure>

**Proof.** Assume the theorem does not hold, i.e., assume that $G/xy$ is not 3-connected for all $x, y : G$ such that $x-y$. We obtain a contradiction as follows:

By Lemma 10, every $xy$-edge can be extended to a separator $\{x, y, z\}$. Choose $x, y, z$, and $F$ such that $x-y$, $\{x, y, z\}$ is a separator, $F$ is connected and disjoint from $\{x, y, z\}$, and with $|F|$ maximal for all possible choices of $x, y, z$ and $F$. Now set $H := F \cup \{x, y\}$. Since $G$ is 3-connected, $\{x, y, z\}$ is indeed a smallest separator of $G$. Thus, $x, y$, and $z$ are pairwise distinct and by Proposition 9 there exists some vertex $u \notin H$ such that $z-u$ (cf. Figure 2). Let $v$ such that $\{z, u, v\}$ is a separator (Lemma 10). Now it suffices to show that $H \setminus \{v\}$ is connected, because this yields a component larger than $F$, contradicting the choice of $F$. If $v \notin H$ this is trivial and if $v \in \{x, y\}$, this follows since $\{x, y, z\}$ is a smallest separator. (Proposition 9 ensures that both $x$ and $y$ have neighbors in $F$.) Hence, we can assume $v \in F$. Now if $H \setminus \{v\}$ was disconnected, then there would be some vertex $w$ such that every $xw$-path in $H$ passes through $v$. However, since $F$ is maximal and therefore has no outgoing edges other than those to $x, y$, and $z$, this would entail that $\{v, z\}$ is a separator (separating $x$ from $w$), contradicting the assumption that $G$ is 3-connected. ◀

We remark that, just like all the other results presented in this paper, the proof of Theorem 11 does not require any classical axioms. The conclusion of the theorem involves only decidable predicates and quantifiers over finite domains (i.e., the vertices of $G$), and these behave classically. Similarly, there are only finitely many choices for $x, y, z$, and $F$, so we can easily obtain a combination where $|F|$ is maximal among all possible choices.

In order to formally state the lemma justifying step (6) of Proposition 7, we need to introduce some operations on duplicate-free lists viewed as cycles. Let $T$ be some type and let $C$ be a duplicate free list over $T$. For $x \in C$, we write $\text{next } Cx$ for the element following $x$ in $C$ or the first element of $C$ if $x$ is at the very end. For $x, y \in C$ with $x \neq y$, we write $\text{arc } Cxy$ for the part of $C$ (seen as a cycle) that starts at $x$ and ends right before $y$. In particular, the results of $\text{next } Cx$ and $\text{arc } Cxy$ are invariant under cyclic shifts of $C$.

**Lemma 12.** Let $G$ be a simple, $K_5$-free, and $K_{3,3}$-free graph, let $x, y : G$ such that $x-y$ and let $C$ be a duplicate-free cycle in $G$ containing neither $x$ nor $y$. Let $X$ be the sub-sequence of $C$ containing $N(x)$ and let $Y$ be the sub-sequence of $C$ containing $N(y)$. If $X$ and $Y$ each contain at least two vertices, then there exists some vertex $z \in X$ such that $Y \subseteq \text{arc } Cz$ (next $Xz$) $\cup$ $\{\text{next } Xz\}$.

**Proof.** We first show that there are at most two vertices in $X \cap Y$. Assume, for the sake of contradiction, three distinct vertices $u, v, w \in X \cap Y$. W.l.o.g., we can assume that $[u, v, w]$ is a sub-cycle of $C$. Hence, we obtain $K_5$ as a minor of $G$ by collapsing by mapping the vertices of $K_5$ to the sets $\{x\}$, $\{y\}$, $\text{arc } Cuv$, $\text{arc } Cvw$, and $\text{arc } Cwu$ as shown in Figure 3(a), contradicting the assumption that $G$ is $K_5$-free.
<figure><img src="image_8.png" /><figcaption>Figure 3 Obtaining $K_5$ (left) and $K_{3,3}$ (right) as minors in Lemma 12.</figcaption></figure>

Next, we show that there cannot be a sub-cycle $[x_1, y_1, x_2, y_2]$ of $C$ such that $\{x_1, x_2\} \subseteq X$ and $\{y_1, y_2\} \subseteq Y$. If such a sub-cycle were to exist, we could exhibit $K_{3,3}$ as a minor of $G$ by mapping the three pairwise-independent left-hand-side vertices to $\{x\}$, $\mathrm{arc}\,C\,y_1\,x_2$, and $\mathrm{arc}\,C\,y_2\,x_1$ and the three right hand side vertices to $\{y\}$, $\mathrm{arc}\,C\,x_1\,y_1$, and $\mathrm{arc}\,C\,x_2\,y_2$, contradicting $K_{3,3}$-freeness of $G$ (cf. Figure 3(b)).

Now, assume that the theorem does not hold, i.e., assume that for every $x' \in X$, there exists some $y' \in Y$ such that $y' \notin \mathrm{arc}\,C\,x' (\mathrm{next}\,X\,x') \cup \{\mathrm{next}\,X\,x'\}$. We consider two cases:

- If $Y \subseteq X$, we have that $Y = [y_1, y_2]$ for two distinct vertices $y_1$ and $y_2$. Now $\mathrm{arc}\,C\,y_1\,y_2$ must contain some vertex $x_2 \in X \setminus \{y_1, y_2\}$, for otherwise $\mathrm{next}\,X\,y_1 = y_2$ and both $y_1$ and $y_2$ are contained in $\mathrm{arc}\,C\,y_1\,y_2 \cup \{y_2\}$. By symmetry, we also have that $\mathrm{arc}\,C\,y_2\,y_1$ must contain some $x_1 \in X \setminus \{y_1, y_2\}$. However, then $[x_1, y_1, x_2, y_2]$ is an alternating subcycle, whose existence we excluded above. Contradiction.

- Otherwise, there exists some $y_1 \in Y \setminus X$. Let $x_1$ such that $y_1 \in \mathrm{arc}\,C\,x_1$ ($\mathrm{next}\,X\,x_1$) and set $x_2 := \mathrm{next}\,X\,x_1$. By assumption, there must be some $y_2 \in Y$ with $y_2 \notin \mathrm{arc}\,C\,x_1\,x_2 \cup \{x_2\}$. Hence, $[x_1, y_1, x_2, y_2]$ is again an excluded alternating subcycle. Contradiction. ◀

Lemma 12 can be considered to be the combinatorial core argument underlying Wagner's theorem. It is the place where absence of certain substructures (i.e., the minors $K_5$ and $K_{3,3}$) is turned into a positive statement that allows reversing the contraction of the $xy$-edge. We remark that while the $\mathrm{arc}$ construction was already present in mathcomp, splitting a cycle along a subcycle required a plethora of additional lemmas about arcs and cycles.

# 5 Combinatorial Hypermaps

We now turn towards the modeling of embeddings in the plane using combinatorial hypermaps. In this section we briefly review hypermaps and their most important properties. The presentation follows [9], because the formal development underpinning this part is based on the formal proof of the four-color theorem presented there. Consequently, none of the results in this section are new.

**Definition 13.** A (combinatorial) hypermap is a tuple $\langle D, e, n, f \rangle$ where $D$ is a finite type, and $e, n, f: D \to D$ such that $n \circ f \circ e \equiv \mathrm{id}_D$. The elements of $D$ are referred to as darts.

The condition $n \circ f \circ e \equiv \mathrm{id}_D$ ensures that the functions $e, n$, and $f$ are bijective (i.e. permutations on $D$). In particular, any two of the permutations determine the third. Each of the permutations partitions the type $D$ into a number of cycles and these cycles are used
17:8 A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

<figure><img src="image_9.png" /><figcaption>Figure 4 A hypermap. (Reprinted with permission from [9], ©2005 Georges Gonthier).</figcaption></figure>

to represent the edges, nodes<fnref n="4" />, and faces of graphs. That is, a hypermap ⟨D, e, n, f⟩ can be
seen as describing a graph embedded on a surface (not necessarily the plane) as follows (cf.
Figure 4):

- every *n*-cycle represents a node of the graph, listing incident edges in counterclockwise order.

- every *e*-cycle represents an edge of the graph, linking the nodes (i.e., *n*-cycles) it intersects.

- every *f*-cycle represents a face, listing in counterclockwise order one dart from every node on the boundary of the face.

Even though one of the three permutations is technically redundant, keeping it makes the definition completely symmetric and facilitates symmetry reasoning. In particular, if ⟨D, e, n, f⟩ is a hypermap, then so are ⟨D, f, e, n⟩ and ⟨D, n, f, e⟩. As we do for graphs, we will usually use the same letter for a hypermap and its underlying type of darts.

► **Definition 14.** Let ⟨D, e, n, f⟩ be a hypermap.

- *D is called plain if every e-cycle has size 2.*

- *D is called loopless if x and e(x) belong to different n-cycles for all x : D.*

- *D is called simple if two n-cycles are linked by at most one e-cycle.*

Plain hypermaps correspond to graphs where every edge is adjacent to two vertices, i.e. graphs without hyperedges. As we will make precise later, plain loopless simple hypermaps correspond to simple graphs, i.e., graphs without self loops and with at most one edge between two vertices. The (partial) hypermap in Figure 4 satisfies all three properties, as will most of the hypermaps we will be dealing with.

We fix a hypermap ⟨D, e, n, f⟩ for the rest of the section. Moreover, we will use the same letter *D* for the hypermap as a whole as well as the underlying type of darts.

The number of “holes” that would be needed in a surface in order to embed a given
hypermap in it can be computed using the Euler characteristic.

**Definition 15 (Genus).** The genus of *D* is ((2*C* + |*D*|) − (*E* + *N* + *F*)) / 2 where *C* is the number of connected components of *e* ∪ *n* ∪ *f* (interpreting the functions as functional relations) and *E*, *N*, and *F* are the number of cycles of *e*, *n*, and *f* respectively. A map of genus 0, i.e., a map satisfying the equation *E* + *N* + *F* = 2*C* + |*D*| is called planar.

<footnote n="4">⁴ In line with the terminology of [9, 10], we say “node” when referring to an *n*-cycle of a hypermap. In line with [8], we continue to use “vertex” when referring to vertices of simple graphs.</footnote>
The following general properties of hypermaps are established in [9].

► **Proposition 16.** $E + N + F \le 2C + |D|$.

► **Proposition 17.** $(2C + |D|) - (E + N + F)$ is even.

Proposition 16 implies that the (natural number) subtraction in Definition 15 is never truncating and Proposition 17 implies that the division in the genus formula is always an integer division without remainder.

For our use of hypermaps as representations of embeddings in the plane, we will need to modify hypermaps and prove that these modifications preserve planarity. Directly proving that an operation such as adding an edge across a face preserves the genus of the hypermap can be cumbersome. It is often simpler to express the operation in terms of more atomic planarity-preserving operations. The most important of these operations are the Walkup [16, 18] operations.

► **Definition 18.** For $x: D$, Walkup$E$ $x$ is the hypermap where $x$ has been removed by skipping over $x$ in the $n$ and $f$ permutations and adapting $e$ as necessary. Similarly, Walkup$N$ $x$ (resp. Walkup$F$ $x$) are the hypermaps where $n$ (resp. $f$) is the permutation being adapted after suppressing $x$ from the other two.

As shown in [9], the Walkup operations never increase the genus of a hypermap and, in particular, always preserve planarity. In addition, the Walkup operations can be shown to preserve the genus in many circumstances, allowing us to prove preservation of planarity for operations that extend the hypermap by expressing them as inverse Walkup operations. Thus, the characterization of planarity in terms of Euler's formula combined with expressing operations as combinations of Walkup operations provides for an easy means of proving that various operations on hypermaps preserve planarity.

In addition to showing that certain operations preserve planarity, we also need to establish some properties of planar hypermaps in general. For instance, we need to show that in every two-connected plane graph, all faces are bounded by (duplicate free) cycles (step (5)). For the topological model of plane graphs, this property is established using the Jordan curve theorem (JCT), which states that every closed simple curve divides the plain into an “inside” and an “outside”. Since hypermaps make no reference to the real plane, we could not use this theorem, even if it was available in Coq. However, the essence of the application of the JCT to plane graphs is captured by the following theorem on hypermaps:

► **Theorem 19 (Jordan curve theorem for hypermaps [9, 10]).** Let $\langle D, e, n, f \rangle$ be a hypermap. Then $D$ is planar iff there do not exist distinct darts $x, y$ and a duplicate-free $(n^{-1} \cup f)$-path from $x$ to $n(y)$ visiting $y$ before $n(x)$ (with $y = n(x)$ being allowed).

Note that when talking about hypermaps, an $(n^{-1} \cup f)$-path is a path in the relation $(n^{-1} \cup f)$. This is to be contrasted with the notion of an *xy*-path in a simple graph, where we mention the endpoints and leave the relation implicit. Paths in the relation $(n^{-1} \cup f)$ are called *contour paths*, because they go around the outside of a group of faces (cf. Figure 4). Thus, a contour cycle in a planar map corresponds to a closed curve. The Jordan curve theorem for hypermaps establishes that in a planar hypermap there cannot be a contour path starting at the inside of a contour cycle and finishing on the outside without otherwise intersecting the cycle. In the theorem above, the contour cycle and the contour path are spliced together in order to obtain a simpler statement (cf. [9, 10]).
**6 Combinatorial Embeddings**

In this section, we make precise what it means for a hypermap to represent an embedding
of a graph on some surface. We first introduce some additional notation. For a relation
$r: D \to D \to \mathbb{B}$ over a finite type $D$ (e.g., the darts of a hypermap) we write $r^*$ for the
reflexive transitive closure of $r$ and $r^*(x)$ for the set $\{y \mid r^* x y\}$. In particular, we write $f^*$
for the transitive closure of a function $f: D \to D$ seen as the relation $\lambda x y. fx = y$. Note
that, because $D$ is finite, $f^*$ is symmetric if $f$ is injective, as is the case for the permutations
comprising hypermaps. For a hypermap $\langle D, e, n, f \rangle$, we call two darts $x$ and $y$ *adjacent*,
written $\text{adj } xy$, if their respective $n$-cycles are linked by an $e$-cycle (i.e., if there exists some
dart $z$ such that $n^* x z$ and $n^* y (e z)$).

► **Definition 20.** Let $G$ be a simple graph and let $\langle D, e, n, f \rangle$ be a plain hypermap. We call a function $g: D \to G$ a (combinatorial) embedding of $G$ if it satisfies the following properties:

1. *g is surjective*

2. $n^* xy \text{ iff } g(x) = g(y)$.

3. $\text{adj } xy \text{ iff } g(x) - g(y)$.

An embedding where $D$ is planar, is called a plane embedding, and an embedding where $D$ is
simple is called a simple embedding. A graph together with a plane embedding is called a
plane graph.

Note that, even though we refer to *g* as an embedding of a graph, the function maps darts of
the hypermap to vertices of the graph. This makes it easier to state the required properties.
Surjectivity of *g* ensures that *D* represents the whole graph. Condition (2) ensures that the
node cycles of *D* are in one-to-one correspondence to the vertices of *G*, and condition (3)
ensures that adjacent node cycles correspond to adjacent vertices of *G*. Note that we do
not require that the hypermap underlying an embedding is simple, i.e., we permit multiple
parallel edges. This reduces the number of conditions to check when constructing plane
embeddings. Parallel edges can always be removed, obtaining a simple embedding where
needed.

► **Remark 21.** Definition 20 abstracts not only from properties that can be changed by continuously deforming the plane, it also does not single out a face as the “outer” face or specify the relationships between the embeddings of disconnected components of a graph, i.e., we do not embed one component in a particular face of the embedding of another component. Consequently, Definition 20 corresponds more to embedding every component of the graph on its own sphere rather than embedding all components together in the plane. Moreover, the degenerate case of a component consisting of a single isolated vertex cannot be represented by hypermaps, because every dart of an *n*-cycle must also be part of an *e*-cycle. This is not really an issue: isolated vertices are components without internal structure, and there would be nothing to learn about such vertices from a combinatorial embedding.

With Definition 20 in place, we can now justify step (1) of the proof of Proposition 7, i.e., obtain a plane embedding for $K_4$. The graph $K_4$ has 6 edges, so we take the 12-element type $I_{12} := \Sigma n : \mathbb{N}. n < 12$ as the type of darts and provide the three permutations as well as a mapping from $I_{12}$ to the vertices of $K_4$. Since both $K_4$ and its embedding are concrete objects, we can use the depth-first search algorithm from mathcomp to compute the genus of the map and check the correctness of the embedding. This requires brute-forcing various quantifiers, which causes no problems due to the small size of their domain (i.e. 4 or 12). Thus, we obtain:

► **Proposition 22.** There exists a plane embedding for $K_4$.
<figure><img src="image_10.png" /><figcaption>Figure 5 Moebious path from the proof of Lemma 26.</figcaption></figure>

We also show that $K_{3,3}$ does not have a plane embedding. While this result does not contribute to the main result of this paper, it serves as an example of how Definition 20 and some of the properties described in Section 5 fit together.

**Proposition 23.** *There exists no plane embedding for $K_{3,3}$.*

**Proof.** Assume there was an embedding $g : D \to K_{3,3}$ with $D$ of genus 0. Without loss of generality, we can assume that $D$ is simple. Thus, we have $N = 6$, $E = 9$, $|D| = 2 * E = 18$, and $C = 1$. By the definition of genus, it suffices to show $(5-F)/2 > 0$ to obtain a contradiction. Since every vertex of $K_{3,3}$ has at least two neighbors and since $D$ is simple, every face-cycle must use at least 3 darts. Moreover, $K_{3,3}$ has no odd-length cycles, so every face-cycle of $D$ must indeed use at last 4 darts. Thus $F \le 4$, since $|D| = 18$. Finally, $F \ne 4$ since the division in the genus formula is always without remainder (Proposition 17). ◀

We now come to the main result of this section, namely that the faces of 2-connected plane graphs are bounded by irredundant cycles. In order to state this property precisely, we define a notion of face for simple graphs relative to an embedding.

**Definition 24.** If $g : \langle D, e, n, f \rangle \to G$ is an embedding, a face of $G$ under $g$ is a cycle in $G$ that can be obtained as the image of an $f$-cycle of $D$ under $g$.

The theorem we want to prove is the following.

**Theorem 25.** Let $g$ be a plane embedding of a 2-connected graph $G$. Then all the faces under $g$ are duplicate-free cycles.

Before we can prove this theorem, we first need to prove the underlying property on hypermaps. This is where the Jordan curve theorem for hypermaps (Theorem 19) is used.

**Lemma 26.** Let $\langle D, e, n, f \rangle$ be a plain loopless planar hypermap such that for all darts $x, y, z$ with $x, y \notin n^*(z)$ there exists an $(n^{-1} \cup f)$-path from $x$ to $y$ not containing any dart in $n^*(z)$. Then there do not exist distinct darts $x, y$ such that $n^* xy$ and $f^* xy$.

**Proof.** Assume there exist $x \ne y$ such that $n^* xy$ and $f^* xy$. We show that this contradicts the planarity of $G$. Without loss of generality, we obtain a duplicate-free $n^{-1}$-path from $y$ to $x$ whose interior $\pi$ is disjoint from $f^*(x)$ (We make $n^{-1}$-steps starting at $y$ and replace $x$ with the first encountered dart in $f^*(y)$). Now we can split the $f$-cycle containing $x$ and $y$ into two semi-cycles, one from $x$ to $y$ and another from $y$ to $x$. We call their respective interiors (which are both disjoint from $\pi \cup \{x, y\}$) $\sigma_{x,y}$ and $\sigma_{y,x}$. By assumption, we can
17:12 A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

obtain ($n^{-1} \cup f$)-paths avoiding $n^*(x)$ and connecting any two darts outside of $n^*(x)$. Thus, we obtain darts $u \in \sigma_{y,x}$ and $v \in \sigma_{x,y}$ and a duplicate-free ($n^{-1} \cup f$)-path from $u$ to $v$ disjoint from the $n$-cycle containing both $x$ and $y$ whose interior we call $\rho$. Without loss of generality, we can assume that $\rho$ is also disjoint from $\sigma_{x,y}$ and $\sigma_{y,x}$ (otherwise we shorten $\rho$, possibly changing the choice of $u$ and $v$). Finally set $\sigma_{y,u}$ to be the part of $\sigma_{y,x}$ before $u$. Thus, we have that $m := \pi \mathrel{\mathbin{\mathbin{\mathbin{\mathbin{\mathbin{\mathbin{\rho}}}}}}}[x] \mathrel{\mathbin{\mathbin{\mathbin{\mathbin{\mathbin{\rho}}}}}} \sigma_{x,y} \mathrel{\mathbin{\mathbin{\mathbin{\mathbin{\mathbin{\rho}}}}}}[y] \mathrel{\mathbin{\mathbin{\mathbin{\mathbin{\mathbin{\rho}}}}}} \sigma_{y,u} \mathrel{\mathbin{\mathbin{\mathbin{\mathbin{\mathbin{\rho}}}}}} u \mathrel{\mathbin{\mathbin{\mathbin{\mathbin{\mathbin{\rho}}}}}} \rho$ is a duplicate-free ($n^{-1} \cup f$)-path. Moreover, the fist dart in $m$ is $n^{-1}(y)$ (which could be $x$) and (since $\sigma_{x,y}$ is an $f$-path) the last dart is $n(v)$ (cf. Figure 5). Since $m$ visits $v$ (which is in $\sigma_{x,y}$) before $y$, $m$ is a "Moebius contour" and Theorem 19 applies, contradicting the planarity of $D$. ◀

Now we can prove Theorem 25, justifying step (5) of the proof of Proposition 7.

**Proof of Theorem 25.** Let $G$ be 2-connected and let $g : (D, e, n, f) \to G$ be a plane embedding. Thus $D$ is plain, loopless, and planar. Let $s$ be a face of $G$ under $g$ arising as the image of some $f$-cycle in $D$. It suffices to show that all the darts in this $f$-cycle belong to different $n$-cycles. Since $G$ is 2-connected, all vertices different from $z$ can be connected using paths that avoid $z$. These paths can be mapped to $(n^{-1} \cup f)$-paths in $D$. Hence, Lemma 26 applies, finishing the proof. ◀

The proof of Theorem 25 exhibits a pattern that is repeated for various lemmas about plane embeddings: we first show the underlying lemma for hypermaps and then lift the property to the language of simple graphs and plane embeddings in order to use them in the proofs of Proposition 7 and Theorem 8.

7 Modifying Plane Embeddings

We now describe the operations on plane embeddings and their underlying hypermaps that are required to carry out steps (4) and (7) of the proof of Proposition 7. That is, we show how to remove a vertex from a plane embedding, obtaining a face containing all neighbors of the removed vertex, and we show how to add a vertex, connecting it to an arbitrary subsequence of a face-cycle.

We begin by showing that every subgraph of a plane graph has a plane embedding. While this is intuitively obvious, the precise argument deserves some mention. Again, we need some notation to express the underlying lemma about hypermaps:

Let $T$ be a finite type and let $f : T \to T$ be an injective function and let $P$ be a subset of $T$. We write $\Sigma P$ for the type of elements of $P$, i.e., the type of dependent pairs $\Sigma x : T. x \in P$. We define $\text{skip}_P f : T \to T$ to be the function which for every $x : T$ returns $f^{n+1}(x)$ for the least $n$ such that $f^{n+1}(x) \in P$ if such an $n$ exists and $x$ otherwise. Such an $n$ always exists when $x \in P$, so $\text{skip}_P f$ can also be seen as a function $\Sigma P \to \Sigma P$. Finally, we write $f \equiv g$, to denote that two functions agree on all arguments.

**Lemma 27.** Let $\langle D, e, n, f \rangle$ be a hypermap, let $P \subseteq D$, and let $\langle \Sigma P, e', n', f' \rangle$ be another hypermap such that $e' \equiv \text{skip}_P e$ and $n' \equiv \text{skip}_P n$. Then genus $\langle \Sigma P, e', n', f' \rangle \le$ genus $\langle D, e, n, f \rangle$.

**Proof.** By induction on $|D|$. If $P$ is the full set, then the two hypermaps are isomorphic and therefore have the same genus. Thus, we can assume there exists some $z \notin P$. Let $H := \text{WalkupF} z$. Since the Walkup operation does not increase the genus, it suffices to show genus $\langle \Sigma P, e', n', f' \rangle \le$ genus $H$. This follows by induction hypothesis since $H$ is defined by skipping over $z$ in the edge and node permutations and, therefore, $\langle \Sigma P, e', n', f' \rangle$ can be obtained from $H$, again up to isomorphism, by skipping over the remaining elements of $\bar{P}$. ◀
<figure><img src="image_11.png" /><figcaption>Figure 6 Removing a vertex from a 2-connected plane graph.</figcaption></figure>

Note that Lemma 27 applies to any hypermap, not just plain ones. This small generalization allows us to prove the lemma by induction, removing a single dart at a time. This would not work with plain maps, which always have an even number of darts. Also note that the proof of the lemma above makes extensive use of isomorphisms for hypermaps, a notion that is not defined in the formal development of the four-color theorem, where only an equivalence for hypermaps with the same type of darts is defined. This turned out to be too restrictive for our purposes. As we do for other types of graphs [8], we define isomorphisms between hypermaps as bijections on the underlying type of darts that preserve the three permutations.

**Lemma 28.** Let $G$ be a 2-connected graph with vertex $x$ and let $g$ be a plane embedding. Then there exists a plane embedding $g'$ for $G - x$ and a face of $g'$ containing all vertices in $N(x)$.

**Proof.** Let $D = (D, e, n, f)$ be the hypermap underlying $g$, and $d_x : D$ such that $g(d_x) = x$. Without loss of generality, we can assume that $D$ is a simple hypermap. We set $P := e^*(n^*(d_x))$ and set $D' = \langle \Sigma P, \text{skip}_P e, \text{skip}_P n, f' \rangle$ for some suitable $f'$, which amounts to removing all $e$-cycles intersecting $n^*(d_x)$. $D'$ is clearly plain, and by Lemma 27 $D'$ is also planar. Since $x \notin g(P)$, the restriction of $g$ to $D'$ yields a plane embedding $g' : D' \to (G - x)$. It remains to show that $g'$ has a face containing $N(x)$. First, 2-connectedness of $G$ rules out the scenario depicted in Figure 6(a), where removing $x$ would disconnect the graph. Moreover, it ensures that every $n$-cycle (in $D$) has at least size two. Together with $D$ being simple, this ensures that no $n$-cycle other than the one for $x$ vanishes and that $f'$ needs to skip over at most one removed dart at a time (Figure 6(b-c)), allowing us to give a simple explicit definition of $f'$: $f'(z) := \text{if } f(z) \in P \text{ then } f(z) \text{ else } n^{-1}(f(z))$

Moreover, we have that for all $d \in n^*(d_x)$, $f(d)$ is in $P$ and on the same (original) $n$-cycle as $e(d)$, meaning every dart $f(d)$ represents a neighbor of $x$. Thus, it suffices to show $f'^*(fd_1)(fd_2)$ for $d_1, d_2 \in n^*(d_x)$. We prove this claim by induction on the $n$-path from $d_1$ to $d_2$, reducing the problem to showing $f'^*(fd)(fn(d))$ for $d \in n^*(d_x)$. Since $D$ is simple, the $f$-orbit of $f(d)$ as length at least 3 and therefore the shape $[f(d)] + o + [(e(n(d)), d)]$. Moreover, since $D$ is an embedding for a 2-connected graph, we can use Lemma 26 to show that $e(n(d))$ and $d$ are the only darts from the $f$-orbit of $f(d)$ that are not in $P$. Thus, the claim follows from the definition of $f'$ since $n^{-1}(e(n(d))) = f(n(d))$. ◀

Note that the proof above uses Lemma 26 for the second time. When we use the lemma in step (4) of the proof of Proposition 7, we apply it to the 3-connected graph $G/xy$, exploiting that $G/xy - v_{xy}$ is still 2-connected, which in turn allows us to argue that the obtained face containing all the neighbors is bounded by a duplicate-free cycle (cf. step (5) and Theorem 25).

Finally, we justify step (7) of Proposition 7, which amounts to two applications of the lemma below, where $G + (z, A)$ is a the simple graph $G$ extended with a new vertex $z$ which is made adjacent to all vertices in the set $A$.
17:14 A Variant of Wagner's Theorem Based on Combinatorial Hypermaps

**Lemma 29.** Let $g: D \to G$ be a plane embedding, let $[x] \dashv p \dashv [y] \dashv q$ be a face of $g$, and let $\{x, y\} \subseteq A \subseteq \{x, y\} \cup p$. Then there exists a plane embedding of $G + (z, A)$ with a face $[x, z, y] \dashv q$.

**Proof.** We first show that for every face $[u] \dashv s$ under some embedding, one can add a single vertex $v$ and obtain an embedding of $G + (v, \{u\})$ with face $[u, v, u] \dashv s$. Moreover, one can always add an edge across a face, splitting a face $[u] \dashv s_1 \dashv [v] \dashv s_2$ into two faces $[v, u] \dashv s_1$ and $[u, v] \dashv s_2$. In each case, we show that the operation can be reversed by a genus-preserving double Walkup operation, showing that the initial addition preserves the genus. The claim then follows by first adding $z$ and the $xz$-edge and then adding the remaining edges in the order in which they appear in $p \dashv [y]$. ◀

This finishes the justification for the individual steps of the proof of Proposition 7. We remark that Lemmas 28 and 29 are “lossy” in that we do not prove that the untouched part of the embedding remains the same. This would only clutter the statements and is not needed for our purposes. Should the need arise, it would be straightforward to turn the underlying constructions into definitions and provide multiple lemmas, as we do with isomorphisms [8].

8 Combining Plane Embeddings

It remains to give a formal account of the combinations of plane embeddings performed in the proof of Theorem 8. That is, we need to be able to glue two plane embeddings together, either along a shared vertex or along a shared edge, the latter being used in the case outlined in the informal proof sketch of Theorem 8 given in Section 3.

It is straightforward to show that disjoint unions of planar hypermaps are again planar. As a consequence, both gluing operations can be reduced to obtaining a plane embedding for $G/xy$ from a plane embedding for $G$. Here, gluing along an edge amounts to merging the respective ends of the two edges one by one. On hypermaps, merging two nodes only changes the node and face permutations, leaving the type of darts and the edge permutation unchanged. Moreover, both the change to the node permutation and the change for the face permutation can be expressed in terms of a single successor-swapping operation.

Let $f: T \to T$ be an injective function over a finite type $T$ and let $x \neq y$.

$$ \text{switch}[x, y, f](z) := \begin{cases} fy & \text{if } z = x \\ fx & \text{if } z = y \\ fz & \text{otherwise} \end{cases} $$

The behavior of `switch[x, y, f]` is to either link two $f$-cycles (if $x$ and $y$ are on different $f$-cycles, as in the drawing above) or to separate an $f$-cycle into two cycles (if $x$ and $y$ are on the same $f$-cycle). Further, we have that

$$ \text{merge} \langle D, e, n, f \rangle d_1 d_2 := \langle D, e, \text{switch}[d_1, d_2, n], \text{switch}[f^{-1}d_2, f^{-1}d_1, f] \rangle $$

is a hypermap. If $d_1$ and $d_2$ are darts from different node cycles, `merge D d_1 d_2` merges said node cycles, adapting the face cycles accordingly. In particular, `merge D d_1 d_2` preserves the genus of $D$ if either $d_1$ and $d_2$ lie on a common face cycle or if $d_1$ and $d_2$ are from separate components of $D$. In the first case, $N$ is decreased by one while $F$ increases by one; in the second case, both $N$ and $F$ are decreased by one, but so is $C$.
If $g: D \to G$ is an embedding of some graph $G$, then for all $x, y: G$ that are not adjacent, and for all $d_x$ and $d_y$ such that $g d_x = x$ and $g d_y = y$, **merge** $D d_1 d_2$ can be used to embed $G/xy$. If $x$ and $y$ lie common face of $g$, then $x$ and $y$ are the images of two darts $d_x$ and $d_y$ that lie on a common face cycle in $D$, and **merge** $D d_x d_y$ yields an embedding of $G/xy$. If $x$ and $y$ are not connected in $G$, any choice of preimages of $x$ and $y$ will yield a plane embedding of $G/xy$. Hence, for gluing two embeddings together on a single vertex, we can make an arbitrary choice. For gluing along two edges $x-x'$ and $y-y'$ we know that there must be two faces $[x, x'] + s_1$ and $[y', y] + s_1$. Choosing $d_x$ and $d_y$ to be the preimages of $x$ and $y$ on the respective face cycles ensures that **merge** $D d_x d_y$ has an *f*-cycle containing preimages for $x'$ and $y'$, allowing us to obtain a plane embedding for $(G/xy)/x'y'$, which corresponds to gluing together two components of $G$ along the edges $x-x'$ and $y-y'$. Note that, due to Definition 20 allowing parallel edges, we do not need to remove darts when gluing along an edge. Putting everything together, we obtain the lemma used in the proof of Theorem 8:

**Lemma 30.** Let $G$ be a simple graph, and let $(V_1, V_2)$ be a separation, such that $V_1 \cap V_2 = \{x, y\}$ and $x \neq y$. If there are plane embeddings for $G[V_1]$ and $G[V_2]$, then there is also a plane embedding for $G$.

# 9 Main Results

Putting everything together, we obtain the following theorem, which corresponds exactly to the theorem formalized in Coq.

**Theorem 31.** Let $G$ be a $K_5$-free and $K_{3,3}$-free simple graph without isolated vertices. Then there exists a (combinatorial) plane embedding for $G$.

Theorem Wagner (G : sgraph) : no_isolated G ->
~ minor G 'K_3,3 /\ ~ minor G 'K_5 -> inhabited (planevo G).

Note that, compared with Theorem 8, we have the additional technical side condition that $G$ may not have isolated vertices. As mentioned in Remark 21, this is necessary, because hypermaps cannot represent isolated vertices. However, isolated vertices can often be treated separately without too much effort as exemplified below.

**Definition 32.** A (loopless) hypermap $\langle D, e, n, f \rangle$ is *k*-colorable if there is a coloring of its darts using at most *k* colors, such that for all *d* : *D*, the color of *e*(*d*) is different from the color of *d* and the color of *n*(*d*) is the same as the color of *d*. A simple graph is *k*-colorable, if there is a coloring of its vertices using at most *k* colors such that adjacent vertices have different colors.

**Theorem 33** ([9, 10]). Every planar loopless hypermap is 4-colorable

**Theorem 34.** Let $G$ be a $K_5$-free and $K_{3,3}$-free simple graph. Then $G$ is four-colorable.

*Proof.* Let $V$ be the set of vertices with nonempty neighborhood. We obtain a 4-coloring of $G[V]$ using Theorems 31 and 33. This coloring extends to a 4-coloring of $G$ by picking an arbitrary color for the isolated vertices. ◀
## 10 Conclusion and Future Work

We have introduced a combinatorial approximation of embeddings of graphs in the plane and proved that, with respect to this notion of plane embedding, every $K_5$-free and $K_{3,3}$-free graph without isolated vertices is planar. This corresponds to proving the mathematically interesting direction of Wagner's theorem and allows proving a structural variant of the four-color theorem that, unlike the formulations in [10], mentions neither hypermaps nor regions of the real plane. Instead, we bridge the gap between simple graphs and hypermaps, making the four-color theorem available to the setting of a more standard representation of graphs.

The main focus of this work was to bridge the aforementioned gap rather than provide a faithful proof of the usual formulation of Wagner's theorem. Nevertheless, we argue that Theorem 8 and its proof are actually quite faithful to the usual formulation. First, it seems plausible that the notion of plane embedding can be adapted to allow for isolated vertices by relaxing the surjectivity requirement, allowing isolated vertices to not have a dart mapped to them. However, this would come at the cost of some (minor) complications, as one could no longer define a partial inverse for every embedding. More importantly, key arguments of the proof (e.g., Theorems 11 and 25 and Lemmas 12 and 28) closely correspond to what one would find in a detailed paper proof [1, 5]. The main difference is that arguments about modifications of plane embeddings, many of which are normally handled informally, either vanish completely or are replaced by rigorous machine-checked proofs on hypermaps. It should be said that finding these proofs took considerable effort. Hypermaps are complex objects and, apart from the work of Gonthier [9, 10], there is little material in the literature on how to reason efficiently using hypermaps on paper and in an interactive theorem prover. Combined with the fact that some of the proofs are quite technical (e.g. Lemma 26), the learning curve is fairly steep. I hope that this work will contribute to making hypermaps more accessible.

Standing at around 7000 lines (counting additions to the preexisting graph-theory library), the Coq development accompanying this paper is substantial, increasing the total size of the library by more than a third. Around half of these additions deal with operations on hypermaps and plane embeddings. Both the total size and the fraction dealing with hypermaps are bigger than originally envisioned, and I hope that both can still be improved.

As mentioned in Section 1, we have only proved one direction of Wagner's theorem. It remains to show that graphs that can be represented using planar hypermaps have neither $K_5$ nor $K_{3,3}$ as a minor. It is relatively straightforward to show that a graph contains $K_5$ or $K_{3,3}$ as minor iff it contains an edge subdivision of $K_5$ or $K_{3,3}$ as a subgraph [5, Proposition 4.4.2]. This leads to a variant of Wagner's theorem known as Kuratowski's theorem. We have already proved that $K_5$ and $K_{3,3}$ do not have plane embeddings (cf. Proposition 23), and that planar graphs are closed under taking subgraphs (Lemma 27). Hence, Kuratowski's theorem and the converse direction of Wagner's theorem could be obtained by proving that planar graphs are closed under removing edge-subdivisions. This direction has already been formalized in Isabelle/HOL [13], and the main obstacle is that reasoning about contained subdivisions (i.e., topological minors) is more cumbersome than reasoning about (normal) minors.

Besides the converse direction of Wagner's theorem, there are many other related theorems that would make for interesting future work. It is well known that in the case of 3-connected planar graphs, all plane embeddings have the same structure [1, Theorem 10.28]. In our setting, this means that the embedding is unique up to isomorphisms of hypermaps. Further, a common strengthening of Proposition 7 is to show that one can obtain a plane embedding in which all inner faces are convex. This strengthening is not expressible using the hypermap
model of plane embeddings, and this raises the question whether one could introduce an abstract notion of plane embedding and instantiate it with hypermaps as well as models based on axiomatic geometry or embeddings in the real plane. On the other hand, given that the (combinatorial) plane embedding of a 3-connected planar graph is unique, it should also be possible to directly construct a convex embedding in the real plane for this hypermap, separating the existence and convexity parts of the proof.

References

1. Adrian Bondy and U.S.R. Murty. *Graph Theory*, volume 244 of *Graduate Texts in Mathematics*. Springer-Verlag London, 2008.

2. Ching-Tsun Chou. A formal theory of undirected graphs in higher-order logic. In *PHOL*, volume 859 of LNCS, pages 144–157. Springer, 1994. doi:10.1007/3-540-58450-1_40.

3. Ching-Tsun Chou. Mechanical verification of distributed algorithms in higher-order logic. In *The Computer Journal*, 38(2):152–161, January 1995. doi:10.1093/comjnl/38.2.152.

4. Robert Cori. *Un code pour les graphes planaires et ses applications*. PhD thesis, Univ. Paris VII, 1973.

5. Reinhard Diestel. *Graph Theory (2nd edition)*. Graduate Texts in Mathematics. Springer, 2000.

6. Christian Doczkal, Guillaume Combette, and Damien Pous. A formal proof of the minor-exclusion property for treewidth-two graphs. In Jeremy Avigad and Assia Mahboubi, editors, *Interactive Theorem Proving (ITP 2018)*, volume 10895 of LNCS, pages 178–195. Springer, 2018. doi:10.1007/978-3-319-94821-8_11.

7. Christian Doczkal and Damien Pous. Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. In *Proc. of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20)*, January 20–21, 2020, New Orleans, LA, USA, 2020. doi:10.1145/3372885.3373831.

8. Christian Doczkal and Damien Pous. Graph theory in Coq: Minors, treewidth, and isomorphisms. *J. Autom. Reason.*, 64(5):795–825, 2020. doi:10.1007/s10817-020-09543-2.

9. Georges Gonthier. A computer-checked proof of the four color theorem, 2005. URL: https://www.cl.cam.ac.uk/~lp15/Pages/4colproof.pdf.

10. Georges Gonthier. Formal proof — the four-color theorem. *Notices Amer. Math. Soc.*, 55(11):1382–1393, 2008. URL: http://www.ams.org/notices/200811/tx081101382p.pdf.

11. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean Mclaughlin, and Tat Thang Nguyen. A formal proof of the Kepler conjecture. *Forum of Mathematics, Pi*, 5, 2017. doi:10.1017/fmp.2017.1.

12. Yatsuka Nakamura and Piotr Rudnicki. Euler circuits and paths. *Formalized Mathematics*, 6(3):417–425, 1997.

13. Lars Noschinski. *Formalizing Graph Theory and Planarity Certificates*. PhD thesis, Technische Universität München, 2016.

14. Daniel E. Severín. Formalization of the domination chain with weighted parameters (short paper). In John Harrison, John O'Leary, and Andrew Tolmach, editors, *Interactive Theorem Provin (ITP 2019)*, volume 141 of LIPIcs, pages 36:1–36:7. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.ITP.2019.36.

15. Abhishek Kr Singh and Raja Natarajan. A constructive formalization of the weak perfect graph theorem. In *Proc. of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20)*, January 20–21, 2020, New Orleans, LA, USA, 2020. doi:10.1145/3372885.3373819.

16. Saul Stahl. A combinatorial analog of the Jordan curve theorem. *J. Comb. Theory, Ser. B*, 35(1):28–38, 1983. doi:10.1016/0095-8956(83)90078-3.

17. William T. Tutte. Duality and trinity. In *Colloquium Mathematical Society Janos Bolyai 10*, pages 1459–1472, 1975.

18. David W. Walkup. How many ways can a permutation be factored into two n-cycles? *Discret. Math.*, 28(3):315–319, 1979. doi:10.1016/0012-365X(79)90138-9.