Lax Lean Archive

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

Rank-width

Lax183560.Rankwidth · concepts/Lax183560/Rankwidth.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 rank-width of a graph is the minimum, over all branch decompositions of its vertex set, of the maximum cut-rank. The cut-rank of a cut is the rank over the two-element field of the adjacency matrix between its two sides. The empty graph has rank-width zero.

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

    Lean source view on GitHub

    1import Lax183560.BranchDecompositions
    2import Lax183560.CutRank
    3
    4/-!
    5---
    6title: Rank-width
    7type: definition
    8---
    9The rank-width of a graph is the minimum, over all branch decompositions of
    10its vertex set, of the maximum cut-rank. The cut-rank of a cut is the rank
    11over the two-element field of the adjacency matrix between its two sides.
    12The empty graph has rank-width zero.
    13-/
    14
    15namespace Lax183560.Rankwidth
    16
    17open Lax183560.BranchDecompositions Lax183560.CutRank
    18
    19/-- Existence of a vertex branch decomposition of cut-rank at most `k`. -/
    20def HasRankwidthAtMost {V : Type} [Fintype V] [DecidableEq V]
    21 (G : SimpleGraph V) (k : ℕ) : Prop :=
    22 IsEmpty V ∨
    23 ∃ t : BranchDecompositions.BinaryTree V,
    24 t.Valid Finset.univ ∧
    25 t.cutWidth (cutRank G) ≤ k
    26
    27/-- The minimum maximum binary cut-rank. -/
    28noncomputable def rankwidth {V : Type} [Fintype V] [DecidableEq V]
    29 (G : SimpleGraph V) : ℕ :=
    30 sInf {k | HasRankwidthAtMost G k}
    31
    32end Lax183560.Rankwidth
    33
    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…