TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Induced graph removal lemma for a fixed graph

Statement

For every finite graph $H$ and every $ϵ > 0$ there are $δ > 0$ and $n_{0}$ such that every graph $G$ of order $n \geq n_{0}$ satisfying ${ind}_{H} (G) < δ n^{∣ V (H) ∣}$ can be changed into an induced- $H$ -free graph by adding or deleting fewer than $ϵ n^{2}$ edges. Equivalently, every graph that is $ϵ$ -far from being induced- $H$ -free contains at least $δ n^{∣ V (H) ∣}$ labelled induced copies of $H$ .

Facts & Assumptions

Given: A fixed graph $H$ , $ϵ > 0$ , and a sufficiently large graph $G$ .

[L1]

For any prescribed minimum part count $k_{0}$ , every graph of order at least $k_{0}$ has an equitable partition into $k$ parts with $k_{0} \leq k \leq K$ , carrying nonempty representative subsets $W_{i} \subseteq V_{i}$ of size at least $δ n$ , such that every representative pair, including self-pairs, is very regular and all but at most $ϵ_{0} k^{2}$ ordered representative densities approximate their coarse densities (Strong regularity with linearly large representative subsets and no irregular representative pair).

[L2]

Regular pairs whose edge and nonedge densities stay away from the wrong extremes force a positive product-proportion of induced embeddings of $H$ (Induced counting lemma: regular edge and nonedge pairs force many induced copies).

[L3]

Edit distance counts added and deleted adjacencies, and $ϵ$ -far means that every graph in the target hereditary property is at distance at least $ϵ n^{2}$ (Graph edit distance and being $ϵ$ -far from an induced-hereditary property).

[L4]

The number ${ind}_{H} (G)$ counts labelled induced embeddings of $H$ in $G$ (The induced-embedding count ${ind}_{H} (G)$ ).

Proof

technique · contraposition

1.1

We prove the equivalent far-from-free formulation. Choose $0 < η ≪ ϵ$ , require $n_{0} \geq 8 / ϵ$ , and apply [L1] with minimum part count $k_{0} = ⌈ 8 / ϵ ⌉$ and with density-approximation error and regularity sequence small enough for [L2]. Write the resulting coarse parts as $V_{1}, \dots, V_{k}$ , so that $k \geq 8 / ϵ$ , and the representatives as $W_{1}, \dots, W_{k}$ .

contrapositive-reducegivenL1L2choose

2.1

Construct $G^{'}$ from $G$ as follows for every unordered coarse pair, allowing a pair with equal indices. If $d (W_{i}, W_{j}) < η$ , delete all corresponding edges; if $d (W_{i}, W_{j}) > 1 - η$ , add all corresponding nonedges; otherwise leave those adjacencies unchanged.

step 1.1choose

3.1

For every coarse pair whose representative and coarse densities differ by at most the approximation error, the number of edits is at most $(η + o (1)) ∣ V_{i} ∣ ∣ V_{j} ∣$ . Exceptional pairs have total count at most $o (k^{2})$ , and equitability controls their weight. The diagonal pairs are edited without any density control, but equitability bounds their total contribution by $\sum_{i} ∣ V_{i} ∣^{2} \leq n \max_{i} ∣ V_{i} ∣ \leq n (n / k + 1) = n^{2} / k + n$ , which the choices $k \geq 8 / ϵ$ and $n \geq n_{0} \geq 8 / ϵ$ of step 1.1 make at most $ϵ n^{2} / 4$ . The choices in step 1.1 therefore make $dist (G, G^{'}) < ϵ n^{2}$ .

step 1.1step 2.1L1L3algebra

4.1

Assume that $G$ is $ϵ$ -far from induced- $H$ -free. Then [L3] and step 3.1 imply that $G^{'}$ contains an induced copy of $H$ . For each pattern vertex $a$ , let $i (a)$ be the coarse part containing its image. Repetitions among the indices are allowed.

assume-hypstep 3.1L3choose

5.1

If $a b \in E (H)$ , the cleaning rule and the edge of this copy imply $d (W_{i (a)}, W_{i (b)}) \geq η$ . If $a b \notin E (H)$ , its nonedge implies $d (W_{i (a)}, W_{i (b)}) \leq 1 - η$ . Every such representative pair is regular, including when $i (a) = i (b)$ , by [L1].

step 2.1step 4.1L1

6.1

Apply [L2] to $W_{i (1)}, \dots, W_{i (h)}$ . Since every representative has size at least $ρ n$ for a constant $ρ > 0$ , the original graph $G$ contains at least $c \prod_{a = 1}^{h} ∣ W_{i (a)} ∣ \geq c ρ^{h} n^{h}$ induced embeddings of $H$ . Set $δ = c ρ^{h}$ .

step 5.1L2L4algebra

7.1

Thus every $ϵ$ -far graph has at least $δ n^{h}$ induced copies. This is the contrapositive, and hence proves both formulations in the Statement.

step 1.1step 6.1discharge-contrapositive∎

Depends on

Used by

Induced removal must permit adding edges as well as deleting them Counterexample

Dependency tree · next 3 levels

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

Y. Zhao, Graph Theory and Additive Combinatorics, Theorem 2.8.1 (standard reference, not scraped)
D. Conlon and J. Fox, Graph removal lemmas, Theorem 1.3 (standard reference, not scraped)