TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Every nonempty $n$ -vertex graph satisfies $hom (G) \geq \frac{1}{2} \log_{2} n$

Statement

Every nonempty finite graph $G$ of order $n$ satisfies $hom (G) \geq \frac{1}{2} \log_{2} n .$

Facts & Assumptions

Given: A nonempty finite graph $G$ with $n = ∣ V (G) ∣$ .

[L1]

For every graph $F$ , $hom (F) = \max {ω (F), α (F)}$ (Homogeneous vertex sets and the homogeneous number $hom (G) = \max {ω (G), α (G)}$ ).

[L2]

For positive natural numbers $s, t$ , every graph on at least $(\binom{s + t - 2}{s - 1})$ vertices has an $s$ -vertex clique or a $t$ -vertex stable set (Finite graph Ramsey theorem: $(\binom{s + t - 2}{s - 1}) \to (s, t)^{2}$ for all positive $s, t$ ).

[L3]

The number $(\binom{m}{r})$ counts the $r$ -element subsets of an $m$ -element set (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L4]

For $b > 0$ with $b \neq 1$ and $x > 0$ , $\log_{b} x : = \log x / \log b$ (The logarithm to a positive base other than one).

[L5]

$\log : (0, \infty) \to R$ is strictly increasing, $\log (x y) = \log x + \log y$ for $x, y > 0$ , and $\log 1 = 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

Proof

technique · direct

1.1

Put $k = ⌊ \frac{1}{2} \log_{2} n ⌋ + 1$ . Then $k$ is a positive integer, $k > \frac{1}{2} \log_{2} n$ , and $2 k - 2 \leq \log_{2} n$ .

givenalgebra

2.1

By [L5], $\log 2 > \log 1 = 0$ , so $2 k - 2 \leq \log_{2} n = \log n / \log 2$ gives $(2 k - 2) \log 2 \leq \log n$ . Applying $\log (x y) = \log x + \log y$ to the $2 k - 2$ factors of $2^{2 k - 2}$ gives $\log (2^{2 k - 2}) = (2 k - 2) \log 2 \leq \log n$ , and $\log$ is strictly increasing, so $2^{2 k - 2} \leq n$ .

step 1.1L4L5algebra

3.1

The $(k - 1)$ -subsets of a $(2 k - 2)$ -set form part of its power set, and binary membership choices give the power set $2^{2 k - 2}$ elements, so $(\binom{2 k - 2}{k - 1}) \leq 2^{2 k - 2} \leq n$ .

step 2.1L3algebra

4.1

Apply [L2] with $s = t = k$ : $G$ has a clique or stable set of order at least $k$ .

step 3.1L2

5.1

Therefore $hom (G) \geq k > \frac{1}{2} \log_{2} n$ by [L1], which proves the stated weak inequality; when $n = 1$ , this reads $1 \geq 0$ and the same argument has $k = 1$ .

step 1.1step 4.1L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 78 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

A. Chernikov, MATH 223M notes, sec. 3.1 (standard reference, not scraped)

Every nonempty nn-vertex graph satisfies hom⁡(G)≥12log⁡2nhom(G)≥21​log2​n