TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26‡ rests on unproved material

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.

‡ Rests on 1 statement not proved in this library. Every dependency marked ‡ below is recorded with a citation but is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Every $H$ -free graph has a homogeneous set of size at least $2^{c \sqrt{\log_{2} n \log_{2} \log_{2} n}}$

Statement

Let $H$ be a finite graph. Then there exists a constant $c_{H} > 0$ such that every nonnull finite $H$ -free graph $G$ with $n : = ∣ V (G) ∣ \geq 2$ satisfies $hom (G) \geq 2^{c_{H} \sqrt{\log_{2} n \log_{2} \log_{2} n}} .$

Facts & Assumptions

Given: A finite graph $H$ , a nonnull finite $H$ -free graph $G$ , and $n : = ∣ V (G) ∣ \geq 2$ .

[L1]

The homogeneous number is $hom (G) = \max {ω (G), α (G)}$ (Homogeneous vertex sets and the homogeneous number $hom (G) = \max {ω (G), α (G)}$ ).

‡ [L2]

Bucić-Nguyen-Scott-Seymour quantitative density: there exists $C_{H} > 0$ such that for every real $x$ with $0 < x < 1 / 2$ there is $S \subseteq V (G)$ with $∣ S ∣ \geq 2^{- C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x)} n$ and one of $G [S]$ and $\overline{G} [S]$ has at most $x (\binom{∣ S ∣}{2})$ edges (Bucić–Nguyen–Scott–Seymour: a log-log quantitative density theorem ‡).

[L3]

If a nonempty vertex set $X$ satisfies $d_{G} (X, X) \leq c$ , then some $X^{'} \subseteq X$ has $∣ X^{'} ∣ \geq ∣ X ∣ / 2$ and is $4 c$ -sparse (A set of self-density at most $c$ has a subset of at least half its size that is $4 c$ -sparse).

[L4]

A nonempty set $X$ is $c$ -sparse exactly when every vertex of $G [X]$ has degree at most $c ∣ X ∣$ (A set is $c$ -sparse exactly when the maximum degree of the graph it induces is at most $c$ times its size).

[L5]

Every nonnull finite graph $F$ satisfies $χ (F) \leq Δ (F) + 1$ (The greedy colouring bound $χ (G) \leq Δ (G) + 1$ for every nonnull finite graph).

[L6]

Every finite graph $F$ satisfies $∣ V (F) ∣ \leq χ (F) α (F)$ (The bounds $ω (G) \leq χ (G)$ and $∣ V (G) ∣ \leq χ (G) α (G)$ ).

[L7]

A vertex set is a clique in $G$ if and only if it is a stable set in $\overline{G}$ (Complementation swaps cliques with stable sets, so $ω (\overline{G}) = α (G)$ ).

[L8]

For nonempty $X$ , the self-density is $d_{G} (X, X) = 2 ∣ E (G [X]) ∣ / ∣ X ∣^{2}$ (Edge counts and densities between nonempty vertex sets).

Proof

technique · direct

1.1

By [L2], choose a constant $C_{H} > 0$ . Because every nonnull graph has $hom (G) \geq 1$ , it is enough to prove the bound for all sufficiently large $n$ ; assume from now on that $n$ is large enough that $L : = \log_{2} n \geq 4$ . Set $β : = 1 / (4 \sqrt{C_{H}})$ and $x : = 2^{- β \sqrt{L \log_{2} L}}$ . Then $0 < x < 1 / 2$ .

L1‡ L2choose

2.1

For large enough $L$ , the inequality $β \sqrt{L \log_{2} L} \geq \sqrt{L}$ holds, so $\log_{2} \log_{2} (1 / x) = \log_{2} (β \sqrt{L \log_{2} L}) \geq \frac{1}{2} \log_{2} L$ . Therefore $C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x) \leq 2 C_{H} β^{2} L = L / 8$ . Using [L2], obtain $S \subseteq V (G)$ with $∣ S ∣ \geq 2^{- L / 8} n = 2^{7 L / 8} \geq \sqrt{n}$ , and one of $G [S]$ and $\overline{G} [S]$ has at most $x (\binom{∣ S ∣}{2})$ edges. For that chosen graph $F$ on vertex set $S$ , [L8] gives $d_{F} (S, S) \leq 2 x (\binom{∣ S ∣}{2}) / ∣ S ∣^{2} = x (∣ S ∣ - 1) / ∣ S ∣ \leq x$ .

step 1.1‡ L2L8algebra

3.1

If $F = G [S]$ , then [L3] gives $X \subseteq S$ with $∣ X ∣ \geq ∣ S ∣ / 2$ and $X$ $4 x$ -sparse in $G$ . By [L4], [L5], and [L6], $α (G [X]) \geq ∣ X ∣ / (4 x ∣ X ∣ + 1)$ .

step 2.1L3L4L5L6

3.2

If $F = \overline{G} [S]$ , then the same argument inside the complement produces a stable set of $\overline{G} [X]$ of size at least $∣ X ∣ / (4 x ∣ X ∣ + 1)$ for some $X \subseteq S$ with $∣ X ∣ \geq ∣ S ∣ / 2$ , and [L7] turns it into a clique of $G [X]$ .

step 2.1L3L4L5L6L7

4.1

Steps 3.1 and 3.2 show that $G$ has a homogeneous set $Y$ with $∣ Y ∣ \geq ∣ X ∣ / (4 x ∣ X ∣ + 1)$ for some $X \subseteq S$ satisfying $∣ X ∣ \geq ∣ S ∣ / 2 \geq \sqrt{n} / 2$ .

step 3.1step 3.2step 2.1L1

5.1

Because $x \sqrt{n} = 2^{L / 2 - β \sqrt{L \log_{2} L}}$ , choose a threshold $N_{H} \geq 2$ so that $x \sqrt{n} \geq 1$ whenever $n \geq N_{H}$ . For those $n$ , step 4.1 gives $4 x ∣ X ∣ \geq 2$ , hence $4 x ∣ X ∣ + 1 \leq 8 x ∣ X ∣$ , and therefore $∣ Y ∣ \geq 1 / (8 x) = 2^{β \sqrt{L \log_{2} L} - 3}$ .

step 4.1step 1.1choosealgebra

6.1

Set $c_{H} : = β / 2$ . For all sufficiently large $n$ , the inequality $β \sqrt{L \log_{2} L} - 3 \geq c_{H} \sqrt{L \log_{2} L}$ holds, so step 5.1 gives $∣ Y ∣ \geq 2^{c_{H} \sqrt{L \log_{2} L}}$ . Shrinking $c_{H}$ if necessary handles the finitely many smaller values of $n$ .

step 5.1choosealgebra

7.1

Hence every nonnull finite $H$ -free graph $G$ with $∣ V (G) ∣ = n \geq 2$ satisfies $hom (G) \geq 2^{c_{H} \sqrt{\log_{2} n \log_{2} \log_{2} n}}$ .

step 6.1L1∎

Depends on

Used by

Dependency tree · two levels

31 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

Matija Bucić, Tung Nguyen, Alex Scott, and Paul Seymour, Induced subgraph density. I. A loglog step towards Erdős-Hajnal, Theorem 1.3 (standard reference, not scraped)

Every HH-free graph has a homogeneous set of size at least 2clog⁡2n log⁡2log⁡2n2clog2​nlog2​log2​n​