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

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 finite graph with an edge has a Turán density $π (H) = \lim_{n \to \infty} ex (n, H) / (\binom{n}{2})$

Statement

For every finite graph $H$ with at least one edge, the limit

$π (H) : = \lim_{n \to \infty} \frac{ex (n, H)}{(\binom{n}{2})}$

exists in $[0, 1]$ . It equals

$\inf_{n \geq 2} \frac{ex (n, H)}{(\binom{n}{2})} .$

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

For a finite graph $H$ with an edge and every $n \geq 3$ , the normalized extremal numbers satisfy $ex (n, H) / (\binom{n}{2}) \leq ex (n - 1, H) / (\binom{n - 1}{2})$ ( $ex (n, H) / (\binom{n}{2})$ is nonincreasing for $n \geq 2$ ).

[F2]

Every nonincreasing real sequence bounded below converges to the infimum of its range (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).

Proof

technique · apply bounded monotone convergence

1.1

The normalized extremal numbers are nonincreasing. They lie in $[0, 1]$ because an edge count is nonnegative and no simple $n$ -vertex graph has more than $(\binom{n}{2})$ edges.

givenF1

2.1

Bounded monotone convergence makes the sequence converge to its infimum. The bounds in step 1.1 place that value in $[0, 1]$ .

step 1.1givenF2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 results over 12 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

Yufei Zhao, Graph Theory and Additive Combinatorics (standard reference, not scraped)

Every finite graph with an edge has a Turán density π(H)=lim⁡n→∞ex⁡(n,H)/(n2)π(H)=limn→∞​ex(n,H)/(2n​)