LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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.

Constant-scale restricted property (*) yields a restricted subgraph, a polynomial clique or stable set, or two blockade alternatives

Statement

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

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

Facts & Assumptions

Given: A finite family $F$ with property $(*)$ and leaf-reducible, an $x \in (0, c^{10}]$ , and a $c^{10}$ -restricted $\overline{F}$ -free graph $G$ .

[L1]

The previous claim says that, under the failure of outcomes 2-4, every $y^{10 / 3}$ -restricted induced subgraph of sufficiently large relative size has a deeper $y^{11 / 3}$ -restricted induced subgraph (Under failure of the global outcomes, a large y^(10/3)-restricted induced subgraph forces a y^(11/3)-restricted induced subgraph).

[L2]

If a graph has a $c^{10}$ -restricted induced subgraph of size at least $(c^{10})^{3 (c_{4} + 2)} ∣ G ∣$ and every $λ$ -restricted induced subgraph of size at least $λ^{3 (c_{4} + 2)} ∣ G ∣$ contains a $λ^{11 / 10}$ -restricted induced subgraph of size at least $λ^{3 (c_{4} + 2) / 10}$ times as many vertices, then the graph has an $x^{10 / 3}$ -restricted induced subgraph with at least $x^{11 (c_{4} + 2)} ∣ G ∣$ vertices (Iterated restricted sparsification reaches the target scale).

[L3]

If a set is $x^{10 / 3}$ -restricted, then it is $x$ -restricted ( $c$ -sparse, $c$ -dense and $c$ -restricted vertex sets).

Proof

Proof technique: if outcomes 2-4 fail, verify the hypotheses of the iterative restricted-sparsification lemma with $b_{1} = \frac{11}{10}$ , $b_{2} = 3 (c_{4} + 2)$ , and $b_{3} = \frac{3 (c_{4} + 2)}{10}$ .

1.1

Let $c_{1}, c_{2}, c_{3} > 0$ , $c_{4}, c_{5} \geq 4$ , and $c : = 2^{- 4 c_{5}}$ be the constants from Under failure of the global outcomes, a large y^(10/3)-restricted induced subgraph forces a y^(11/3)-restricted induced subgraph, and set $b_{1} : = 11 / 10, b_{2} : = 3 (c_{4} + 2), b_{3} : = 3 (c_{4} + 2) / 10.$

L1choose

1.2

Suppose outcomes 2, 3, and 4 all fail. We will show that outcome 1 then holds.

givenassume-contra

2.1

Hypothesis 1 of [L2] is immediate: the graph $G$ itself is $c^{10}$ -restricted and has size $∣ G ∣ \geq (c^{10})^{b_{2}} ∣ G ∣$ because $b_{2} > 0$ and $c^{10} < 1$ .

step 1.1L2givenalgebra

2.2

Let $λ \in [x^{10 / 3}, c^{10}]$ and let $F$ be a $λ$ -restricted induced subgraph of $G$ with $∣ F ∣ \geq λ^{b_{2}} ∣ G ∣$ . Write $λ = y^{10 / 3}$ , so $y = λ^{3 / 10} \in [x, c^{3}]$ . Then $∣ F ∣ \geq y^{10 (c_{4} + 2)} ∣ G ∣$ . Since outcomes 2-4 fail globally, [L1] applied with this $y$ gives a $y^{11 / 3} = λ^{11 / 10}$ -restricted induced subgraph of $F$ with at least $y^{c_{4} + 2} ∣ F ∣ = λ^{b_{3}} ∣ F ∣$ vertices.

step 1.1step 1.2L1L2algebra

2.3

The exponent condition for [L2] holds because $b_{1} b_{2} = \frac{11}{10} \cdot 3 (c_{4} + 2) = \frac{33 (c_{4} + 2)}{10} \geq \frac{30 (c_{4} + 2)}{10} = b_{2} + b_{3} .$

step 1.1L2algebra

3.1

Therefore [L2] yields an $x^{10 / 3}$ -restricted induced subgraph $S \subseteq G$ with at least $(x^{10 / 3})^{b_{1} b_{2}} ∣ G ∣ = x^{11 (c_{4} + 2)} ∣ G ∣$ vertices. Since $c_{4} \geq 4$ , the exponent satisfies $11 (c_{4} + 2) \leq 22 c_{4}$ , so $∣ S ∣ \geq x^{22 c_{4}} ∣ G ∣$ . By [L3], the subgraph $S$ is $x$ -restricted. Hence outcome 1 holds.

step 2.1step 2.2step 2.3L2L3algebra

4.1

Outcome 1 follows whenever outcomes 2-4 fail. Hence at least one of the four stated outcomes always holds.

step 1.2step 3.1discharge-contradiction∎

Depends on

Used by

Rödl initialization removes the constant-scale restriction in the property (*) four-outcome theorem Lemma

Dependency tree · two levels

9 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.3 (standard reference, not scraped)
Tung H. Nguyen, Notes on Recent Work on the Erdős-Hajnal Conjecture, Lemma 5.3 (standard reference, not scraped)