Lax Lean Archive

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

Treewidth transfer through an almost-embedding

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

    An almost-embedding maps each vertex of HH into GG and assigns to each edge a connected vertex set joining its mapped endpoints. Sets assigned to nonincident edges are disjoint. If HH has maximum degree at most dd and no isolated vertices, a decomposition of GG with bags of size at most ww gives a decomposition of HH with bags of size at most 2dw2dw.

    Concept map
    4 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.ConnectedRepresentations
    2import Mathlib.Combinatorics.SimpleGraph.Finite
    3
    4/-!
    5---
    6title: Treewidth transfer through an almost-embedding
    7type: theorem
    8---
    9An almost-embedding maps each vertex of HH into GG and assigns to each edge
    10a connected vertex set joining its mapped endpoints. Sets assigned to
    11nonincident edges are disjoint. If HH has maximum degree at most dd and
    12no isolated vertices, a decomposition of GG with bags of size at most ww
    13gives a decomposition of HH with bags of size at most 2dw2dw.
    14
    15# Formalization notes
    16
    17The connected vertex sets can in particular be the supports of the simple
    18paths in the paper. This slightly more general definition keeps precisely
    19the properties needed for tree-decomposition transfer. Mapped vertices need
    20not be distinct, and singleton routes are allowed. An induced almost-embedding
    21also forbids edges between routes assigned to nonincident edges.
    22
    23# Attribution
    24
    25Bonnet–Chang, Lemma 9.
    26-/
    27
    28namespace Lax263307.AlmostEmbeddings
    29
    30open Lax228581.Treewidth
    31
    32/-- A connected route for every edge, disjoint for nonincident edges. -/
    33structure AlmostEmbedding {t n : ℕ} (H : SimpleGraph (Fin t))
    34 (G : SimpleGraph (Fin n)) where
    35 /-- Vertex images, with no injectivity requirement. -/
    36 vertexMap : Fin t → Fin n
    37 /-- Host vertices on each route. -/
    38 route : H.edgeSet → Finset (Fin n)
    39 /-- Each route is nonempty and connected. -/
    40 connected : ∀ e, (G.induce (↑(route e) : Set (Fin n))).Connected
    41 /-- A route contains the images of its edge's endpoints. -/
    42 endpoints : ∀ e v, v ∈ e.val → vertexMap v ∈ route e
    43 /-- Routes of nonincident edges share no host vertex. -/
    44 disjoint : ∀ e f, Disjoint e.val.toFinset f.val.toFinset → Disjoint (route e) (route f)
    45
    46/-- In addition, nonincident routes have no edges between them in the host. -/
    47def IsInduced {t n : ℕ} {H : SimpleGraph (Fin t)} {G : SimpleGraph (Fin n)}
    48 (E : AlmostEmbedding H G) : Prop :=
    49 ∀ e f, Disjoint e.val.toFinset f.val.toFinset →
    50 ∀ a ∈ E.route e, ∀ b ∈ E.route f, ¬G.Adj a b
    51
    52/-- The union of all routes incident to one represented vertex. -/
    53noncomputable def vertexCarrier {t n : ℕ} {H : SimpleGraph (Fin t)}
    54 {G : SimpleGraph (Fin n)} (E : AlmostEmbedding H G) (v : Fin t) : Finset (Fin n) := by
    55 classical
    56 exact Finset.univ.biUnion fun e : H.edgeSet => if v ∈ e.val then E.route e else ∅
    57
    58/-- An almost-embedding transfers decompositions with at most factor `2d` loss. -/
    59axiom transfer_decomposition {t n : ℕ} (H : SimpleGraph (Fin t))
    60 [DecidableRel H.Adj] (G : SimpleGraph (Fin n)) (E : AlmostEmbedding H G)
    61 (d w : ℕ) (degree_bound : ∀ v, H.degree v ≤ d)
    62 (no_isolates : ∀ v, ¬H.IsIsolated v)
    63 (D : TreeDecomposition G) (bag_bound : ∀ i, (D.bag i).card ≤ w) :
    64 ∃ D' : TreeDecomposition H, ∀ i, (D'.bag i).card ≤ 2 * d * w
    65
    66end Lax263307.AlmostEmbeddings
    67
    Show Proof
    Formalization notes

    The connected vertex sets can in particular be the supports of the simple paths in the paper. This slightly more general definition keeps precisely the properties needed for tree-decomposition transfer. Mapped vertices need not be distinct, and singleton routes are allowed. An induced almost-embedding also forbids edges between routes assigned to nonincident edges.

    Attribution

    Bonnet–Chang, Lemma 9.

    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…