LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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.

Property (*) and leaf reducibility yield a long x-sparse or complete blockade, or a better outcome

Statement

Suppose that $F$ has property $(*)$ and that $F$ is leaf-reducible. Then there exist constants $c_{1}, c_{2}, c_{3} > 0$ and $c_{4}, c_{5} \geq 4$ such that, with $c : = 2^{- 4 c_{5}}$ , for every $0 < x \leq y \leq c$ and every $c y^{3}$ -restricted $\overline{F}$ -free graph $G$ , at least one of the following holds:

$G$ has an $x$ -sparse or complete blockade of length at least $y^{- 1}$ and width at least $y^{c_{4} + 2} ∣ G ∣$ ;
$G$ has a $2 y^{4}$ -restricted induced subgraph with at least $y^{c_{4} + 2} ∣ G ∣$ vertices;
$G$ has a clique or stable set of size at least $(x^{10} ∣ G ∣)^{c_{1}}$ ;
$G$ has a complete or anticomplete $(k, ∣ G ∣ / k^{c_{2} + 7 / c_{3}})$ -blockade for some real $k \geq y^{- c_{3}}$ ;
$G$ has a pure $(ℓ, ∣ G ∣ / ℓ^{9})$ -blockade for some real $ℓ \in [y^{- 1}, x^{- 2}]$ .

Facts & Assumptions

Given: A finite family $F$ with property $(*)$ and leaf-reducible, parameters $0 < x \leq y \leq c$ , and a $c y^{3}$ -restricted $\overline{F}$ -free graph $G$ .

[L1]

The five-outcome lemma provides constants $c_{1}, c_{2}, c_{3} > 0$ and $c_{4}, c_{5} \geq 4$ for $y^{3}$ -restricted graphs (Property (*) and leaf reducibility yield five comb outcomes in a restricted graph).

[L2]

If every induced subgraph $F$ of $G$ with $∣ F ∣ \geq c ∣ G ∣$ has disjoint sets $X, Y$ with $∣ X ∣ \geq y^{c_{4}} ∣ F ∣$ , $∣ Y ∣ \geq (1 - c_{5} y) ∣ F ∣$ , and $Y$ $x$ -sparse or complete to $X$ , then $G$ has an $x$ -sparse or complete blockade of length at least $y^{- 1}$ and width at least $y^{c_{4} + 2} ∣ G ∣$ (Large sparse-pair hypotheses yield an $x$ -sparse or complete blockade).

[L3]

If a graph is $c y^{3}$ -restricted and $F$ is an induced subgraph with $∣ F ∣ \geq c ∣ G ∣$ , then $F$ is $y^{3}$ -restricted ( $c$ -sparse, $c$ -dense and $c$ -restricted vertex sets).

Proof

Proof technique: either every large induced subgraph satisfies the large pair hypothesis of [L2], or choose a counterexample $F$ and apply the five-outcome lemma inside it.

1.1

Let $c_{1}, c_{2}, c_{3} > 0$ and $c_{4}, c_{5} \geq 4$ be the constants from [L1], and put $c : = 2^{- 4 c_{5}}$ .

L1choose

2.1

If $∣ G ∣ \leq y^{- (c_{4} + 2)}$ , then $y^{c_{4} + 2} ∣ G ∣ \leq 1$ . Any single vertex spans an induced subgraph that is $0$ -restricted, hence $2 y^{4}$ -restricted, so outcome 2 holds. Therefore we may assume $∣ G ∣ \geq y^{- (c_{4} + 2)}$ .

step 1.1givenalgebracases

2.2

[assume-case universal-pair] Suppose that every induced subgraph $F$ of $G$ with $∣ F ∣ \geq c ∣ G ∣$ has disjoint sets $X, Y$ with $∣ X ∣ \geq y^{c_{4}} ∣ F ∣$ , $∣ Y ∣ \geq (1 - c_{5} y) ∣ F ∣$ , and $Y$ $x$ -sparse or complete to $X$ . Then [L2] gives outcome 1.

step 1.1L2

2.3

[assume-case obstruction] Assume instead that there is an induced subgraph $F$ of $G$ with $∣ F ∣ \geq c ∣ G ∣$ for which no such pair $X, Y$ exists. By [L3], the graph $F$ is $y^{3}$ -restricted, so [L1] applies to $F$ . Because the first outcome of [L1] fails for this specific $F$ , one of the remaining four outcomes of [L1] holds inside $F$ .

step 1.1L1L3

3.1

If [L1] gives a $2 y^{4}$ -restricted induced subgraph of $F$ with at least $y^{c_{4}} ∣ F ∣$ vertices, then that subgraph has at least $y^{c_{4}} c ∣ G ∣ = y^{c_{4} + 1} ∣ G ∣ \geq y^{c_{4} + 2} ∣ G ∣$ vertices because $y \leq c < 1$ . Hence outcome 2 holds in $G$ .

step 2.3L1algebra

3.2

If [L1] gives a clique or stable set of size at least $(x^{9} ∣ F ∣)^{c_{1}}$ , then $(x^{9} ∣ F ∣)^{c_{1}} \geq (x^{9} \cdot c ∣ G ∣)^{c_{1}} \geq (x^{9} \cdot x ∣ G ∣)^{c_{1}} = (x^{10} ∣ G ∣)^{c_{1}},$ because $x \leq y \leq c$ . So outcome 3 holds.

step 2.3L1algebra

3.3

If [L1] gives a complete or anticomplete $(k, ∣ F ∣ / k^{c_{2} + 6 / c_{3}})$ -blockade with $k \geq y^{- c_{3}}$ , then $\frac{∣ F ∣}{k^{c_{2} + 6 / c_{3}}} \geq \frac{c ∣ G ∣}{k^{c_{2} + 6 / c_{3}}} \geq \frac{y ∣ G ∣}{k^{c_{2} + 6 / c_{3}}} \geq \frac{∣ G ∣}{k^{c_{2} + 7 / c_{3}}},$ because $k \geq y^{- c_{3}}$ implies $k^{1 / c_{3}} \geq y^{- 1}$ . Hence outcome 4 holds.

step 2.3L1algebra

3.4

If [L1] gives a pure $(ℓ, ∣ F ∣ / ℓ^{8})$ -blockade with $ℓ \in [y^{- 1}, x^{- 2}]$ , then $\frac{∣ F ∣}{ℓ^{8}} \geq \frac{c ∣ G ∣}{ℓ^{8}} \geq \frac{y ∣ G ∣}{ℓ^{8}} \geq \frac{∣ G ∣}{ℓ^{9}},$ again because $ℓ \geq y^{- 1}$ . Thus outcome 5 holds.

step 2.3L1algebra

4.1

The exhaustive alternatives 2.1 and 2.2, together with steps 3.1-3.4, show that one of the five stated outcomes always holds.

step 2.2step 2.3step 3.1step 3.2step 3.3step 3.4cases-exhaustive∎

Depends on

Used by

Under failure of the global outcomes, a large y^(10/3)-restricted induced subgraph forces a y^(11/3)-restricted induced subgraph Lemma

Dependency tree · two levels

15 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

Shenwei Huang, Yiao Ju, and Yidong Zhou, Erdős-Hajnal beyond the five-vertex path, Lemma 4.2 (standard reference, not scraped)
Tung Nguyen, Alex Scott, and Paul Seymour, Induced subgraph density. VII. The five-vertex path, Lemma 7.2 (standard reference, not scraped)