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.

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

Statement

Let $F$ have property $(*)$ and be leaf-reducible, and let $c_{1}, c_{2}, c_{3} > 0$ , $c_{4}, c_{5} \geq 4$ , and $c : = 2^{- 4 c_{5}}$ be the constants from Property (*) and leaf reducibility yield a long x-sparse or complete blockade, or a better outcome. Fix $x \in (0, c^{10}]$ , and let $G$ be a $c^{10}$ -restricted $\overline{F}$ -free graph for which none 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}]$ .

Then for every $y \in [x, c^{3}]$ and every $y^{10 / 3}$ -restricted induced subgraph $F$ of $G$ with $∣ F ∣ \geq y^{10 (c_{4} + 2)} ∣ G ∣$ , there exists a $y^{11 / 3}$ -restricted induced subgraph of $F$ with at least $y^{c_{4} + 2} ∣ F ∣$ vertices.

Facts & Assumptions

Given: The data and failure hypotheses in the Statement, together with a parameter $y \in [x, c^{3}]$ and an induced subgraph $F$ of $G$ that is $y^{10 / 3}$ -restricted and satisfies $∣ F ∣ \geq y^{10 (c_{4} + 2)} ∣ G ∣$ .

[L1]

The previous lemma says that every $c y^{3}$ -restricted $\overline{F}$ -free graph satisfies one of five outcomes: a long $x$ -sparse or complete blockade, a $2 y^{4}$ -restricted induced subgraph, a clique or stable set, a complete or anticomplete blockade, or a pure blockade (Property (*) and leaf reducibility yield a long x-sparse or complete blockade, or a better outcome).

[L2]

If a set is $η$ -restricted, then it is also $η^{'}$ -restricted for every $η^{'} \geq η$ ( $c$ -sparse, $c$ -dense and $c$ -restricted vertex sets).

Proof

technique · apply the previous lemma to $F$ with parameter $y$ and show that every outcome except the deeper restricted-set outcome contradicts one of the assumed global failures

1.1

Because $y \leq c^{3}$ , one has $y^{10 / 3} = y^{3} y^{1 / 3} \leq c y^{3}$ . Thus [L2] upgrades the hypothesis that $F$ is $y^{10 / 3}$ -restricted to the statement that $F$ is $c y^{3}$ -restricted.

givenL2algebra

2.1

Apply [L1] to the graph $F$ with the original parameter $x$ and the current parameter $y$ . One of the five outcomes of [L1] holds for $F$ .

step 1.1L1

3.1

Suppose the first outcome of [L1] holds for $F$ : there is an $x$ -sparse or complete blockade in $F$ of length at least $y^{- 1}$ and width at least $y^{c_{4} + 2} ∣ F ∣$ . Since $y^{- 1} \in [c^{- 1}, x^{- 1}] \subseteq [c^{- 1}, x^{- 2}]$ and $y^{c_{4} + 2} ∣ F ∣ \geq y^{11 (c_{4} + 2)} ∣ G ∣ \geq y^{29 c_{4}} ∣ G ∣,$ this produces the forbidden global outcome 4.

step 2.1algebra

3.2

Suppose the second outcome of [L1] holds for $F$ . Because $2 y^{4} \leq y^{11 / 3}$ for $0 < y < 1$ , the resulting induced subgraph is already the desired $y^{11 / 3}$ -restricted induced subgraph of size at least $y^{c_{4} + 2} ∣ F ∣$ .

step 2.1algebra

3.3

Suppose the third outcome of [L1] holds for $F$ . Then $(x^{10} ∣ F ∣)^{c_{1}} \geq (x^{10} \cdot y^{10 (c_{4} + 2)} ∣ G ∣)^{c_{1}} \geq (x^{10 c_{4} + 30} ∣ G ∣)^{c_{1}} \geq (x^{30 c_{4}} ∣ G ∣)^{c_{1}},$ because $y \geq x$ and $c_{4} \geq 4$ . This contradicts the failure of global outcome 2.

step 2.1algebra

3.4

Suppose the fourth outcome of [L1] holds for $F$ : there is a complete or anticomplete $(k, ∣ F ∣ / k^{c_{2} + 7 / c_{3}})$ -blockade with $k \geq y^{- c_{3}}$ . If $k \geq 2$ , then $\frac{∣ F ∣}{k^{c_{2} + 7 / c_{3}}} \geq \frac{y^{10 (c_{4} + 2)} ∣ G ∣}{k^{c_{2} + 7 / c_{3}}} \geq \frac{∣ G ∣}{k^{c_{2} + 7 / c_{3} + 10 (c_{4} + 2) / c_{3}}} \geq \frac{∣ G ∣}{k^{c_{2} + 27 c_{4} / c_{3}}},$ so global outcome 3 holds, a contradiction. If instead $1 < k < 2$ , then the blockade has at least two blocks, and $\frac{∣ F ∣}{k^{c_{2} + 7 / c_{3}}} \geq \frac{∣ F ∣}{2^{c_{2} + 7 / c_{3}}} \geq \frac{∣ G ∣}{2^{c_{2} + 7 / c_{3} + 10 (c_{4} + 2) / c_{3}}} \geq \frac{∣ G ∣}{2^{c_{2} + 27 c_{4} / c_{3}}},$ because $∣ F ∣ \geq y^{10 (c_{4} + 2)} ∣ G ∣$ , the inequality $y^{- c_{3}} \leq k < 2$ implies $y^{10 (c_{4} + 2)} \geq 2^{- 10 (c_{4} + 2) / c_{3}}$ , and $7 + 10 (c_{4} + 2) \leq 27 c_{4}$ for $c_{4} \geq 4$ . Thus $G$ has a complete or anticomplete $(2, ∣ G ∣ / 2^{c_{2} + 27 c_{4} / c_{3}})$ -blockade, again contradicting the failure of global outcome 3.

step 2.1algebra

3.5

Suppose the fifth outcome of [L1] holds for $F$ : there is a pure $(ℓ, ∣ F ∣ / ℓ^{9})$ -blockade with $ℓ \in [y^{- 1}, x^{- 2}]$ . Then $\frac{∣ F ∣}{ℓ^{9}} \geq \frac{y^{10 (c_{4} + 2)} ∣ G ∣}{ℓ^{9}} \geq \frac{∣ G ∣}{ℓ^{29 c_{4}}},$ because $ℓ \geq y^{- 1}$ . This again gives the forbidden global outcome 4.

step 2.1algebra

4.1

The first, third, fourth, and fifth cases are impossible under the standing global failure hypotheses. Therefore the second case, recorded in step 3.2, must hold, which is exactly the desired conclusion.

step 3.1step 3.2step 3.3step 3.4step 3.5∎

Depends on

Used by

Constant-scale restricted property (*) yields a restricted subgraph, a polynomial clique or stable set, or two blockade alternatives 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, Claim 4.3.1 (standard reference, not scraped)