CorollaryStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every $P_{4}$ -free graph has a clique or stable set of size at least the square root of its order

Statement

If $G$ is a finite $P_{4}$ -free graph on $n$ vertices, then $G$ contains a clique or a stable set of size at least $\sqrt{n}$ .

Facts & Assumptions

Given: A finite $P_{4}$ -free graph $G$ on $n$ vertices.

[L1]

Every induced subgraph of a $P_{4}$ -free graph is again $P_{4}$ -free ( $H$ -free and $F$ -free graphs under the induced-subgraph convention).

[L2]

Every nontrivial $P_{4}$ -free graph is disconnected or has disconnected complement (Every nontrivial $P_{4}$ -free graph is disconnected or has disconnected complement).

[L3]

Connected components partition the vertex set, and anticomponents do too (The connected components of a graph partition its vertex set and are its maximal connected subgraphs, The anticonnected components of $G$ are exactly the connected components of $\overline{G}$ ).

[L4]

Distinct connected components are anticomplete, and distinct anticomponents are complete (Distinct connected components are anticomplete, and distinct anticonnected components are complete).

[L5]

The clique number and stability number are $ω (G)$ and $α (G)$ (Cliques, stable sets, the clique number $ω (G)$ and stability number $α (G)$ ).

Proof

technique · direct

1.1

We prove by induction on $n$ the stronger statement $α (G) ω (G) \geq n$ . If $n \leq 1$ , then $α (G) = 1$ when $n = 1$ and $α (G) = ω (G) = 0$ when $n = 0$ , so the inequality is immediate.

givenbase

2.1

Assume $n \geq 2$ . By [L2], either $G$ is disconnected or $\overline{G}$ is disconnected.

step 1.1L2

3.1

Suppose first that $G$ is disconnected. By [L3], choose a connected component $C$ of $G$ and let $D : = V (G) ∖ C$ ; then $C$ and $D$ are nonempty, $G [C]$ and $G [D]$ are induced subgraphs of $G$ , and [L4] makes $C$ anticomplete to $D$ . By [L1] both induced subgraphs are $P_{4}$ -free, so the induction hypothesis gives $α (G [C]) ω (G [C]) \geq ∣ C ∣$ and $α (G [D]) ω (G [D]) \geq ∣ D ∣$ . A stable set in $G [C]$ together with a stable set in $G [D]$ is still stable in $G$ , while every clique of $G$ lies in one side. Hence $α (G) \geq α (G [C]) + α (G [D])$ and $ω (G) \geq \max {ω (G [C]), ω (G [D])}$ , so $α (G) ω (G) \geq α (G [C]) ω (G [C]) + α (G [D]) ω (G [D]) \geq ∣ C ∣ + ∣ D ∣ = n$ .

step 2.1L1L3L4ihalgebra

3.2

Suppose instead that $\overline{G}$ is disconnected. By [L3], choose an anticomponent $C$ of $G$ and let $D : = V (G) ∖ C$ ; then $C$ and $D$ are nonempty, the induced subgraphs $G [C]$ and $G [D]$ are $P_{4}$ -free by [L1], and [L4] makes $C$ complete to $D$ . The induction hypothesis again yields $α (G [C]) ω (G [C]) \geq ∣ C ∣$ and $α (G [D]) ω (G [D]) \geq ∣ D ∣$ . Now a clique in $G [C]$ together with a clique in $G [D]$ is a clique in $G$ , while every stable set of $G$ lies in one side. Thus $ω (G) \geq ω (G [C]) + ω (G [D])$ and $α (G) \geq \max {α (G [C]), α (G [D])}$ , and again $α (G) ω (G) \geq ∣ C ∣ + ∣ D ∣ = n$ .

step 2.1L1L3L4ihalgebra

4.1

Steps 3.1 and 3.2 prove $α (G) ω (G) \geq n$ . Since $\max {α (G), ω (G)}^{2} \geq α (G) ω (G)$ , one obtains $\max {α (G), ω (G)} \geq \sqrt{n}$ . By [L5], this says that $G$ has a clique or a stable set of size at least $\sqrt{n}$ .

step 3.1step 3.2L5algebradischarge-induction∎

Depends on

Used by

The strong Erdős–Hajnal property implies the Erdős–Hajnal property Theorem

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Tung H. Nguyen, Notes on Recent Work on the Erdős-Hajnal Conjecture, Exercise 1.1 (standard reference, not scraped)

Every P4P4​-free graph has a clique or stable set of size at least the square root of its order