TheoremStatement: Literature-sourcedProof: 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 graph with bounded A-degree has a large comb or a small B-side

Statement

Let $G$ be a finite graph with a bipartition $(A, B)$ such that every vertex of $B$ has a neighbour in $A$ . Let $Γ, Δ > 0$ and let $d \in (0, 1)$ . Suppose every vertex of $A$ has at most $Δ$ neighbours in $B$ . 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)$ ;
$∣ B ∣ \leq \frac{3^{d + 1}}{3 / 2 - (3 / 2)^{d}} Γ^{d} Δ^{1 - d} .$

Facts & Assumptions

Given: A bipartite graph $(A, B)$ , parameters $Γ, Δ > 0$ and $d \in (0, 1)$ , every vertex of $B$ has a neighbour in $A$ , and every vertex of $A$ has at most $Δ$ neighbours in $B$ .

[L1]

Under the layer hypotheses of the previous lemma, either a $(t, Γ t^{- 1 / d})$ -comb already appears or the current layer $C$ has size at most $2^{d + 1} (2 / 3)^{s - s d - 1} Γ^{d} Δ^{1 - d}$ (A bipartite layer is small unless a large comb already appears).

[L2]

If $∣ r ∣ < 1$ , then $\sum_{n \geq 0} r^{n} = 1 / (1 - r)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

Proof

technique · direct

1.1givenchoose

Define pairwise disjoint sets $C_{1}, C_{2}, \dots$ inductively. Set $D_{1} : = B$ , and after defining $C_{1}, \dots, C_{s - 1}$ let $D_{s} : = B ∖ (C_{1} \cup \dots \cup C_{s - 1})$ . Choose distinct vertices $a_{1}, \dots, a_{k} \in A$ with $k$ maximal such that for each $i$ there are at least $(2 / 3)^{s} Δ$ vertices of $D_{s}$ adjacent to $a_{i}$ and to none of $a_{1}, \dots, a_{i - 1}$ . Let $C_{s}$ be the set of vertices of $D_{s}$ adjacent to one of $a_{1}, \dots, a_{k}$ . By maximality of $k$ , every vertex of $A$ has at most $(2 / 3)^{s} Δ$ neighbours in $D_{s} ∖ C_{s}$ . Inducting on $s$ shows that every vertex of $A$ has at most $(2 / 3)^{s - 1} Δ$ neighbours in $D_{s}$ .

2.1step 1.1givenalgebra

Every vertex of $B$ belongs to some layer $C_{s}$ . Indeed, if some $b \in B$ survived in every $D_{s}$ , choose a neighbour $a \in A$ of $b$ . Then $a$ has at least one neighbour in each $D_{s}$ , contradicting step 1.1 for all large $s$ because $(2 / 3)^{s - 1} Δ < 1$ eventually. Thus $B = C_{1} ⊔ C_{2} ⊔ \dots$ .

2.2step 1.1L1cases

Fix $s \geq 1$ . The data $D_{s}$ and the chosen vertices $a_{1}, \dots, a_{k}$ satisfy the hypotheses of [L1]. Therefore either [L1] already yields a $(t, Γ t^{- 1 / d})$ -comb in $(A, B)$ , or $∣ C_{s} ∣ \leq 2^{d + 1} (2 / 3)^{s - s d - 1} Γ^{d} Δ^{1 - d}$ . So if the first alternative never occurs, the displayed bound holds for every $s$ .

3.1step 2.1step 2.2L2algebra

Put $q : = (2 / 3)^{1 - d}$ . Since $d \in (0, 1)$ , we have $0 < q < 1$ , and $(2 / 3)^{s - s d - 1} = (3 / 2)^{d} q^{s - 1}$ . Hence [L2] gives $\sum_{s \geq 1} (2 / 3)^{s - s d - 1} = (3 / 2)^{d} \sum_{n \geq 0} q^{n} = (3 / 2)^{d} / (1 - (2 / 3)^{1 - d})$ . Using the disjoint union from step 2.1 and the layer bound from step 2.2, we obtain $∣ B ∣ = \sum_{s \geq 1} ∣ C_{s} ∣ \leq 2^{d + 1} Γ^{d} Δ^{1 - d} \sum_{s \geq 1} (2 / 3)^{s - s d - 1} = \frac{2^{d + 1} (3 / 2)^{d}}{1 - (2 / 3)^{1 - d}} Γ^{d} Δ^{1 - d} = \frac{3^{d + 1}}{3 / 2 - (3 / 2)^{d}} Γ^{d} Δ^{1 - d}$ .

4.1step 2.2step 3.1cases-exhaustive∎

Therefore either the comb alternative occurs at some stage, or the displayed bound on $∣ B ∣$ holds. This is exactly the Statement.

Depends on

Used by

Dependency tree · two levels

16 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, Theorem 2.1 (standard reference, not scraped)