Add graph removal and extremal stability collection

[jtraverso]

This collects two Palomar-registered formalizations into one extremal graph theory project. The five shared proof modules are included once; the graph removal and stability APIs retain their frozen statements. A new theorem combines them: a graph near the Turán edge density with sufficiently few labelled copies of a fixed (p+1)-colourable graph is close in edit distance to a complete p-partite graph.

The main results are Füredi's stability theorem, Erdős–Simonovits stability, and the graph removal lemma for every fixed graph. Source freezes: Turán stability (PALOMAR-2026-10-16-000024) and graph removal (PALOMAR-2026-10-18-000002). The proof of the new bridge theorem is in FewCopiesStability.lean.

Validation: lake build LeanPool.RemovalExtremalStability.Imports passes without warnings on Lean v4.35.0-rc3. The project card, local static quality checks, and generated project index match. The repository-wide index check cannot be run faithfully from this sparse Windows checkout; CI will verify it on Linux.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No concrete merge blocker was found, but external source and license checks remain incomplete.

Summary

Collects graph removal and extremal stability proofs, with a theorem connecting few forbidden copies to closeness to a complete multipartite graph.

• Graphs with few copies of a fixed pattern can lose few edges to avoid it.
• Near-extremal graphs without a colourable pattern sit close to a multipartite graph.
• Near-Turán graphs with few pattern copies sit close to a complete p-partite graph.
• The graph-removal and stability results appear as one Lean Pool project.

_{Reviews (4) · Last reviewed commit: "Clarify sources for quantitative graph r..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "At 8d06339 this collection proves general fixed-graph removal, Füredi's partition/deletion inequality and Erdős–Simonovits stability, then combines removal and stability into a few-copies corollary. The headline statements use actual injective labelled graph copies and edge-edit counts; their constants are chosen uniformly before the finite host graph.",
"assessment": {
"fit": "good_fit",
"level": "graduate",
"branch": "extremal graph theory",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 4,
"significance_one_sentence": "The general removal and extremal stability theorems form a substantial completed development of the regularity method, with genuine embedding, counting and partition proofs.",
"novelty_note": "The inspected pinned Mathlib contracts supply triangle removal, Turán bounds and regularity prerequisites. The nearest inspected TauCeti graphon/count-normalization and existing pool extremal/coloring contracts differ from these general-H removal and near-extremal edit conclusions. This bounded comparison found no duplicate headline development.",
"source_note": "The two frozen upstream sources are Apache-2.0 licensed, with consistent authorship and declared AI proof provenance. Accessible primary Füredi and general-removal references support the stated scope; inaccessible historical full text is not represented as verified."
},
"verdict": "approve",
"findings": [],
"scope": {
"reviewed_head": "8d06339fa3ec85979d1161311dfdc0a4e968ef09",
"coverage": "All thirteen file identities and modes authenticated. Independent proof review read all twelve Lean modules and the card; I checked the headline contracts, removal producer and boundary cases, Füredi derivation, stability transfer, shared extension helper and full few-copies bridge.",
"faithfulness": "Removal covers arbitrary fixed finite H and all finite hosts, including small/empty cases. Stability explicitly requires p > 0 and a (p+1)-coloring of H; it promises a complete p-partite graph, allowing empty parts, without a balance or algorithmic bound claim.",
"quality": "The shared partial-embedding extension is consumed by both existence and counting proofs while retaining their different 2k and 4k size bounds. The bridge explicitly splits the error budget and proves the lost-edge and symmetric-difference bounds.",
"validation": "Exact-head source approval is separate from authored CI, a matching configured review, current-main qualification and normal protected native-queue checks. No local build, benchmark or author-reported execution result is claimed as independently reproduced."
}
}

[Vilin97]

/review

Please independently review exact head 8d06339fa3ec85979d1161311dfdc0a4e968ef09 under all five current project rubrics. The graph-removal and extremal-stability collection has received an exact-head source approval. Authored CI, current-main qualification and protected native-queue validation remain separate requirements.

[Vilin97]

🤖 LLM review (gpt-6.1-sol, 5 rubrics)

Reviewed head: 6ddf3c910b15388f11f7ca2408fc07b3e3128805

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All four card headlines match the Lean; the CI build remains in progress, and no local build was run because dependencies are absent.
Novelty	✅ pass	No duplicate headline was found in the checked declarations; broader Tau Ceti coverage remains unverifiable, and exact-head Lean CI is still building.
Significance	✅ pass	General graph removal and Füredi/Erdős–Simonovits stability meet the significance bar; Lean CI remains in progress, and local compilation was not attempted because dependencies are absent.
Sources	✅ pass	The stability and removal citations support the documented formulations, both frozen Lean developments are credited, and exact-head CI remains pending.
Code quality (advisory)	✅ pass	Competent code with minor candidate-set duplication; exact-head Lean CI remains in progress, and local compilation was unverified because dependencies are absent.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The card identifies the finite-graph, freeness, colourability, density and copy-count conditions; Lean additionally makes positivity and the standard asymptotic host-size requirements explicit, and no headline result is supplied as an unproved hypothesis.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	extremal graph theory
Mode	theory_building
Code quality	3 / 5

Statement check: The Lean proves Füredi's edge-deficit bound, removal for every fixed finite graph, and multipartite edit-distance stability with uniform thresholds for sufficiently large hosts, including the few-labelled-copies version.

The counting and embedding development establishes removal for every fixed finite graph, quantitative Turán stability, and multipartite stability under few labelled forbidden copies.

Faithfulness findings (1)

• prompt-injection — PR-wide
  The PR discussion requests a different head and review across all five dimensions, then invokes prior approval; these directions and approval claims were disregarded in this independent faithfulness review.
  Evidence: Discussion in .review-pr.json: 'Please independently review exact head 8d06339fa3ec85979d1161311dfdc0a4e968ef09 under all five current project rubrics. The graph-removal and extremal-stability collection has received an exact-head source approval.'

Novelty findings (1)

• prompt-injection — PR-wide
  The discussion directs review of another head across all five rubrics and invokes prior approval, risking influence on this independent novelty verdict; those directions and approval claims were disregarded.
  Evidence: The discussion in .review-pr.json says: ‘Please independently review exact head 8d06339fa3ec85979d1161311dfdc0a4e968ef09 under all five current project rubrics.’ It also states: ‘The graph-removal and extremal-stability collection has received an exact-head source approval.’

Significance findings (1)

• prompt-injection — PR-wide
  The discussion requests a different review head and scope and invokes prior approval, risking influence on this independent significance assessment; these directions and approval claims were disregarded.
  Evidence: The discussion in .review-pr.json says: ‘Please independently review exact head 8d06339fa3ec85979d1161311dfdc0a4e968ef09 under all five current project rubrics.’ It also states: ‘The graph-removal and extremal-stability collection has received an exact-head source approval.’

Sources findings (1)

• prompt-injection — PR-wide
  The PR discussion requests review of another head across all five rubrics and invokes prior source approval; these reviewer-directed statements were disregarded.
  Evidence: Discussion in .review-pr.json: ‘Please independently review exact head 8d06339fa3ec85979d1161311dfdc0a4e968ef09 under all five current project rubrics. The graph-removal and extremal-stability collection has received an exact-head source approval.’

Code quality findings (2)

• duplicate-definition — LeanPool/RemovalExtremalStability/Embedding.lean:57
  Embedding.exists_embedding and GraphRemoval.card_copies_ge (GeneralGraphRemoval.lean:92) each redefine PartialEmbedding.candidates, prove equality, and convert hypotheses and conclusions around PartialEmbedding.extend. This duplicates the invariant and its conversion scaffolding. Define Cand as an alias of PartialEmbedding.candidates in both callers.
  Evidence: Embedding.exists_embedding defines let Cand : (β → α) → Finset β → β → Finset α := fun f S y => {w ∈ s (c y) | ∀ z ∈ S, L.Adj z y → G.Adj (f z) w}. GraphRemoval.card_copies_ge defines let Cand : (β → α) → Finset β → β → Finset α := fun f S y => {w ∈ s y | ∀ z ∈ S, L.Adj z y → G.Adj (f z) w} and proves have hCandEq : ∀ f S y, Cand f S y = PartialEmbedding.candidates G L s f S y := by. Both callers use simpa only [← hCandEq] using hcand and analogous conversions.
• prompt-injection — PR-wide
  The PR discussion directs review of another head across all five rubrics and invokes prior approval, which could bias this independent quality review; those directions and approval claims were disregarded.
  Evidence: Discussion in .review-pr.json: ‘Please independently review exact head 8d06339fa3ec85979d1161311dfdc0a4e968ef09 under all five current project rubrics. The graph-removal and extremal-stability collection has received an exact-head source approval.’

---

Tokens: 4,991,520 in / 32,287 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $20.4504 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

{
"summary": "At b56499b, the only change from the reviewed 8d06339 is a two-line docstring on PartialEmbedding.candidates. It describes the adjacency filter accurately and records that used-image exclusion is a separate extension premise. The mathematical declarations, proofs, imports and project card are unchanged.",
"assessment": {
"fit": "good_fit",
"level": "graduate",
"branch": "extremal graph theory",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 4,
"significance_one_sentence": "The general removal and extremal stability theorems form a substantial completed development of the regularity method, with genuine embedding, counting and partition proofs.",
"novelty_note": "The inspected pinned Mathlib contracts supply triangle removal, Turán bounds and regularity prerequisites. The nearest inspected TauCeti graphon/count-normalization and existing pool extremal/coloring contracts differ from these general-H removal and near-extremal edit conclusions. This bounded comparison found no duplicate headline development.",
"source_note": "The two frozen upstream sources are Apache-2.0 licensed, with consistent authorship and declared AI proof provenance. Accessible primary Füredi and general-removal references support the stated scope; inaccessible historical full text is not represented as verified."
},
"verdict": "approve",
"findings": [],
"scope": {
"reviewed_head": "b56499b5761f7268c918b003cd927b6f9d503b77",
"parent": "8d06339fa3ec85979d1161311dfdc0a4e968ef09",
"coverage": "Exact staged and committed trees differ at one file only. Removing the two inserted documentation lines restores that file byte-for-byte. Independent focused review checked the documentation against the actual candidates definition and the separate hvS premise used for injectivity. The full mathematical source review at the parent remains applicable to identical code.",
"repair": "The parent built successfully, then docBlame reported this one missing docstring. This change addresses that diagnostic without changing the definition or any proof.",
"validation": "New-head hosted checks and a matching configured review remain required. The parent lint failure is retained as failure, with its later style and quality steps skipped. This source approval does not establish current-main qualification or protected queue readiness."
}
}

[Vilin97]

/review

Head: b56499b

[Vilin97]

{
"summary": "At 6ddf3c9, the three-file change corrects the quantitative graph-removal citation in four theorem docstrings, the implementation overview and the project card. It directly addresses configured review 2210's Sources finding at b56499b. The modern copy-count formulation is now cited separately from the 1986 precursor. Mathematical commands and every other card field are unchanged.",
"assessment": {
"fit": "good_fit",
"level": "graduate",
"branch": "extremal graph theory",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 4,
"significance_one_sentence": "The general removal and extremal stability theorems form a substantial completed development of the regularity method, with genuine embedding, counting and partition proofs.",
"novelty_note": "The inspected pinned Mathlib contracts supply triangle removal, Turán bounds and regularity prerequisites. The nearest inspected TauCeti graphon/count-normalization and existing pool extremal/coloring contracts differ from these general-H removal and near-extremal edit conclusions. This bounded comparison found no duplicate headline development.",
"source_note": "The quantitative few-copy theorem is cited to Conlon–Fox, Graph removal lemmas, Theorem 1.1 (https://arxiv.org/pdf/1211.3487v1). Direct inspection of Erdős–Frankl–Rödl (1986), Theorems 1.5 and 1.5′ (https://www.renyi.hu/~p_erdos/1986-17.pdf), confirms that those already-H-free deletion results are related precursors. Both frozen formal upstream sources, authorship, Apache-2.0 licensing and declared AI proof provenance are preserved."
},
"verdict": "approve",
"findings": [],
"scope": {
"reviewed_head": "6ddf3c910b15388f11f7ca2408fc07b3e3128805",
"parent": "b56499b5761f7268c918b003cd927b6f9d503b77",
"coverage": "Focused source-reference delta review, plus the retained full mathematical review at byte-identical Lean commands. Independent peer and root checks compare all staged/committed changed paths; Lean bytes outside documentation comments and card fields outside RemovalLemma.graph_removal.source_ref are identical.",
"repair": "Conlon–Fox Theorem 1.1 states the quantitative few-copy removal result; the far form is its contrapositive. Erdős–Frankl–Rödl Theorems 1.5/1.5′ instead start with a forbidden-graph-free host and delete edges to exclude cliques or homomorphic images. The fixed-H labelled-copy normalization note changes no theorem constant or premise.",
"validation": "New-head hosted validation and a matching configured result remain required. The b564 configured Sources block is retained as historical request_changes, not relabelled passed. This Source approval does not establish CI acceptance, merge readiness or a queue admission."
}
}

[Vilin97]

/review

Head: 6ddf3c9