TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

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.

Large sparse-pair hypotheses yield an $x$ -sparse or complete blockade

Statement

Let $x \in (0, \frac{1}{2})$ , let $a > 1$ , $b > 0$ , and let $c : = 2^{- 4 b}$ . Let $y \in (0, c]$ . Suppose that $G$ is a graph with $∣ G ∣ \geq y^{- (a + 2)}$ such that for every induced subgraph $F$ of $G$ with $∣ F ∣ \geq c ∣ G ∣$ , there are disjoint sets $X, Y \subseteq V (F)$ satisfying

$∣ X ∣ \geq y^{a} ∣ F ∣, ∣ Y ∣ \geq (1 - b y) ∣ F ∣,$

and such that $Y$ is $x$ -sparse or complete to $X$ .

Then $G$ contains an $x$ -sparse or complete $(⌈ y^{- 1} ⌉, y^{a + 2} ∣ G ∣)$ -blockade.

Facts & Assumptions

Given: The hypotheses of the statement.

Proof

technique · direct

1.1

Let $n$ be maximal such that $G$ has a blockade $(B_{1}, \dots, B_{n})$ with $∣ B_{i} ∣ \geq y^{a + 2} ∣ G ∣$ for all $i$ , with $∣ B_{n} ∣ \geq (1 - b y)^{n} ∣ G ∣$ , and such that for every $i \in [n]$ , either every later block is $x$ -sparse to $B_{i}$ or every later block is complete to $B_{i}$ . This is possible because $n = 1$ and $B_{1} = V (G)$ already satisfy the conditions.

givenchoose

2.1

Suppose that $n < 2 y^{- 1}$ . Since $y \leq c = 2^{- 4 b}$ , one has $b y \leq b 2^{- 4 b} < 1 / 2$ . For $t \in [0, 1 / 2]$ the elementary inequality $1 - t \geq 2^{- 2 t}$ holds, so with $t = b y$ we get $(1 - b y)^{2 y^{- 1}} \geq (2^{- 2 b y})^{2 y^{- 1}} = 2^{- 4 b} = c$ . Therefore $∣ B_{n} ∣ \geq (1 - b y)^{n} ∣ G ∣ \geq c ∣ G ∣$ . Applying the hypothesis to the induced subgraph $G [B_{n}]$ , choose disjoint $X, Y \subseteq B_{n}$ with $∣ X ∣ \geq y^{a} ∣ B_{n} ∣ \geq y^{a + 2} ∣ G ∣$ and $∣ Y ∣ \geq (1 - b y) ∣ B_{n} ∣ \geq (1 - b y)^{n + 1} ∣ G ∣$ , and with $Y$ $x$ -sparse or complete to $X$ . Because $X \cup Y \subseteq B_{n}$ , the relation of every earlier block $B_{i}$ to $B_{n}$ restricts to the same relation to both $X$ and $Y$ . Hence $(B_{1}, \dots, B_{n - 1}, X, Y)$ is a larger blockade of the same type, contradicting the maximality of $n$ . So $n \geq 2 y^{- 1}$ .

step 1.1assume-contragivenalgebradischarge-contradiction

3.1

Let $Q$ be the set of indices $i$ such that every later block is $x$ -sparse to $B_{i}$ , and let $R$ be the set of indices $i$ such that every later block is complete to $B_{i}$ . By construction every index lies in $Q \cup R$ , so one of $Q$ or $R$ has cardinality at least $n / 2 \geq y^{- 1}$ .

step 1.1step 2.1algebra

4.1

Since one of $∣ Q ∣, ∣ R ∣$ is an integer at least $y^{- 1}$ , step 3.1 makes that cardinality at least $⌈ y^{- 1} ⌉$ . [step 3.1, given] If it is $∣ Q ∣$ , choose $⌈ y^{- 1} ⌉$ indices from $Q$ in their inherited order; the corresponding blocks form an $x$ -sparse blockade. If it is $∣ R ∣$ , the same choice from $R$ gives a complete blockade. Every selected block has size at least $y^{a + 2} ∣ G ∣$ by step 1.1. Thus one of the two required blockades exists.

step 1.1step 3.1givenchoose

5.1

Therefore $G$ contains an $x$ -sparse or complete $(⌈ y^{- 1} ⌉, y^{a + 2} ∣ G ∣)$ -blockade.

step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

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, Lemma 2.8 (standard reference, not scraped)

Large sparse-pair hypotheses yield an xx-sparse or complete blockade