Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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 bipartite graph with at least one edge has Turán density zero

Statement

If H is a finite bipartite graph with at least one edge, then

π(H)=0.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

The complete bipartite graph KA,B has exactly all edges joining a vertex of A to a vertex of B (Empty and complete graphs, complete bipartite graphs, and the convention that Pn and Cn have n vertices).

[F2]

For s,t≥1, the Kővári–Sós–Turán theorem gives ex⁡(N,Ks,t)=Os,t(N2−1/s) (Kővári–Sós–Turán: exact bipartite and ordinary-graph upper bounds for excluding Ks,t).

[F3]

For every finite graph H with an edge, the normalized extremal numbers converge to π(H), their infimum over n≥2 (Every finite graph with an edge has a Turán density π(H)=lim⁡n→∞ex⁡(n,H)/(n2)).

Proof

technique · embed the forbidden graph in a complete bipartite graph
1.1

Choose a bipartition of H and enlarge its two sides, including any isolated vertices, to positive sizes s,t such that H is an ordinary subgraph of Ks,t. Every H-free graph is then Ks,t-free.

givenF1
2.1

Hence 0≤ex⁡(n,H)≤ex⁡(n,Ks,t)=Os,t(n2−1/s). Dividing by (n2) makes the right side tend to 0. The existing limit π(H) is therefore 0.

step 1.1givenF2F3
3.1

The at-least-one-edge hypothesis ensures both bipartition sides can be chosen positive and is exactly the scope in which the extremal density was defined.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · two levels

12 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