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.

cy-restricted generalized niceness yields three outcomes

Statement

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

$G$ has a clique or stable set of size at least $(y^{c_{1}} ∣ G ∣)^{c_{2}};$
$G$ has a complete or anticomplete $(k, ∣ G ∣ / k^{c_{3}})$ -blockade with $k \geq y^{- 1}$ ; or
$G$ has a $y^{c_{4}}$ -restricted induced subgraph with at least $y^{c_{3}} ∣ G ∣$ vertices.

Facts & Assumptions

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

[L1]

The previous lemma provides constants $a_{1}, a_{2}, a_{5} > 0$ and $a_{3} \geq a_{4} \geq 4$ with the four reduction outcomes (Generalized niceness yields four reduction outcomes).

[L2]

The almost-pure-pair hypothesis yields a complete or anticomplete blockade (Large almost-pure pair hypotheses yield a complete or anticomplete blockade).

[L3]

If a graph is $λ$ -restricted on its full vertex set, then every induced subgraph on at least $c$ times as many vertices is $(λ / c)$ -restricted ( $c$ -sparse, $c$ -dense and $c$ -restricted vertex sets).

Proof

technique · either every large induced subgraph already has a large pure pair, or one large induced subgraph avoids that outcome and the previous four-outcome lemma applies there

1.1

Let $a_{1}, a_{2}, a_{5}, a_{3}, a_{4}$ be as in [L1], and set $c : = \min {2^{- 4 a_{5}}, (2 a_{5})^{- 1}, 1 / 4}$ , $c_{1} : = a_{1} + 1$ , $c_{2} : = a_{2}$ , $c_{3} : = a_{3} + 2$ , and $c_{4} : = a_{4}$ . Then $c \in (0, \frac{1}{2})$ and $c_{3} \geq c_{4} \geq 4$ .

L1choosealgebra

2.1

If $∣ G ∣ \leq y^{- c_{3}}$ , then any one-vertex induced subgraph of $G$ is $y^{c_{4}}$ -restricted and has size at least $y^{c_{3}} ∣ G ∣$ , so outcome 3 holds.

step 1.1givenalgebra

2.2

Suppose every induced subgraph $F$ of $G$ with $∣ F ∣ \geq c ∣ G ∣$ contains disjoint sets $X, Y \subseteq V (F)$ with $∣ X ∣ \geq y^{a_{3}} ∣ F ∣$ , $∣ Y ∣ \geq (1 - a_{5} y) ∣ F ∣$ , and $Y$ complete or anticomplete to $X$ . Since $y \leq c \leq (2 a_{5})^{- 1}$ and $c \leq 2^{- 4 a_{5}}$ , the hypotheses of [L2] are satisfied with $a = a_{3}$ and $b = a_{5}$ . Therefore [L2] yields a complete or anticomplete $(⌈ y^{- 1} ⌉, y^{a_{3} + 2} ∣ G ∣)$ -blockade in $G$ . Because $c_{3} = a_{3} + 2$ and $1 / ⌈ y^{- 1} ⌉ \leq y$ , each block has size at least $y^{c_{3}} ∣ G ∣ \geq ∣ G ∣ / ⌈ y^{- 1} ⌉^{c_{3}}$ . Hence outcome 2 holds after shrinking to exactly $⌈ y^{- 1} ⌉$ blocks if necessary.

step 1.1L2choosealgebra

2.3

We may therefore choose an induced subgraph $F$ of $G$ with $∣ F ∣ \geq c ∣ G ∣$ for which no such almost-pure pair exists. Because $G$ is $c y$ -restricted and $∣ F ∣ \geq c ∣ G ∣$ , [L3] implies that $F$ is $y$ -restricted. Apply [L1] to $F$ . Its fourth outcome is excluded by the choice of $F$ . If [L1] gives a clique or stable set of size at least $(y^{a_{1}} ∣ F ∣)^{a_{2}}$ , then $(y^{a_{1}} ∣ F ∣)^{a_{2}} \geq (y^{a_{1} + 1} ∣ G ∣)^{a_{2}} = (y^{c_{1}} ∣ G ∣)^{c_{2}}$ , because $∣ F ∣ \geq c ∣ G ∣ \geq y ∣ G ∣$ . So outcome 1 holds. If [L1] gives a complete or anticomplete blockade $(k, ∣ F ∣ / k^{a_{3}})$ with $k \geq y^{- 1}$ , then $∣ F ∣ / k^{a_{3}} \geq c ∣ G ∣ / k^{a_{3}} \geq y^{2} ∣ G ∣ / k^{a_{3}} \geq ∣ G ∣ / k^{a_{3} + 2} = ∣ G ∣ / k^{c_{3}}$ , because $c \geq y \geq y^{2}$ and $y \geq 1 / k$ . So outcome 2 holds. Finally, if [L1] gives a $y^{a_{4}}$ -restricted induced subgraph of size at least $y^{a_{3}} ∣ F ∣$ , then $y^{a_{3}} ∣ F ∣ \geq y^{a_{3}} c ∣ G ∣ \geq y^{a_{3} + 2} ∣ G ∣ = y^{c_{3}} ∣ G ∣$ , because $c \geq y^{2}$ , and $a_{4} = c_{4}$ . So outcome 3 holds.

step 1.1L1L3givenalgebra

3.1

Steps 2.1, 2.2, and 2.3 cover all cases, so one of the three stated outcomes always holds.

step 2.1step 2.2step 2.3∎

Depends on

Used by

Dependency tree · two levels

17 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.2 (standard reference, not scraped)