ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-26

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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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, The Erdős-Hajnal Conjecture: A Survey, sec. 2 (standard reference, not scraped)

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