CorollaryStatement: AI-adaptedProof: AI-generatedSession-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.

For every $λ > 0$ a bounded number of disjoint $ϵ$ -restricted sets covers all but $λ ∣ V (G) ∣$ vertices of an $H$ -free graph

Statement

Fix a graph $H$ , a real $ϵ \in (0, \frac{1}{2})$ , and $λ > 0$ . Then there is an integer $t = t (H, ϵ, λ)$ such that every nonempty $H$ -free finite simple graph $G$ contains pairwise disjoint $ϵ$ -restricted sets $X_{1}, \dots, X_{s}$ for some $s \leq t$ , whose union misses fewer than $λ ∣ V (G) ∣$ vertices.

Facts & Assumptions

Given: A graph $H$ , reals $ϵ \in (0, \frac{1}{2})$ and $λ > 0$ .

[L1]

Every induced subgraph of an $H$ -free graph is $H$ -free (Every class defined by forbidden induced subgraphs is hereditary, Every induced subgraph of an $F$ -free graph is $F$ -free, $H$ -free and $F$ -free graphs under the induced-subgraph convention).

[L2]

Rödl's theorem provides a constant $δ > 0$ such that every nonempty $H$ -free graph contains an $ϵ$ -restricted set of size at least $δ$ times its order (Rödl: for every $H$ and every $ϵ \in (0, \frac{1}{2})$ there is $δ > 0$ such that every nonempty $H$ -free graph has an $ϵ$ -restricted vertex set of size at least $δ ∣ V (G) ∣$ ).

[L3]

Sparsity is internal to induced subgraphs, so a set that is $ϵ$ -restricted in an induced subgraph is also $ϵ$ -restricted in the ambient graph (A set is $c$ -sparse exactly when the maximum degree of the graph it induces is at most $c$ times its size, $c$ -sparse, $c$ -dense and $c$ -restricted vertex sets).

Proof

technique · direct

1.1

Let $δ$ be the constant from [L2]. Choose $t$ minimal with $(1 - δ)^{t} < λ$ .

L2choose

1.2

Starting from $G$ , repeatedly apply [L2] to the induced subgraph on the current remainder while that remainder has at least $λ ∣ V (G) ∣$ vertices. By [L1] each remainder is still $H$ -free, so this produces pairwise disjoint $ϵ$ -restricted sets $X_{1}, X_{2}, \dots$ .

L1L2choose

2.1

After each extraction, at least a $δ$ fraction of the current remainder is removed. Hence after $k$ steps the remainder has size at most $(1 - δ)^{k} ∣ V (G) ∣$ . In particular, after $t$ steps it has size strictly below $λ ∣ V (G) ∣$ by the choice of $t$ .

step 1.1step 1.2algebra

3.1

The process therefore stops after some number $s \leq t$ of extractions, and [L3] makes every extracted set $ϵ$ -restricted in the original graph.

step 1.2step 2.1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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, proof sketch of Theorem 1.3 (standard reference, not scraped)

For every λ>0λ>0 a bounded number of disjoint ϵϵ-restricted sets covers all but λ∣V(G)∣λ∣V(G)∣ vertices of an HH-free graph