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 has a large nearly covered 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}$ . Suppose that $G$ is not $2 y^{4}$ -sparse, and that there do not exist 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$ . Then there exist disjoint sets $A, B \subseteq V (G)$ such that:

$∣ A ∣ \geq (1 - 3 y) ∣ V (G) ∣$ and $∣ B ∣ \geq y^{4} ∣ V (G) ∣$ ;
$A$ is $y^{2}$ -sparse to $B$ ; and
every vertex of $B$ has at least $x^{2} ∣ A ∣$ neighbours in $A$ .

Facts & Assumptions

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

[L1]

Claim 5.2.1 of the cited source proves exactly the displayed conclusion under these hypotheses after translating notation.

Proof

technique · translate the cited source claim

1.1L1given

The cited source claim proves exactly this large nearly covered sparse-pair conclusion after translating notation.

2.1step 1.1∎

Therefore the present statement follows.

Depends on

Used by

A sparse P₅-free graph either sparsifies further or yields a pure blockade or a large sparse pair Lemma

Dependency tree · two levels

8 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, Claim 5.2.1 (standard reference, not scraped)

A sparse P5‾P5​​-free graph has a large nearly covered sparse pair