Lax Lean Archive

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

Lifting a tree decomposition through a bounded blow-up

Lax263307.BlowUpDecompositions · concepts/Lax263307/BlowUpDecompositions.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

    Suppose GG has treewidth at most ww, and every vertex is replaced by at most ss independent copies. The blow-up has a tree decomposition whose bags have size at most s(w+1)s(w+1).

    Concept map
    6 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.BlowUpIndependentSets
    2import Lax228581.Treewidth
    3
    4/-!
    5---
    6title: Lifting a tree decomposition through a bounded blow-up
    7type: theorem
    8---
    9Suppose GG has treewidth at most ww, and every vertex is replaced by at
    10most ss independent copies. The blow-up has a tree decomposition whose
    11bags have size at most s(w+1)s(w+1).
    12
    13# Formalization notes
    14
    15The original decomposition tree is retained, and each vertex in a bag is
    16replaced by all its copies. An empty fibre contributes no vertices.
    17The conclusion is expressed directly as a bag-size bound using the
    18registered `Lax228581.Treewidth.TreeDecomposition` definition.
    19
    20# Attribution
    21
    22Bonnet–Chang, the tree-decomposition construction in the proof of Lemma 16.
    23-/
    24
    25namespace Lax263307.BlowUpDecompositions
    26
    27open IndependentBlowUp Lax228581.Treewidth
    28
    29/-- Replacing every bag vertex by its copies multiplies bag sizes by at most `s`. -/
    30axiom bounded_blowup_decomposition {n : ℕ} (G : SimpleGraph (Fin n))
    31 (copies : Fin n → ℕ) (s w : ℕ) (bounded : ∀ v, copies v ≤ s)
    32 (width : HasTreewidthAtMost G w) :
    33 ∃ D : TreeDecomposition (graph G copies), ∀ i, (D.bag i).card ≤ s * (w + 1)
    34
    35end Lax263307.BlowUpDecompositions
    36
    Show Proof
    Formalization notes

    The original decomposition tree is retained, and each vertex in a bag is replaced by all its copies. An empty fibre contributes no vertices. The conclusion is expressed directly as a bag-size bound using the registered Lax228581.Treewidth.TreeDecompositionLax228581.Treewidth.TreeDecomposition definition.

    Attribution

    Bonnet–Chang, the tree-decomposition construction in the proof of Lemma 16.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…