The extremal function for $K_9^=$ minors

TL;DR

This paper determines the maximum number of edges in large graphs that do not contain a specific minor, namely $K_9^=$, and characterizes the structure of extremal graphs, using both theoretical and computational methods.

Contribution

The paper establishes the extremal function for $K_9^=$ minors and characterizes the extremal graphs, combining theoretical proofs with computer-assisted lemmas.

Findings

Graphs with at least 6n - 20 edges contain a $K_9^=$ minor or are structurally specific.

Identifies extremal graphs formed from disjoint copies of $K_8$ and $K_{2,2,2,2,2}$.

Uses computer assistance to prove key lemmas.

Abstract

We prove the extremal function for $K_9^=$ minors, where $K_9^=$ denotes the complete graph $K_9$ with two edges removed. In particular, we show that any graph with $n$ vertices and at least $6n - 20$ edges either contains a $K_9^=$ minor or is isomorphic to a graph obtained from disjoint copies of $K_8$ and $K_{2, 2, 2, 2, 2}$ by identifying cliques of size 5. We utilize computer assistance to prove one of our lemmas.