definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
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.
Lean source view on GitHub
| 1 | import Lax48.TwinWidth |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Cographs |
| 6 | type: definition |
| 7 | --- |
| 8 | A finite graph is a cograph if it has twin-width zero. Equivalently, it can |
| 9 | be reduced to one vertex by repeatedly contracting a pair of twins, without |
| 10 | ever creating a red edge. |
| 11 | |
| 12 | # Formalization notes |
| 13 | |
| 14 | The definition uses `HasTwinWidthAtMost G 0` rather than the numerical |
| 15 | equality `twinWidth G = 0`. For finite graphs these are equivalent, while the |
| 16 | bounded predicate exposes the width-zero contraction sequence that witnesses |
| 17 | the property. The bound really is zero, not one: the width convention counts |
| 18 | the maximum red degree and a cograph contraction creates no red adjacency. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax214022.Cographs |
| 22 | |
| 23 | open Lax48.TwinWidth |
| 24 | |
| 25 | /-- A finite graph is a cograph when it admits a contraction sequence of red |
| 26 | degree zero. -/ |
| 27 | def IsCograph {V : Type} [Fintype V] [DecidableEq V] |
| 28 | (G : SimpleGraph V) : Prop := |
| 29 | HasTwinWidthAtMost G 0 |
| 30 | |
| 31 | end Lax214022.Cographs |
| 32 |
Formalization notes
The definition uses rather than the numerical equality . 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.
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments