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

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 generalized niceness yields an x-scale restricted subgraph, a polynomial clique or stable set, or a blockade

Statement

Let $F$ be a generalized nice, leaf-reducible, wonderful finite family. Then there exist constants $c \in (0, \frac{1}{2})$ , $a_{1} \geq 1$ , and $a_{2} > 0$ such that for every $x \in (0, c^{2})$ and every $c^{2}$ -restricted $\overline{F}$ -free graph $G$ , at least one of the following holds:

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

Facts & Assumptions

Given: A generalized nice, leaf-reducible, wonderful finite family $F$ , a parameter $x \in (0, c^{2})$ , and a $c^{2}$ -restricted $\overline{F}$ -free graph $G$ .

[L1]

The three-outcome theorem provides constants $c, c_{1}, c_{2} > 0$ and $c_{3} \geq c_{4} \geq 4$ (cy-restricted generalized niceness yields three outcomes).

[L2]

Under the failure of the global clique/stable-set and blockade outcomes, every sufficiently large $c y$ -restricted induced subgraph contains a smaller scale restricted induced subgraph (A large cy-restricted subgraph in the three-outcome theorem forces a smaller-scale restricted subgraph).

[L3]

The iterative restricted-sparsification lemma turns a constant-scale restricted starting point plus the smaller-scale hypothesis into an $x$ -restricted induced subgraph (Iterated restricted sparsification reaches the target scale).

[L4]

A $c^{2}$ -restricted graph is, in particular, a valid starting point for the iterative lemma with starting constant $c^{2}$ ( $c$ -sparse, $c$ -dense and $c$ -restricted vertex sets).

Proof

technique · if the clique/stable-set and blockade outcomes fail, use the helper claim to verify the second hypothesis of the iterative lemma

1.1

Let $c, c_{1}, c_{2}, c_{3}, c_{4}$ be the constants from [L1], and set $a_{1} : = c_{1} + 3 c_{3}$ , $a_{2} : = c_{2}$ , $b_{1} : = c_{4} / 2$ , $b_{2} : = 4 c_{3} / c_{4}$ , and $b_{3} : = c_{3}$ .

L1choose

2.1

Hypothesis 1 of [L3] is automatic with starting constant $c^{2}$ : the graph $G$ itself is $c^{2}$ -restricted by assumption, so it has a $c^{2}$ -restricted induced subgraph of size $∣ G ∣ = (c^{2})^{0} ∣ G ∣$ , and in particular of size at least $(c^{2})^{b_{2}} ∣ G ∣$ because $b_{2} > 0$ and $c^{2} < 1$ .

step 1.1givenL3L4algebra

2.2

Suppose outcomes 2 and 3 fail for the given graph $G$ . We will show that outcome 1 must then hold.

step 1.1assume-contra

3.1

Apply [L2] with the constants from step 1.1. It shows that for every $y$ with $c y \in [x, c^{2}]$ and every $c y$ -restricted induced subgraph $F$ of $G$ with $∣ F ∣ \geq (c y)^{4 c_{3} / c_{4}} ∣ G ∣$ , there is a $(c y)^{c_{4} / 2}$ -restricted induced subgraph of $F$ with at least $(c y)^{c_{3}} ∣ F ∣$ vertices. Writing $λ : = c y$ , this is exactly hypothesis 2 of [L3] for every $λ \in [x, c^{2}]$ , with the starting constant $c^{2}$ and the choices $b_{1} = c_{4} / 2$ , $b_{2} = 4 c_{3} / c_{4}$ , and $b_{3} = c_{3}$ from step 1.1.

step 1.1step 2.2L2L3

4.1

The inequality required by [L3] holds for these choices, because $b_{1} b_{2} = (c_{4} / 2) \cdot (4 c_{3} / c_{4}) = 2 c_{3} \geq c_{3} + 4 c_{3} / c_{4} = b_{3} + b_{2}$ , using $c_{4} \geq 4$ .

step 1.1step 3.1algebraL3

5.1

Therefore [L3] applies and yields an $x$ -restricted induced subgraph of $G$ with at least $x^{b_{1} b_{2}} ∣ G ∣ = x^{2 c_{3}} ∣ G ∣$ vertices. Since $a_{1} = c_{1} + 3 c_{3} \geq 2 c_{3}$ and $x \in (0, 1)$ , we have $x^{2 c_{3}} \geq x^{a_{1}}$ , so outcome 1 holds.

step 1.1step 2.1step 3.1step 4.1L3algebra

6.1

Outcome 1 follows whenever outcomes 2 and 3 fail. Hence at least one of the three stated outcomes holds for every admissible $G$ .

step 2.2step 5.1discharge-contradiction∎

Depends on

Used by

A numeric run of the Lemma 3.3 exponent choice Example

Dependency tree · two levels

12 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, Erdos-Hajnal beyond the five-vertex path, Lemma 3.3 (standard reference, not scraped)