LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 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 either sparsifies further or yields a pure blockade or a large sparse pair

Statement

Let $x, y > 0$ with $x \leq y \leq 2^{- 8}$ , and let $G$ be a $y^{3}$ -sparse $\overline{P_{5}}$ -free graph with $∣ V (G) ∣ \geq y^{- 4}$ . Then at least one of the following holds:

$G$ is $2 y^{4}$ -sparse;
there exists an integer $k \in [y^{- 1 / 4}, 1 / x]$ and a pure $(k, ∣ V (G) ∣ / k^{26})$ -blockade in $G$ ; or
there are disjoint sets $X, Y \subseteq V (G)$ such that $∣ X ∣ \geq y^{4} ∣ V (G) ∣$ , $∣ Y ∣ \geq (1 - 4 y) ∣ V (G) ∣$ , and $Y$ is $x$ -sparse to $X$ .

Facts & Assumptions

Given: Parameters $x, y$ and a graph $G$ satisfying the displayed hypotheses.

[L1]

Lemma 5.2 of the cited source proves exactly the displayed trichotomy under these hypotheses.

Proof

technique · translate the cited source lemma

1.1L1given

The cited source lemma proves exactly the three displayed alternatives under these hypotheses.

2.1step 1.1∎

Therefore the present trichotomy holds.

Depends on

Used by

An x-sparse blockade iteration yields further sparsification or a pure blockade Lemma

Dependency tree · two levels

19 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.2 (standard reference, not scraped)

A sparse P5‾P5​​-free graph either sparsifies further or yields a pure blockade or a large sparse pair