Alphabeta Math
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.

Erdős–Stone–Simonovits: ex(n,H)=(11/(χ(H)1)+o(1))(n2) for every graph with an edge

Statement

Let H be a finite graph with at least one edge and put r=χ(H)2. Then

ex(n,H)=(11r1+o(1))(n2).

Equivalently,

limnex(n,H)(n2)=11χ(H)1.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

A proper k-vertex-colouring is a map c:Vk with c(u)c(v) for every edge {u,v}, its fibres are the colour classes, and χ(G)=min{kN:G is k-colourable} (Proper vertex colourings and chromatic number).

[F2]

For nN and r1, Turán's theorem gives ex(n,Kr+1)=e(Tn,r), and an n-vertex Kr+1-free graph attains equality exactly when it is isomorphic to Tn,r (Turán's theorem with equality: ex(n,Kr+1)=e(Tn,r), and Tn,r is the unique extremal graph).

[F3]

Every finite graph of chromatic number r embeds as an ordinary subgraph of Kr[s] for some s1 (Every finite graph H with χ(H)=r is an ordinary subgraph of Kr[s] for some s).

[F4]

For r2 and s1, π(Kr[s])=11/(r1) (Erdős–Stone for balanced blowups: π(Kr[s])=11/(r1) for r2).

Proof

technique · sandwich $H$ between a Turán graph and a balanced blowup
1.1

Every (r1)-partite graph is H-free, since every subgraph of it is (r1)-colourable while χ(H)=r. Therefore Tn,r1 gives lim infnex(n,H)/(n2)11/(r1).

givenF1F2
1.2

The embedding lemma gives an s1 with HKr[s]. Hence every H-free graph is Kr[s]-free, and balanced-blowup Erdős–Stone gives lim supnex(n,H)/(n2)11/(r1).

givenF3F4
2.1

The two bounds agree, proving the limit and the o(1) formulation. When r=2, the expression is 0 and the same proof uses Tn,1 for the lower bound and K2[s] for the upper bound, so the bipartite boundary is included.

step 1.1step 1.2givenF4

Depends on

Used by

Dependency tree · next 3 levels

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