Challenge 5: the Erdős–Hajnal property for the path $P_r$

Read-back of the definition TenChallenges.statement_05.

For a natural number $r \in \{0, 1, 2, \dots\}$, the proposition $\mathrm{statement\_05}(r)$ is defined as $\mathrm{ErdosHajnalConjectureFor}(P_r)$, where $P_r$ is Mathlib's path graph on $r$ vertices: its vertex set is $\{0, 1, \dots, r-1\}$ (the type of natural numbers below $r$), and two vertices $i, j$ are adjacent exactly when $i + 1 = j$ or $j + 1 = i$ (it is the Hasse diagram of the linear order on $\{0,\dots,r-1\}$, i.e. the graph of the covering relation). Thus $P_r$ has $r$ vertices and $r - 1$ edges for $r \ge 1$; it is indexed by its number of vertices, not edges. In particular $P_0$ is the graph with no vertices, $P_1$ is a single isolated vertex, $P_2$ is a single edge, and $P_3$ is a path with two edges.

Unfolding $\mathrm{ErdosHajnalConjectureFor}(P_r)$ in full, $\mathrm{statement\_05}(r)$ asserts:

Binder by binder:

• $c$: there exists a real number $c$ with $0 < c$ (strict, no upper bound); $c$ may depend on $r$ but is fixed before $V$ and $G$ are chosen, so one $c$ must serve all $V, G$ below.
• $V$: for every type $V$ in the lowest universe (ordinary sets) equipped with a finiteness structure, i.e. every finite vertex set, the empty set included.
• $G$: for every simple graph $G$ on $V$ (irreflexive symmetric adjacency $\sim_G$).
• Hypothesis $P_r \not\trianglelefteq G$: there is no graph embedding of $P_r$ into $G$, where a graph embedding is an injective map $f : \{0,\dots,r-1\} \to V$ with $f(i) \sim_G f(j)$ if and only if $|i - j| = 1$, for all $i, j$. Concretely: $G$ does not contain $r$ distinct vertices $v_0, \dots, v_{r-1}$ such that $v_i \sim_G v_{i+1}$ for all $0 \le i \le r-2$ and $v_i \not\sim_G v_j$ whenever $|i - j| \ge 2$. That is, $G$ has no induced path on $r$ vertices (no chordless path with $r$ vertices). A path on $r$ vertices that carries extra edges (chords) among its vertices is not excluded by the hypothesis.
• Conclusion: there exists a finite set $s$ of vertices (possibly empty) such that either every two distinct elements of $s$ are adjacent in $G$ ($s$ is a clique of $G$), or every two distinct elements of $s$ are non-adjacent in $G$ ($s$ is a clique of the complement $\overline{G}$, whose adjacency is "$u \ne v$ and $u \not\sim_G v$", i.e. $s$ is an independent set of $G$); and, as real numbers,

with $|s|$ the number of elements of $s$, $|V|$ the number of vertices of $G$, non-strict inequality, and $x^{c}$ the real power ($e^{c \ln x}$ for $x > 0$; $0^{c} = 0$ since $c > 0$).

Degenerate values of $r$ and other edge cases:

• $r = 0$: $P_0$ has no vertices, so the empty map embeds $P_0$ into every $G$; the hypothesis $P_0 \not\trianglelefteq G$ is never satisfied and the universal part holds vacuously; $\mathrm{statement\_05}(0)$ reduces to "there exists a real $c > 0$", which is true.
• $r = 1$: $P_1$ is one vertex, which embeds into $G$ exactly when $V \ne \varnothing$; so the hypothesis holds only for $V = \varnothing$, where $|V|^{c} = 0$ and $s = \varnothing$ (vacuously a clique of $G$ and of $\overline{G}$) satisfies the conclusion.
• $r = 2$: $P_2$ is a single edge, which embeds into $G$ exactly when $G$ has at least one edge; so the hypothesis says $G$ is edgeless, and then $s = V$ is an independent set of size $|V|$.
• For any $r$: $V$ may be empty (then $|V|^{c} = 0$ and $s = \varnothing$ works); $s = \varnothing$ and singletons are vacuously both cliques and independent sets, so whenever $|V|^{c} \le 1$ the conclusion is met trivially.