LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31

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 bipartite layer is small unless a large comb already appears

Statement

Let $G$ be a finite graph with a bipartition $(A, B)$ , let $Γ, Δ > 0$ , let $d \in (0, 1)$ , and let $s \geq 1$ be an integer. Suppose that $D \subseteq B$ and distinct vertices $a_{1}, \dots, a_{k} \in A$ satisfy:

every vertex of $A$ has at most $(2 / 3)^{s - 1} Δ$ neighbours in $D$ ; and
for each $i \in {1, \dots, k}$ , at least $(2 / 3)^{s} Δ$ vertices of $D$ are adjacent to $a_{i}$ and to none of $a_{1}, \dots, a_{i - 1}$ .

Let $C \subseteq D$ be the set of vertices adjacent to at least one of $a_{1}, \dots, a_{k}$ . Then at least one of the following holds:

for some integer $t \geq 1$ , there is a $(t, Γ t^{- 1 / d})$ -comb in $(A, B)$ whose teeth lie in ${a_{1}, \dots, a_{k}}$ and whose blocks lie in $C$ ;
$∣ C ∣ \leq 2^{d + 1} (2 / 3)^{s - s d - 1} Γ^{d} Δ^{1 - d} .$

Facts & Assumptions

Given: A bipartite graph $(A, B)$ , parameters $Γ, Δ > 0$ and $d \in (0, 1)$ , an integer $s \geq 1$ , a set $D \subseteq B$ , distinct vertices $a_{1}, \dots, a_{k} \in A$ , and the two hypotheses in the Statement.

[L1]

A $(t, w)$ -comb in $(A, B)$ consists of distinct teeth in $A$ and pairwise disjoint blocks in $B$ , each tooth complete to its own block and anticomplete to all other blocks (Combs in a graph).

Proof

technique · direct

1.1

For each $i$ , let $P_{i}$ be the set of vertices in $D$ adjacent to $a_{i}$ and to none of $a_{1}, \dots, a_{i - 1}$ . By the second hypothesis, $∣ P_{i} ∣ \geq (2 / 3)^{s} Δ$ , and the sets $P_{1}, \dots, P_{k}$ are pairwise disjoint. Let $Q_{i}$ be the set of vertices in $D ∖ P_{i}$ adjacent to $a_{i}$ . Since every vertex of $A$ has at most $(2 / 3)^{s - 1} Δ$ neighbours in $D$ , we have $∣ Q_{i} ∣ \leq (2 / 3)^{s - 1} Δ - (2 / 3)^{s} Δ = (2 / 3)^{s} Δ / 2$ .

givenalgebra

2.1

Declare the vertices $a_{k}, a_{k - 1}, \dots, a_{1}$ good backwards as follows: $a_{i}$ is good when at most $∣ P_{i} ∣ / 2$ vertices of $P_{i}$ are adjacent to a good vertex among $a_{i + 1}, \dots, a_{k}$ . Let $I$ be the set of good indices, and let $Q : = ⋃_{i \in I} Q_{i}$ . For every bad index $i \notin I$ , at least $∣ P_{i} ∣ / 2 \geq (2 / 3)^{s} Δ / 2$ vertices of $P_{i}$ lie in $Q$ . Since the $P_{i}$ are disjoint and each $Q_{i}$ has size at most $(2 / 3)^{s} Δ / 2$ , it follows that $(k - ∣ I ∣) (2 / 3)^{s} Δ / 2 \leq ∣ Q ∣ \leq ∣ I ∣ (2 / 3)^{s} Δ / 2$ , so $∣ I ∣ \geq k / 2$ .

step 1.1algebra

3.1

If $I \neq \emptyset$ , then for each $i \in I$ let $B_{i} : = P_{i} ∖ Q$ . We have $∣ B_{i} ∣ \geq ∣ P_{i} ∣ / 2 \geq (2 / 3)^{s} Δ / 2$ . If $i < j$ are both in $I$ , then $B_{i}$ is disjoint from $P_{j}$ and every vertex of $B_{i}$ avoids $Q_{j}$ , so no vertex of $B_{i}$ is adjacent to $a_{j}$ ; similarly no vertex of $B_{j}$ is adjacent to $a_{i}$ . Therefore $((a_{i}, B_{i}) : i \in I)$ is a $(∣ I ∣, (2 / 3)^{s} Δ / 2)$ -comb in $(A, B)$ by [L1].

step 1.1step 2.1L1construct

4.1

If $I \neq \emptyset$ and $(2 / 3)^{s} Δ / 2 \geq Γ ∣ I ∣^{- 1 / d}$ , then step 3.1 already gives the first alternative. Hence we may assume either $I = \emptyset$ or $(2 / 3)^{s} Δ / 2 < Γ ∣ I ∣^{- 1 / d}$ . In the second case, $∣ I ∣ < (2 Γ (3 / 2)^{s} / Δ)^{d}$ . When $I = \emptyset$ , step 2.1 gives $k = 0$ , so then $C = \emptyset$ . In either remaining case, $k \leq 2 (2 Γ (3 / 2)^{s} / Δ)^{d}$ .

step 3.1step 2.1algebracases

5.1

Since every $a_{i}$ has at most $(2 / 3)^{s - 1} Δ$ neighbours in $D$ , the set $C$ of all vertices of $D$ adjacent to one of the $a_{i}$ satisfies $∣ C ∣ \leq k (2 / 3)^{s - 1} Δ \leq 2 (2 Γ (3 / 2)^{s} / Δ)^{d} (2 / 3)^{s - 1} Δ = 2^{d + 1} (2 / 3)^{s - s d - 1} Γ^{d} Δ^{1 - d}$ . This is the second alternative.

step 4.1givenalgebra∎

Depends on

Combs in a graph

Used by

A bipartite graph with bounded A-degree has a large comb or a small B-side Theorem

Dependency tree · two levels

3 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

Maria Chudnovsky, Alex Scott, Paul Seymour, and Sophie Spirkl, Erdős-Hajnal for graphs with no 5-hole, proof of Theorem 2.1 (standard reference, not scraped)