Erdős–Hajnal for the five-vertex path

Read-back of TenChallenges.challenge_05_r5. The declaration asserts the proposition $\mathrm{statement}_{05}(5)$, which by definition is the bundle's predicate ErdosHajnalConjectureFor applied to Mathlib's path graph $P_{5}$; the parameter is fixed to $n = 5$ throughout.

The fixed graph $P_n$. $P_n$ is the simple graph whose vertex set is $\{0, 1, \dots, n-1\}$ (the finite type with $n$ elements) and in which two vertices $i, j$ are adjacent iff $i + 1 = j$ or $j + 1 = i$ (as natural numbers). With $n = 5$ this is the path $0 - 1 - 2 - 3 - 4$: $5$ vertices and the $4$ edges $\{0,1\}, \{1,2\}, \{2,3\}, \{3,4\}$. It is an undirected simple graph; the vertices $0$ and $n-1$ are its two endpoints.

What is asserted. There exists a real number $c$ with

such that for every set $V$ (an arbitrary type, implicit argument) equipped with a finiteness structure (so $V$ is a finite set of vertices, possibly empty) and for every simple graph $G$ with vertex set $V$ (symmetric irreflexive adjacency $\sim_G$; no loops, no multiple edges):

if $P_n$ is not inducedly contained in $G$, then there exists a finite subset $S \subseteq V$ such that

The pieces mean the following.

• "$P_n$ is inducedly contained in $G$" (Mathlib's relation $P_n \trianglelefteq G$) means that there exists a graph embedding of $P_n$ into $G$: an injective map $f : \{0, \dots, n-1\} \to V$ such that for all $a, b$,

i.e. $G$ contains an induced subgraph isomorphic to $P_n$ (the images of consecutive path vertices are adjacent, and the images of non-consecutive path vertices are non-adjacent). The hypothesis is the negation: $G$ contains no induced copy of $P_n$ (it is "induced-$P_n$-free"). For graphs $G$ that do contain an induced $P_n$ the hypothesis fails, so nothing is asserted about them. Non-induced copies of $P_n$ (a path whose image has extra chords in $G$) are not excluded by the hypothesis.

• "$S$ is a clique of $G$" (Mathlib's IsClique) means that any two distinct elements of $S$ are adjacent in $G$. $G^{c}$ is the complement graph: $u \sim_{G^c} v$ iff $u \ne v$ and $u \not\sim_G v$. So "$S$ is a clique of $G^c$" means any two distinct elements of $S$ are non-adjacent in $G$, i.e. $S$ is an independent (stable) set of $G$. The disjunction is inclusive. The empty set and every one-element set are cliques of both $G$ and $G^c$.
• $|S| \ge |V|^{c}$ is an inequality of real numbers: the cardinality of $S$ (a natural number, cast to $\mathbb{R}$) is at least $|V|$ (the number of vertices of $G$, cast to $\mathbb{R}$) raised to the real exponent $c$. For $|V| \ge 1$ this is the usual positive real $|V|^c = \exp(c \ln |V|)$. If $V$ is empty, then $|V|^c = 0^c = 0$ because $c \ne 0$, and $S = \emptyset$ satisfies the conclusion. The inequality is non-strict.

Quantifier structure and edge cases. The order is $\exists c > 0 \;\; \forall V \;\; \forall G \;\; (\text{hypothesis} \Rightarrow \exists S \dots)$: a single constant $c$ must be chosen before $V$ and $G$ and must work uniformly for every finite induced-$P_n$-free graph; $c$ may depend only on the fixed $n = 5$. No upper bound on $c$ is imposed (any positive real is allowed, including $c > 1$), and $S$ is not required to be maximal or to be a clique and independent set simultaneously. Nothing else is assumed about $G$: it may be edgeless, complete, disconnected, or have a single vertex. The declaration does not say anything about path graphs with a different number of vertices, nor about non-induced containment.