Lax Lean Archive

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

Branchwidth

Lax183560.Branchwidth · concepts/Lax183560/Branchwidth.lean · lax-183560

definition

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

    Definition

    The branchwidth of a graph is the minimum, over all branch decompositions of its edge set, of the maximum size of a middle set. The middle set of a cut consists of the vertices incident with an edge on each side of the cut. Graphs with at most one edge have branchwidth zero.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax183560.BranchDecompositions
    2
    3/-!
    4---
    5title: Branchwidth
    6type: definition
    7---
    8The branchwidth of a graph is the minimum, over all branch decompositions of
    9its edge set, of the maximum size of a middle set. The middle set of a cut
    10consists of the vertices incident with an edge on each side of the cut.
    11Graphs with at most one edge have branchwidth zero.
    12-/
    13
    14namespace Lax183560.Branchwidth
    15
    16open Lax183560.BranchDecompositions
    17
    18/-- Number of vertices incident with an edge in `A` and an edge outside `A`. -/
    19noncomputable def middleSize {V : Type} [Fintype V] [DecidableEq V]
    20 (G : SimpleGraph V) (A : Finset (Sym2 V)) : ℕ :=
    21 {v : V | (∃ e : Sym2 V, e ∈ G.edgeSet ∧ e ∈ A ∧ v ∈ e) ∧
    22 (∃ e : Sym2 V, e ∈ G.edgeSet ∧ e ∉ A ∧ v ∈ e)}.ncard
    23
    24/-- A branch decomposition with every middle set of size at most `k`. -/
    25noncomputable def HasBranchwidthAtMost {V : Type} [Fintype V] [DecidableEq V]
    26 (G : SimpleGraph V) (k : ℕ) : Prop := by
    27 classical
    28 exact G.edgeSet = ∅ ∨
    29 ∃ t : BranchDecompositions.BinaryTree (Sym2 V),
    30 t.Valid G.edgeFinset ∧
    31 t.cutWidth (middleSize G) ≤ k
    32
    33/-- The minimum middle-set width of an edge branch decomposition. -/
    34noncomputable def branchwidth {V : Type} [Fintype V] [DecidableEq V]
    35 (G : SimpleGraph V) : ℕ :=
    36 sInf {k | HasBranchwidthAtMost G k}
    37
    38end Lax183560.Branchwidth
    39
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…