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 -free graph partitions into boundedly many vertex sets of self-density at most or at least
Statement
Fix a graph and a real . Then there exists an integer such that every -free finite simple graph admits a partition
in which every part satisfies or .
Facts & Assumptions
Given: A graph and a real .
The edge-density form of Rödl's theorem supplies a constant such that every nonempty -free finite simple graph contains a set with and either or (The edge-density form of Rödl's theorem: every nonempty -free graph has a linearly large set of self-density at most or at least ).
Every induced subgraph of an -free graph is again -free (Every class defined by forbidden induced subgraphs is hereditary, Every induced subgraph of an -free graph is -free, -free and -free graphs under the induced-subgraph convention).
If then has the same adjacencies on every subset as does, so (Subgraphs, induced subgraphs and spanning subgraphs, Edge counts and densities between nonempty vertex sets).
For , the sequence tends to (For the sequence is null, and for the sequence diverges to ).
Proof
Let be the constant from [L1], set , and note that . Then every nonempty -free graph contains a set with and either or .
Since , [L3] applied to yields a natural number with .
Let be an -free finite simple graph. If , the empty partition works, so assume . Put . For each , if stop; otherwise the induced subgraph is -free by [L2], so step 1.1 and [F1] give a nonempty set with and either or . Define .
If the process stops at some stage because , then the nonempty extracted sets partition and each already has self-density at most or at least , hence in particular at most or at least .
Assume now that the process does not stop before stage . Then are pairwise disjoint nonempty sets, and an induction on using step 2.2 gives for every . Hence by step 2.1, while by step 2.2.
Put and for . Then partition . Writing , , and , step 3.2 gives .
If , then because the new ordered edges are those incident with at least one vertex of . Therefore .
If instead , then . Since and , one has , so .
In the situation of steps 3.2 and 4.1, step 5.1 or 5.2 handles , while each for already has self-density at most or at least . Therefore every part of the partition has self-density at most or at least .
Step 3.1 settles the case where the extraction stops early, and step 6.1 settles the case where it reaches stage . So works for every and .
Depends on
- The edge-density form of Rödl's theorem: every nonempty $H$-free graph has a linearly large set of self-density at most $\epsilon$ or at least $1-\epsilon$
- Every class defined by forbidden induced subgraphs is hereditary
- Every induced subgraph of an $\mathcal F$-free graph is $\mathcal F$-free
- $H$-free and $\mathcal F$-free graphs under the induced-subgraph convention
- Subgraphs, induced subgraphs and spanning subgraphs
- Edge counts and densities between nonempty vertex sets
- For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$
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
- M. Chudnovsky, A. Scott, P. Seymour, and S. Spirkl, Strengthening Rödl's theorem, Theorem 1.3 (standard reference, not scraped)