Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Treewidth loss under edge deletion

Lax263307.EdgeDeletionWidth · concepts/Lax263307/EdgeDeletionWidth.lean · lax-263307

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Deleting qq edges reduces treewidth by at most qq. Choose one endpoint of each deleted edge and add all chosen vertices to every bag of a decomposition of the remaining graph. This restores edge coverage and increases bag sizes by at most qq.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax228581.Treewidth
    2import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
    3import Mathlib.Data.Fintype.Fin
    4
    5/-!
    6---
    7title: Treewidth loss under edge deletion
    8type: theorem
    9---
    10Deleting qq edges reduces treewidth by at most qq. Choose one endpoint of
    11each deleted edge and add all chosen vertices to every bag of a decomposition
    12of the remaining graph. This restores edge coverage and increases bag sizes
    13by at most qq.
    14
    15# Attribution
    16
    17The edge-deletion estimate used to retain linear treewidth after discarding
    18long sampled paths in Bonnet–Chang, Lemma 11.
    19-/
    20
    21namespace Lax263307.EdgeDeletionWidth
    22
    23open Lax228581.Treewidth
    24
    25/-- A width bound after edge deletion gives this bound for the original graph. -/
    26axiom restore_edges {n : ℕ} (G : SimpleGraph (Fin n)) (F : Finset (Sym2 (Fin n)))
    27 (w : ℕ) (width : HasTreewidthAtMost (G.deleteEdges (↑F : Set (Sym2 (Fin n)))) w) :
    28 HasTreewidthAtMost G (w + F.card)
    29
    30end Lax263307.EdgeDeletionWidth
    31
    Show Proof

    Attribution

    The edge-deletion estimate used to retain linear treewidth after discarding long sampled paths in Bonnet–Chang, Lemma 11.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…