Lax Lean Archive

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

Treedepth and Δ-forestwidth

Lax461425.TreedepthForestwidth · concepts/Lax461425/TreedepthForestwidth.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

    If fwΔ(F)≤w\mathrm{fw}_\Delta(F) \leq w, then td(F)≤(w+1)Δ\mathrm{td}(F) \leq (w + 1)\Delta: placing the vertices introduced at a node of the decomposition in a chain below those introduced at its ancestors gives an elimination forest. Conversely, if td(F)≤t\mathrm{td}(F) \leq t, then fwt(F)≤t−1\mathrm{fw}_t(F) \leq t - 1: the nodes of an elimination forest below a new root, each with the bag of vertices on its path to the root, form such a decomposition.

    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 forestwidthLE_of_treedepthLE proven

    2 treedepthLE_of_forestwidthLE proven

    Lean source view on GitHub

    1import Lax461425.PatternWidths
    2import Lax461425.Forestwidth
    3
    4/-!
    5---
    6title: Treedepth and Δ-forestwidth
    7type: theorem
    8---
    9If fwΔ(F)≤w\mathrm{fw}_\Delta(F) \leq w, then td(F)≤(w+1)Δ\mathrm{td}(F) \leq (w + 1)\Delta: placing the
    10vertices introduced at a node of the decomposition in a chain below those introduced at its
    11ancestors gives an elimination forest. Conversely, if td(F)≤t\mathrm{td}(F) \leq t, then
    12fwt(F)≤t−1\mathrm{fw}_t(F) \leq t - 1: the nodes of an elimination forest below a new root, each with
    13the bag of vertices on its path to the root, form such a decomposition.
    14-/
    15
    16namespace Lax461425.TreedepthForestwidth
    17
    18open HomomorphismPolynomials Forestwidth PatternWidths
    19
    20/-- Bounded-depth decompositions with bags of size at most `w + 1` give elimination forests
    21of height at most `(w + 1) * Δ`. -/
    22axiom treedepthLE_of_forestwidthLE {Δ w : ℕ} {F : Pattern} (h : ForestwidthLE Δ w F) :
    23 TreedepthLE ((w + 1) * Δ) F
    24
    25/-- Elimination forests of height at most `t` give decompositions of depth at most `t` with
    26bags of size at most `t`. -/
    27axiom forestwidthLE_of_treedepthLE {t : ℕ} {F : Pattern} (h : TreedepthLE t F) :
    28 ForestwidthLE t (t - 1) F
    29
    30end Lax461425.TreedepthForestwidth
    31
    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…