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.

✓ 4 results · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Classical and Log-Log Erdős–Hajnal Bounds — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-09-26 (gpt-6-sol)Open item page →

For large $n$ , the Fox–Sudakov choice of $x$ leaves a dense-or-sparse set of order at least $\sqrt{n}$

Example

Fix a nonempty finite graph $H$ , let $C_{H} > 0$ be the constant from Fox sudakov quantitative induced density bound, and let $G$ be an $H$ -free graph on $n$ vertices. Write $L : = \log_{2} n$ , assume $L > 2 C_{H}$ , and choose $x : = 2^{- \sqrt{L / (2 C_{H})}}$ .

Facts & Assumptions

Given: The data in the Example, in particular $L > 2 C_{H}$ .

[L1]

For nonempty $H$ and $G$ and $0 < x < 1 / 2$ , the proved quantitative-density corollary gives every $H$ -free $n$ -vertex graph a nonempty set $S$ of order at least $2^{- C_{H} (\log_{2} (1 / x))^{2}} n$ such that $G [S]$ or its complement has at most $x (\binom{∣ S ∣}{2})$ edges (Fox sudakov quantitative induced density bound). The hypothesis $L > 2 C_{H} > 0$ ensures $n > 1$ , so $G$ is nonempty.

Verification

technique · direct

1.1givenalgebra

For the chosen $x$ , one has $\log_{2} (1 / x) = \sqrt{L / (2 C_{H})} > 1$ , so $0 < x < 1 / 2$ .

2.1step 1.1L1algebra

Therefore $2^{- C_{H} (\log_{2} (1 / x))^{2}} n = 2^{- C_{H} \cdot L / (2 C_{H})} n = 2^{- L / 2} n = \sqrt{n}$ .

3.1step 2.1L1∎

So the proved quantitative-density corollary guarantees a dense-or-sparse set of order at least $\sqrt{n}$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-09-26 (gpt-6-sol)Open item page →

For large $n$ , the log-log choice of $x$ still leaves a dense-or-sparse set of order at least $\sqrt{n}$

Example

Fix a nonempty finite graph $H$ , let $C_{H} > 0$ be the constant from Loglog quantitative induced density bound, and let $G$ be an $H$ -free graph on $n \geq 3$ vertices. Write $L : = \log_{2} n$ , and set $β : = 1 / (4 \sqrt{C_{H}})$ and $x : = 2^{- β \sqrt{L \log_{2} L}}$ .

Facts & Assumptions

Given: The data in the Example.

[L1]

For nonempty $H, G$ and $0 < x < 1 / 2$ , the proved quantitative induced-density theorem gives every $H$ -free $n$ -vertex graph a nonempty set $S$ of order at least $2^{- C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x)} n$ whose induced graph or complement has at most $x (\binom{∣ S ∣}{2})$ edges (Loglog quantitative induced density bound).

Verification

technique · direct

1.1givenalgebra

For the chosen $x$ , one has $\log_{2} (1 / x) = β \sqrt{L \log_{2} L}$ .

2.1step 1.1algebra

For all sufficiently large $L$ , the inequality $β \sqrt{L \log_{2} L} \geq \sqrt{L} > 1$ holds. Hence $0 < x < 1 / 2$ and $\log_{2} \log_{2} (1 / x) \geq \frac{1}{2} \log_{2} L$ .

3.1step 2.1L1algebra

Hence, for all sufficiently large $n$ , $C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x) \leq 2 C_{H} β^{2} L = L / 8$ , and therefore $2^{- C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x)} n \geq 2^{- L / 8} n = 2^{7 L / 8} \geq \sqrt{n}$ .

4.1step 3.1L1∎

So for all sufficiently large $n$ , this choice of $x$ still leaves a dense-or-sparse set of order at least $\sqrt{n}$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

A lower bound of size $2^{c \sqrt{\log_{2} n}}$ is still subpolynomial in $n$

Example

Fix $c, ε > 0$ . Then the function $2^{c \sqrt{\log_{2} n}}$ grows more slowly than $n^{ε}$ .

Facts & Assumptions

Given: Positive reals $c$ and $ε$ .

[L1]

For $n > 1$ , $\log_{2} n$ is defined (The logarithm to a positive base other than one).

Verification

technique · direct

1.1L1algebra

Write $n = 2^{L}$ with $L : = \log_{2} n$ . Then $2^{c \sqrt{L}} / n^{ε} = 2^{c \sqrt{L} - ε L}$ .

2.1step 1.1algebra

If $L \geq (2 c / ε)^{2}$ , then $c \sqrt{L} \leq (ε / 2) L$ , so $c \sqrt{L} - ε L \leq - (ε / 2) L$ . Hence for all sufficiently large $n$ , $2^{c \sqrt{\log_{2} n}} / n^{ε} \leq 2^{- (ε / 2) \log_{2} n} = 1 / n^{ε / 2}$ , which tends to $0$ .

3.1step 2.1∎

Therefore $2^{c \sqrt{\log_{2} n}} = o (n^{ε})$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-26Open item page →

A lower bound of size $2^{c \sqrt{\log_{2} n \log_{2} \log_{2} n}}$ is still subpolynomial in $n$

Example

Fix $c, ε > 0$ . Then the function $2^{c \sqrt{\log_{2} n \log_{2} \log_{2} n}}$ still grows more slowly than $n^{ε}$ .

Facts & Assumptions

Given: Positive reals $c$ and $ε$ .

[L1]

For $n > 2$ , both $\log_{2} n$ and $\log_{2} \log_{2} n$ are defined (The logarithm to a positive base other than one).

Verification

technique · direct

1.1L1algebra

Write $n = 2^{L}$ with $L : = \log_{2} n$ . Then $2^{c \sqrt{L \log_{2} L}} / n^{ε} = 2^{c \sqrt{L \log_{2} L} - ε L}$ .

2.1step 1.1algebra

For $L \geq 16$ , one has $\log_{2} L \leq \sqrt{L}$ , so $\sqrt{L \log_{2} L} \leq L^{3 / 4}$ . If moreover $L \geq (2 c / ε)^{4}$ , then $c L^{3 / 4} \leq (ε / 2) L$ , and therefore $c \sqrt{L \log_{2} L} - ε L \leq - (ε / 2) L$ . Hence for all sufficiently large $n$ , $2^{c \sqrt{\log_{2} n \log_{2} \log_{2} n}} / n^{ε} \leq 1 / n^{ε / 2}$ , which tends to $0$ .

3.1step 2.1∎

Therefore $2^{c \sqrt{\log_{2} n \log_{2} \log_{2} n}} = o (n^{ε})$ .

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

The $P_{3}$ -free case is much stronger than the general lower bounds

Example

For $P_{3}$ -free graphs the general lower bounds of this page are far from sharp.

Facts & Assumptions

Given: A nonnull finite $P_{3}$ -free graph $G$ with $n : = ∣ V (G) ∣$ .

[L1]

Every $P_{3}$ -free graph satisfies $hom (G) \geq \sqrt{n}$ (Every $P_{3}$ -free graph $G$ satisfies $hom (G) \geq \sqrt{∣ V (G) ∣}$ ).

[L2]

For $n > 1$ , $\log_{2} n$ is defined (The logarithm to a positive base other than one).

Verification

technique · direct

1.1L1L2algebra

By [L1], the $P_{3}$ -free class admits the lower bound $hom (G) \geq \sqrt{n} = 2^{(\log_{2} n) / 2}$ .

2.1step 1.1algebra

The exponent $(\log_{2} n) / 2$ grows faster than every constant multiple of $\sqrt{\log_{2} n}$ , because if $L : = \log_{2} n$ and $L \geq 4 a^{2}$ , then $L / 2 \geq a \sqrt{L}$ . Hence for all sufficiently large $n$ , $2^{(\log_{2} n) / 2} \geq 2^{a \sqrt{\log_{2} n}}$ for every fixed $a > 0$ .

2.2step 1.1algebra

The same exponent $(\log_{2} n) / 2$ also grows faster than every constant multiple of $\sqrt{\log_{2} n \log_{2} \log_{2} n}$ , because for $L \geq 16$ one has $\log_{2} L \leq \sqrt{L}$ , so $\sqrt{L \log_{2} L} \leq L^{3 / 4}$ and then $L / 2 \geq b L^{3 / 4}$ for all sufficiently large $L$ . Thus for every fixed $b > 0$ and all sufficiently large $n$ , $2^{(\log_{2} n) / 2} \geq 2^{b \sqrt{\log_{2} n \log_{2} \log_{2} n}}$ .

3.1step 2.1step 2.2∎

So the square-root homogeneous-set bound for $P_{3}$ -free graphs is much stronger than either general scale on this page.

Classical and Log-Log Erdős–Hajnal Bounds — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

For large nn, the Fox–Sudakov choice of xx leaves a dense-or-sparse set of order at least nn​

Example

Facts & Assumptions

Verification

For large nn, the log-log choice of xx still leaves a dense-or-sparse set of order at least nn​

Example

Facts & Assumptions

Verification

A lower bound of size 2clog⁡2n2clog2​n​ is still subpolynomial in nn

Example

Facts & Assumptions

Verification

A lower bound of size 2clog⁡2n log⁡2log⁡2n2clog2​nlog2​log2​n​ is still subpolynomial in nn

Example

Facts & Assumptions

Verification

The P3P3​-free case is much stronger than the general lower bounds

Example

Facts & Assumptions

Verification

Sources

For large $n$ , the Fox–Sudakov choice of $x$ leaves a dense-or-sparse set of order at least $\sqrt{n}$

For large $n$ , the log-log choice of $x$ still leaves a dense-or-sparse set of order at least $\sqrt{n}$

A lower bound of size $2^{c \sqrt{\log_{2} n}}$ is still subpolynomial in $n$

A lower bound of size $2^{c \sqrt{\log_{2} n \log_{2} \log_{2} n}}$ is still subpolynomial in $n$

The $P_{3}$ -free case is much stronger than the general lower bounds