Lax Lean Archive

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

Almost-embedding transfer with isolated source vertices

Lax263307.IsolatedEmbeddingTransfer · concepts/Lax263307/IsolatedEmbeddingTransfer.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 of a graph of maximum degree at most dd transfers a host decomposition with bag size at most ww to source bags of size at most max⁡{1,2dw}\max\{1,2dw\}, even if the source has isolated vertices. Restrict to its nonisolated vertices, apply the connected-carrier transfer, then attach a singleton leaf bag for each omitted isolated vertex.

    Concept map
    5 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.AlmostEmbeddings
    2
    3/-!
    4---
    5title: Almost-embedding transfer with isolated source vertices
    6type: theorem
    7---
    8An almost-embedding of a graph of maximum degree at most dd transfers a
    9host decomposition with bag size at most ww to source bags of size at most
    10max⁡{1,2dw}\max\{1,2dw\}, even if the source has isolated vertices. Restrict to
    11its nonisolated vertices, apply the connected-carrier transfer, then attach
    12a singleton leaf bag for each omitted isolated vertex.
    13
    14# Attribution
    15
    16The treewidth transfer needed after discarding long routes in Bonnet–Chang,
    17Lemma 11, extending the no-isolates formulation of Lemma 9.
    18-/
    19
    20namespace Lax263307.IsolatedEmbeddingTransfer
    21
    22open Lax263307.AlmostEmbeddings Lax228581.Treewidth
    23
    24axiom transfer_decomposition {t n : ℕ} (H : SimpleGraph (Fin t)) [DecidableRel H.Adj]
    25 (G : SimpleGraph (Fin n)) (E : AlmostEmbedding H G) (d w : ℕ)
    26 (degree_bound : ∀ v, H.degree v ≤ d)
    27 (D : TreeDecomposition G) (bag_bound : ∀ i, (D.bag i).card ≤ w) :
    28 ∃ D' : TreeDecomposition H, ∀ i, (D'.bag i).card ≤ max 1 (2 * d * w)
    29
    30end Lax263307.IsolatedEmbeddingTransfer
    31
    Show Proof

    Attribution

    The treewidth transfer needed after discarding long routes in Bonnet–Chang, Lemma 11, extending the no-isolates formulation of 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…