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.

A large cy-restricted subgraph in the three-outcome theorem forces a smaller-scale restricted subgraph

Statement

Let $F$ be a generalized nice, leaf-reducible, wonderful finite family. Assume constants $c \in (0, \frac{1}{2})$ , $c_{1}, c_{2} > 0$ , and $c_{3} \geq c_{4} \geq 4$ satisfy the conclusion of cy-restricted generalized niceness yields three outcomes for $F$ . Let $x \in (0, c^{2})$ , and let $G$ be an $\overline{F}$ -free graph such that:

$G$ has no clique and no stable set of size at least $(x^{c_{1} + 3 c_{3}} ∣ G ∣)^{c_{2}};$
for every integer $k \geq 2$ , $G$ has no complete or anticomplete $(k, ∣ G ∣ / k^{c_{1} + 3 c_{3}})$ -blockade.

Then 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.

Facts & Assumptions

Given: The family $F$ , the constants $c, c_{1}, c_{2}, c_{3}, c_{4}$ , the parameter $x$ , the $\overline{F}$ -free graph $G$ , the two global failure hypotheses, a parameter $y$ with $c y \in [x, c^{2}]$ , and a $c y$ -restricted induced subgraph $F$ with $∣ F ∣ \geq (c y)^{4 c_{3} / c_{4}} ∣ G ∣$ .

[L1]

The three-outcome theorem applies to every $c y$ -restricted $\overline{F}$ -free graph with the displayed constants (cy-restricted generalized niceness yields three outcomes).

[L2]

Every induced subgraph of an $\overline{F}$ -free graph is again $\overline{F}$ -free ( $H$ -free and $F$ -free graphs under the induced-subgraph convention).

Proof

technique · apply the three-outcome theorem to $F$ and rule out its first two outcomes by the assumed global failures in $G$

1.1

Because $c y \in [x, c^{2}]$ and $c < 1$ , we have $y \geq x$ and $y \leq c$ . Also $c y \geq y^{2}$ because $y \leq c$ . Therefore $∣ F ∣ \geq (c y)^{4 c_{3} / c_{4}} ∣ G ∣ \geq y^{8 c_{3} / c_{4}} ∣ G ∣$ .

givenalgebra

2.1

Since $F$ is an induced subgraph of the $\overline{F}$ -free graph $G$ , [L2] implies that $F$ is also $\overline{F}$ -free. Apply [L1] to $F$ . If it gives a clique or stable set in $F$ of size at least $(y^{c_{1}} ∣ F ∣)^{c_{2}}$ , then by step 1.1 one has $(y^{c_{1}} ∣ F ∣)^{c_{2}} \geq (y^{c_{1} + 8 c_{3} / c_{4}} ∣ G ∣)^{c_{2}} \geq (x^{c_{1} + 3 c_{3}} ∣ G ∣)^{c_{2}}$ , because $8 c_{3} / c_{4} \leq 2 c_{3} \leq 3 c_{3}$ and $y \geq x$ . This contradicts global hypothesis 1.

L1L2step 1.1givenalgebra

2.2

If [L1] gives a complete or anticomplete $(k, ∣ F ∣ / k^{c_{3}})$ -blockade in $F$ with $k \geq y^{- 1}$ , then $k \geq 2$ . Using step 1.1 and $k \geq y^{- 1}$ , one has $∣ F ∣ / k^{c_{3}} \geq y^{8 c_{3} / c_{4}} ∣ G ∣ / k^{c_{3}} \geq ∣ G ∣ / k^{c_{3} + 8 c_{3} / c_{4}} \geq ∣ G ∣ / k^{c_{1} + 3 c_{3}}$ , since $c_{3} + 8 c_{3} / c_{4} \leq c_{1} + 3 c_{3}$ . This contradicts global hypothesis 2.

L1step 1.1givenalgebra

3.1

Therefore only the third outcome of [L1] can occur. So $F$ has a $y^{c_{4}}$ -restricted induced subgraph $S$ with $∣ S ∣ \geq y^{c_{3}} ∣ F ∣$ . Because $c y \geq y^{2}$ , one has $y^{c_{4}} = (y^{2})^{c_{4} / 2} \leq (c y)^{c_{4} / 2}$ , so $S$ is also $(c y)^{c_{4} / 2}$ -restricted. Since $c y \leq y$ , we also have $y^{c_{3}} \geq (c y)^{c_{3}}$ , hence $∣ S ∣ \geq y^{c_{3}} ∣ F ∣ \geq (c y)^{c_{3}} ∣ F ∣$ . This is exactly the claimed smaller-scale restricted induced subgraph.

step 2.1step 2.2L1algebra

4.1

The claimed induced subgraph exists.

step 3.1∎

Depends on

Used by

Dependency tree · two levels

7 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, Claim 3.3.1 (standard reference, not scraped)