Lax Lean Archive

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

Treewidth and Δ-forestwidth

Lax461425.TreewidthForestwidth · concepts/Lax461425/TreewidthForestwidth.lean · lax-461425

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

    A pattern has treewidth at most ww if, and only if, fwΔ(F)≤w\mathrm{fw}_\Delta(F) \leq w for some Δ≥1\Delta \geq 1. A decomposition witnessing fwΔ(F)≤w\mathrm{fw}_\Delta(F) \leq w is a tree decomposition with bags of size at most w+1w + 1. Conversely, rooting a tree decomposition of width at most ww at any node and adding a new root with an empty bag gives such a decomposition whose depth is at most the number of nodes plus one.

    Concept map
    12 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 exists_forestwidthLE_of_treewidthLE proven

    2 treewidthLE_of_forestwidthLE proven

    Lean source view on GitHub

    1import Lax461425.PatternWidths
    2import Lax461425.Forestwidth
    3
    4/-!
    5---
    6title: Treewidth and Δ-forestwidth
    7type: theorem
    8---
    9A pattern has treewidth at most ww if, and only if, fwΔ(F)≤w\mathrm{fw}_\Delta(F) \leq w for some
    10Δ≥1\Delta \geq 1. A decomposition witnessing fwΔ(F)≤w\mathrm{fw}_\Delta(F) \leq w is a tree
    11decomposition with bags of size at most w+1w + 1. Conversely, rooting a tree decomposition of
    12width at most ww at any node and adding a new root with an empty bag gives such a
    13decomposition whose depth is at most the number of nodes plus one.
    14-/
    15
    16namespace Lax461425.TreewidthForestwidth
    17
    18open HomomorphismPolynomials Forestwidth PatternWidths
    19
    20/-- A bounded-depth decomposition with empty root bag is a tree decomposition. -/
    21axiom treewidthLE_of_forestwidthLE {Δ w : ℕ} {F : Pattern} (h : ForestwidthLE Δ w F) :
    22 TreewidthLE w F
    23
    24/-- Every tree decomposition can be rooted below a new node with an empty bag. -/
    25axiom exists_forestwidthLE_of_treewidthLE {w : ℕ} {F : Pattern} (h : TreewidthLE w F) :
    26 ∃ Δ, 1 ≤ Δ ∧ ForestwidthLE Δ w F
    27
    28end Lax461425.TreewidthForestwidth
    29
    Show ProofShow Proof
    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…