Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

Every H-free graph partitions into boundedly many vertex sets of self-density at most ϵ or at least 1ϵ

Statement

Fix a graph H and a real ϵ(0,12). Then there exists an integer B=B(H,ϵ) such that every H-free finite simple graph G admits a partition

V(G)=X1Xm,mB,

in which every part satisfies dG(Xi,Xi)ϵ or dG(Xi,Xi)1ϵ.

Facts & Assumptions

Given: A graph H and a real ϵ(0,12).

[L1]

The edge-density form of Rödl's theorem supplies a constant δ0>0 such that every nonempty H-free finite simple graph J contains a set XV(J) with Xδ0V(J) and either dJ(X,X)ϵ/2 or dJ(X,X)1ϵ/2 (The edge-density form of Rödl's theorem: every nonempty H-free graph has a linearly large set of self-density at most ϵ or at least 1ϵ).

[F1]

If WV(G) then G[W] has the same adjacencies on every subset XW as G does, so dG[W](X,X)=dG(X,X) (Subgraphs, induced subgraphs and spanning subgraphs, Edge counts and densities between nonempty vertex sets).

Proof

technique · direct
1.1

Let δ0>0 be the constant from [L1], set ρ:=min{δ0,12}, and note that 0<ρ12. Then every nonempty H-free graph J contains a set XV(J) with XρV(J) and either dJ(X,X)ϵ/2 or dJ(X,X)1ϵ/2.

L1algebrachoose
2.1

Since 0<1ρ<1, [L3] applied to r=1ρ yields a natural number t1 with (1ρ)t<ρϵ/16.

step 1.1L3choose
2.2

Let G be an H-free finite simple graph. If V(G)=, the empty partition works, so assume n:=V(G)>0. Put R0:=V(G). For each i=1,,t, if Ri1= stop; otherwise the induced subgraph G[Ri1] is H-free by [L2], so step 1.1 and [F1] give a nonempty set XiRi1 with XiρRi1 and either dG(Xi,Xi)ϵ/2 or dG(Xi,Xi)1ϵ/2. Define Ri:=Ri1Xi.

step 1.1L2F1choose
3.1

If the process stops at some stage it because Ri1=, then the nonempty extracted sets X1,,Xi1 partition V(G) and each already has self-density at most ϵ/2 or at least 1ϵ/2, hence in particular at most ϵ or at least 1ϵ.

step 2.2algebra
3.2

Assume now that the process does not stop before stage t. Then X1,,Xt are pairwise disjoint nonempty sets, and an induction on i using step 2.2 gives Ri(1ρ)Ri1 for every it. Hence Rt(1ρ)tn<(ρϵ/16)n by step 2.1, while X1ρn by step 2.2.

step 2.1step 2.2algebra
4.1

Put Y1:=X1Rt and Yi:=Xi for 2it. Then Y1,,Yt partition V(G). Writing x:=X1, r:=Rt, y:=Y1=x+r and α:=r/x, step 3.2 gives α<ϵ/16.

step 3.2algebra
5.1

If dG(X1,X1)ϵ/2, then eG(Y1,Y1)eG(X1,X1)+2ry because the new ordered edges are those incident with at least one vertex of Rt. Therefore dG(Y1,Y1)(ϵ/2)(x/y)2+2r/yϵ/2+2α<ϵ.

step 4.1algebra
5.2

If instead dG(X1,X1)1ϵ/2, then dG(Y1,Y1)dG(X1,X1)(x/y)2(1ϵ/2)/(1+α)2. Since α<ϵ/16 and ϵ<1/2, one has (1+α)2<(1+ϵ/16)21+ϵ/2, so dG(Y1,Y1)>(1ϵ/2)/(1+ϵ/2)>1ϵ.

step 4.1algebra
6.1

In the situation of steps 3.2 and 4.1, step 5.1 or 5.2 handles Y1, while each Yi=Xi for i2 already has self-density at most ϵ/2 or at least 1ϵ/2. Therefore every part of the partition has self-density at most ϵ or at least 1ϵ.

step 2.2step 4.1step 5.1step 5.2
7.1

Step 3.1 settles the case where the extraction stops early, and step 6.1 settles the case where it reaches stage t. So B:=t works for every H and ϵ.

step 2.1step 3.1step 6.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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