Lax Lean Archive

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

Modular-width

Lax183560.ModularWidth · concepts/Lax183560/ModularWidth.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 modular-width of a graph is the minimum, over all modular decompositions, of the maximum number of parts in a substitution other than a disjoint union or a complete join. Disjoint unions and complete joins do not contribute to the width. Under this convention, cographs have modular-width zero.

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

    Lean source view on GitHub

    1import Lax183560.ModularDecomposition
    2import Mathlib.Order.Lattice.Nat
    3
    4/-!
    5---
    6title: Modular-width
    7type: definition
    8---
    9The modular-width of a graph is the minimum, over all modular decompositions,
    10of the maximum number of parts in a substitution other than a disjoint union
    11or a complete join. Disjoint unions and complete joins do not contribute to
    12the width. Under this convention, cographs have modular-width zero.
    13-/
    14
    15namespace Lax183560.ModularWidth
    16
    17open Lax183560.ModularDecomposition
    18
    19/-- Existence of a modular decomposition with substitution arity bounded by k. -/
    20def HasModularWidthAtMost (V : Type) (G : SimpleGraph V) (k : ℕ) : Prop :=
    21 ModularDecomposition V G k
    22
    23/-- The least maximum arity of a non-union, non-join substitution. -/
    24noncomputable def modularWidth {V : Type} [Fintype V] [DecidableEq V]
    25 (G : SimpleGraph V) : ℕ :=
    26 sInf {k | HasModularWidthAtMost V G k}
    27
    28end Lax183560.ModularWidth
    29
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…