TheoremStatement: 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.

$\overline{P_{5}}$ -free graphs admit a pure or $x$ -sparse polynomial blockade

Statement

There exists $d \geq 40$ such that for every $x \in (0, 2^{- d})$ and every $\overline{P_{5}}$ -free graph $G$ with $∣ V (G) ∣ \geq x^{- d}$ , there exists an integer $k \in [2, x^{- 1}]$ and either

a pure $(k, ∣ V (G) ∣ / k^{d})$ -blockade in $G$ ; or
an $x$ -sparse $(k, ∣ V (G) ∣ / k^{d})$ -blockade in $G$ .

Facts & Assumptions

Given: After the exponent $d$ is chosen below, a parameter $x \in (0, 2^{- d})$ and a $\overline{P_{5}}$ -free graph $G$ with $∣ V (G) ∣ \geq x^{- d}$ .

[L1]

Lemma 5.5 of the cited source supplies an exponent $D \geq 40$ such that, under its convention allowing a real blockade-length threshold, there is some $r \in [2, x^{- 1}]$ and a pure or $x$ -sparse $(r, ∣ V (G) ∣ / r^{D})$ -blockade whenever $x \in (0, 2^{- D})$ and $∣ V (G) ∣ \geq x^{- D}$ .

[F2]

In this library, the first parameter of an $(ℓ, w)$ -blockade must be a natural number, and the actual length is at least $ℓ$ (Blockades, their length, their width, and their support).

Proof

technique · translate the cited source theorem

1.1

Let $D \geq 40$ be supplied by [L1], and set $d : = 2 D$ . Fix $x$ and $G$ as in the Statement. Since $d \geq D$ , one has $x < 2^{- D}$ and $∣ V (G) ∣ \geq x^{- D}$ . Thus [L1] gives a real $r \in [2, x^{- 1}]$ and a pure or $x$ -sparse blockade whose actual length is at least $r$ and whose width is at least $∣ V (G) ∣ / r^{D}$ .

L1givenalgebra

2.1

Put $k : = ⌊ r ⌋$ . Then $k$ is an integer and $2 \leq k \leq r \leq x^{- 1}$ . The blockade's integral actual length, being at least $r$ , is in particular at least $k$ , as required by [F2].

step 1.1F2algebra

3.1

Since $k \geq 2$ and $k \leq r < k + 1$ , one has $r^{D} < (k + 1)^{D} \leq (3 k / 2)^{D} \leq k^{2 D} = k^{d}$ . Consequently $∣ V (G) ∣ / r^{D} \geq ∣ V (G) ∣ / k^{d}$ . The blockade from step 1.1 is therefore a pure or $x$ -sparse $(k, ∣ V (G) ∣ / k^{d})$ -blockade in the library's sense.

step 1.1step 2.1algebra

4.1

The chosen $d = 2 D$ satisfies $d \geq 40$ , and steps 1.1--3.1 prove the stated conclusion for every admissible $x$ and $G$ .

step 1.1step 3.1∎

Depends on

Used by

Dependency tree · two levels

14 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 5.5 (standard reference, not scraped)

P5‾P5​​-free graphs admit a pure or xx-sparse polynomial blockade