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.

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

Statement

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

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

Facts & Assumptions

Given: A finite family $F$ with property $(*)$ and leaf-reducible, a parameter $x \in (0, 2^{- d})$ , and an $\overline{F}$ -free graph $G$ with $∣ G ∣ \geq x^{- d}$ .

[L1]

The constant-scale four-outcome theorem gives constants $c_{1}, c_{2}, c_{3} > 0$ , $c_{4}, c_{5} \geq 4$ , and $c : = 2^{- 4 c_{5}}$ such that every $c^{10}$ -restricted $\overline{F}$ -free graph satisfies one of the four outcomes on the current page (Constant-scale restricted property (*) yields a restricted subgraph, a polynomial clique or stable set, or two blockade alternatives).

[L2]

For $ξ : = c^{10}$ , every $\overline{F}$ -free graph has a $ξ$ -restricted induced subgraph of size at least $δ ∣ G ∣$ for some $δ > 0$ (Rödl: for every $H$ and every $ϵ \in (0, \frac{1}{2})$ there is $δ > 0$ such that every nonempty $H$ -free graph has an $ϵ$ -restricted vertex set of size at least $δ ∣ V (G) ∣$ ).

Proof

technique · apply Rödl at the fixed scale $\xi=c^{10}$, then transfer each outcome of the constant-scale theorem back to $G$ by choosing $d$ large enough

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 [L1], and set $ξ : = c^{10}$ . Let $δ > 0$ be the constant from [L2] for the family $\overline{F}$ and the parameter $ξ$ .

L1L2choose

2.1

Choose $d$ so large that $d \geq 58 c_{4}, 2^{- d} < c^{10}, δ \geq 2^{116 c_{4} - d}, δ \geq 2^{c_{2} + 27 c_{4} / c_{3} - d} .$

step 1.1choose

3.1

By [L2], the graph $G$ has a $ξ$ -restricted induced subgraph $F \subseteq G$ with $∣ F ∣ \geq δ ∣ G ∣$ . Since $x < 2^{- d} < ξ$ , the parameter $x$ lies in the range allowed by [L1], so [L1] applies to $F$ .

step 2.1L1L2

4.1

If [L1] gives an $x$ -restricted induced subgraph of $F$ with at least $x^{22 c_{4}} ∣ F ∣$ vertices, then $x^{22 c_{4}} ∣ F ∣ \geq x^{22 c_{4}} δ ∣ G ∣ \geq x^{22 c_{4}} 2^{58 c_{4} - d} ∣ G ∣ \geq x^{23 c_{4}} ∣ G ∣,$ because $x < 2^{- d}$ implies $x^{c_{4}} \leq 2^{58 c_{4} - d}$ . Thus outcome 1 holds.

step 2.1step 3.1L1algebra

4.2

If [L1] gives a clique or stable set of size at least $(x^{30 c_{4}} ∣ F ∣)^{c_{1}}$ , then the same estimate yields $(x^{30 c_{4}} ∣ F ∣)^{c_{1}} \geq (x^{31 c_{4}} ∣ G ∣)^{c_{1}}$ , so outcome 3 holds.

step 2.1step 3.1L1algebra

4.3

If [L1] gives a complete or anticomplete $(k, ∣ F ∣ / k^{c_{2} + 27 c_{4} / c_{3}})$ -blockade with $k \geq 2$ , let $j : = ⌈ k ⌉$ . Its actual length is integral and at least $k$ , hence at least $j$ , while $\frac{∣ F ∣}{k^{c_{2} + 27 c_{4} / c_{3}}} \geq \frac{δ ∣ G ∣}{k^{c_{2} + 27 c_{4} / c_{3}}} \geq \frac{∣ G ∣}{k^{d}} \geq \frac{∣ G ∣}{j^{d}} .$ Thus the same blocks form a complete or anticomplete $(j, ∣ G ∣ / j^{d})$ -blockade. If $j \geq x^{- 1}$ this is outcome 4; if $j < x^{- 1}$ , then the integer $j \in [2, x^{- 1}]$ gives outcome 2.

step 2.1step 3.1L1algebrachoosecases

4.4

If [L1] gives a pure or $x$ -sparse $(ℓ, ∣ F ∣ / ℓ^{29 c_{4}})$ -blockade with $ℓ \in [c^{- 1}, x^{- 2}]$ , set $k : = ⌊ \sqrt{ℓ} ⌋ .$ Then $k$ is an integer in $[2, x^{- 1}]$ , because $ℓ \geq c^{- 1} \geq 2^{4}$ and $\sqrt{ℓ} \leq x^{- 1}$ . The blockade has length at least $ℓ \geq k$ , and $ℓ < (k + 1)^{2} \leq 4 k^{2}$ , so $\frac{∣ F ∣}{ℓ^{29 c_{4}}} \geq \frac{∣ F ∣}{(4 k^{2})^{29 c_{4}}} = \frac{∣ F ∣}{2^{58 c_{4}} k^{58 c_{4}}} \geq \frac{δ ∣ G ∣}{2^{58 c_{4}} k^{58 c_{4}}} \geq \frac{∣ G ∣}{k^{d}},$ because $k \geq 2$ and step 2.1 gives $δ \geq 2^{116 c_{4} - d}$ . Hence outcome 2 holds.

step 2.1step 3.1L1algebrachoose

5.1

The four branches 4.1-4.4 exhaust the conclusion of [L1], so one of the stated outcomes always holds for $G$ .

step 3.1step 4.1step 4.2step 4.3step 4.4cases-exhaustive∎

Depends on

Used by

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

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