Adapted from jtraverso/graph-removal-lemma (Palomar-registered source).

Proofs of the statements in Challenge.lean

The theorems are proved in RemovalLib/GraphRemoval.lean (namespace GraphRemoval), on top of StabilityLib/ (the clique counting, clique removal and embedding lemmas of the registered entry PALOMAR-2026-10-16-000024, included unchanged). The counting lemma is the greedy embedding argument of StabilityLib/Embedding.lean, turned into a count of partial embeddings. The far form applies Mathlib's Szemerédi regularity lemma (szemeredi_regularity) and finds a copy of H in the reduced graph; its parts satisfy the hypotheses of the counting lemma. The removal lemma is its contrapositive.

theorem RemovalLemma.card_copies_ge {α : Type u_1} {β : Type u_2} [Fintype β] (L : SimpleGraph β) (G : SimpleGraph α) [DecidableRel G.Adj] (s : β → Finset α) {η d : ℝ} (hη : 0 < η) (hη₁ : η ≤ 1) (hd : 0 < d) (hd₁ : d ≤ 1) (hηd : 2 * ↑(Fintype.card β) * η ≤ d ^ Fintype.card β) (hsize : ∀ (x : β), 4 * ↑(Fintype.card β) ≤ d ^ Fintype.card β * ↑(s x).card) (hs : ∀ (x y : β), L.Adj x y → ∀ A ⊆ s x, ∀ B ⊆ s y, η * ↑(s x).card ≤ ↑A.card → η * ↑(s y).card ≤ ↑B.card → d ≤ ↑(G.edgeDensity A B)) : (d ^ Fintype.card β / 4) ^ Fintype.card β * ∏ x : β, ↑(s x).card ≤ ↑(Nat.card { f : β ↪ α // (∀ (x : β), f x ∈ s x) ∧ ∀ (x y : β), L.Adj x y → G.Adj (f x) (f y) })

Counting lemma for a fixed graph. Let L be a graph on a finite type β with k = card β vertices, and s : β → Finset α parts of a graph G such that for every edge xy of L, all subsets A ⊆ s x, B ⊆ s y with #A ≥ η #(s x), #B ≥ η #(s y) have edge density at least d, where 0 < η ≤ 1, 0 < d ≤ 1, 2 k η ≤ d ^ k and every part has at least 4 k / d ^ k elements. Then there are at least (d ^ k / 4) ^ k ∏ₓ #(s x) injective maps f : β → α with f x ∈ s x for every x that send edges of L to edges of G.

theorem RemovalLemma.le_labelledCopyCount_of_deleteFar {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (α : Type) [inst : Fintype α] [DecidableEq α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj], G.DeleteFar (fun (G' : SimpleGraph α) => H.Free G') (ε * ↑(Fintype.card α ^ 2)) → δ * ↑(Fintype.card α) ^ Fintype.card β ≤ ↑(G.labelledCopyCount H)

Graph removal lemma, far form. The contrapositive of Conlon–Fox, Graph removal lemmas, Theorem 1.1. For every finite graph H and every ε > 0 there is δ > 0 such that every finite graph on n vertices that is ε n²-far from being H-free has at least δ n ^ (card β) labelled copies of H.

theorem RemovalLemma.graph_removal {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (α : Type) [inst : Fintype α] [DecidableEq α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj], ↑(G.labelledCopyCount H) < δ * ↑(Fintype.card α) ^ Fintype.card β → ∃ G' ≤ G, ∃ (x : DecidableRel G'.Adj), ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ H.Free G'

Graph removal lemma. See Conlon–Fox, Graph removal lemmas, Theorem 1.1. For every finite graph H and every ε > 0 there is δ > 0 such that every finite graph on n vertices with fewer than δ n ^ (card β) labelled copies of H has an H-free subgraph obtained by deleting fewer than ε n² edges.