LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-31

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.

A sparse $\overline{P_{5}}$ -free graph yields deeper sparsification or a complete blockade or a large anticomplete set

Statement

There exists a constant $d \geq 40$ such that, for every $y \in (0, \frac{1}{2})$ and every $y$ -sparse $\overline{P_{5}}$ -free graph $G$ , at least one of the following holds:

there is a set $S \subseteq V (G)$ with $∣ S ∣ \geq y^{30 d^{3}} ∣ V (G) ∣$ such that $G [S]$ is $y^{2 d}$ -sparse;
there is a complete $(y^{- 1}, y^{33 d^{3}} ∣ V (G) ∣) -blockade$ in $G$ ; or
there are disjoint sets $X, Y \subseteq V (G)$ such that $∣ X ∣ \geq y^{33 d^{3}} ∣ V (G) ∣, ∣ Y ∣ \geq (1 - 3 y) ∣ V (G) ∣,$ and $X$ is anticomplete to $Y$ .

Facts & Assumptions

Given: A parameter $y \in (0, \frac{1}{2})$ and a $y$ -sparse $\overline{P_{5}}$ -free graph $G$ .

[F1]

Lemma 7.1 of Nguyen, Scott, and Seymour's cited paper states the displayed trichotomy, with the same constant $d \geq 40$ and the same exponents and blockade parameters.

[F2]

In the proof of that lemma, Claim 7.1.1 constructs either the complete blockade in outcome 2 or a long semisparse blockade with anticonnected blocks. Claim 7.1.2 shows that a vertex mixed on many of those blocks yields outcome 1; otherwise averaging over the blocks gives a block anticomplete to a set of size at least $(1 - 3 y) ∣ V (G) ∣$ , which is outcome 3.

Proof

technique · translate the cited source lemma

1.1

Apply [F1] to the graph in the Given. Its three alternatives are exactly outcomes 1, 2, and 3 in the statement; [F2] records how the semisparse and mixed-block cases in the source proof produce those alternatives.

F1F2givencases

2.1

Therefore the present trichotomy holds.

step 1.1∎

Depends on

Used by

A sparse P₅-free graph yields a complete or anticomplete blockade or a sparser subgraph Lemma

Dependency tree · two levels

16 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 Nguyen, Alex Scott, and Paul Seymour, Induced subgraph density. VII. The five-vertex path, Lemma 7.1 (standard reference, not scraped)

A sparse P5‾P5​​-free graph yields deeper sparsification or a complete blockade or a large anticomplete set