Lax Lean Archive

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

Tree-decomposition transfer through connected vertex representations

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

    Represent each vertex of HH by a nonempty connected vertex set of GG, with intersecting sets for every edge of HH. Suppose at most BB represented vertices use any one vertex of GG. A tree decomposition of GG with bags of size at most ww then gives a tree decomposition of HH with bags of size at most BwBw.

    Concept map
    3 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 Lax263307.ConnectedBags
    2
    3/-!
    4---
    5title: Tree-decomposition transfer through connected vertex representations
    6type: theorem
    7---
    8Represent each vertex of HH by a nonempty connected vertex set of GG, with
    9intersecting sets for every edge of HH. Suppose at most BB represented
    10vertices use any one vertex of GG. A tree decomposition of GG with bags
    11of size at most ww then gives a tree decomposition of HH with bags of
    12size at most BwBw.
    13
    14# Attribution
    15
    16The connected-set transfer used in Bonnet–Chang, Lemma 9.
    17-/
    18
    19namespace Lax263307.ConnectedRepresentations
    20
    21open Lax228581.Treewidth
    22
    23/-- A connected vertex set in `G` for each vertex of `H`. -/
    24structure Representation {t n : ℕ} (H : SimpleGraph (Fin t))
    25 (G : SimpleGraph (Fin n)) where
    26 /-- The vertices used by a represented vertex. -/
    27 carrier : Fin t → Finset (Fin n)
    28 /-- Each carrier is nonempty and connected. -/
    29 connected : ∀ v, (G.induce (↑(carrier v) : Set (Fin n))).Connected
    30 /-- Carriers of adjacent vertices intersect. -/
    31 touching : ∀ u v, H.Adj u v → ∃ a, a ∈ carrier u ∧ a ∈ carrier v
    32
    33/-- Which represented vertices use a particular host vertex. -/
    34def users {t n : ℕ} {H : SimpleGraph (Fin t)} {G : SimpleGraph (Fin n)}
    35 (R : Representation H G) (a : Fin n) : Finset (Fin t) :=
    36 Finset.univ.filter fun v => a ∈ R.carrier v
    37
    38/-- Transfer a decomposition with a uniform bound on the representation load. -/
    39axiom transfer_decomposition {t n : ℕ} (H : SimpleGraph (Fin t))
    40 (G : SimpleGraph (Fin n)) (R : Representation H G)
    41 (B w : ℕ) (load_bound : ∀ a, (users R a).card ≤ B)
    42 (D : TreeDecomposition G) (bag_bound : ∀ i, (D.bag i).card ≤ w) :
    43 ∃ D' : TreeDecomposition H, ∀ i, (D'.bag i).card ≤ B * w
    44
    45end Lax263307.ConnectedRepresentations
    46
    Show Proof

    Attribution

    The connected-set transfer used in Bonnet–Chang, Lemma 9.

    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…