Lax Lean Archive

Cographs

Lax214022.Cographs · concepts/Lax214022/Cographs.lean · lax-214022

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

    A finite graph is a cograph if it has twin-width zero. Equivalently, it can be reduced to one vertex by repeatedly contracting a pair of twins, without ever creating a red edge.

    Concept map
    2 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    Lean source view on GitHub

    1import Lax228581.TwinWidth
    2
    3/-!
    4---
    5title: Cographs
    6type: definition
    7---
    8A finite graph is a cograph if it has twin-width zero. Equivalently, it can
    9be reduced to one vertex by repeatedly contracting a pair of twins, without
    10ever creating a red edge.
    11
    12# Formalization notes
    13
    14The definition uses `HasTwinWidthAtMost G 0` rather than the numerical
    15equality `twinWidth G = 0`. For finite graphs these are equivalent, while the
    16bounded predicate exposes the width-zero contraction sequence that witnesses
    17the property. The bound really is zero, not one: the width convention counts
    18the maximum red degree and a cograph contraction creates no red adjacency.
    19-/
    20
    21namespace Lax214022.Cographs
    22
    23open Lax228581.TwinWidth
    24
    25/-- A finite graph is a cograph when it admits a contraction sequence of red
    26degree zero. -/
    27def IsCograph {V : Type} [Fintype V] [DecidableEq V]
    28 (G : SimpleGraph V) : Prop :=
    29 HasTwinWidthAtMost G 0
    30
    31end Lax214022.Cographs
    32
    Formalization notes

    The definition uses HasTwinWidthAtMostG0HasTwinWidthAtMost G 0 rather than the numerical equality twinWidthG=0twinWidth G = 0. For finite graphs these are equivalent, while the bounded predicate exposes the width-zero contraction sequence that witnesses the property. The bound really is zero, not one: the width convention counts the maximum red degree and a cograph contraction creates no red adjacency.

    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…