Lax Lean Archive

Finite graphs and their binary encoding

Lax323828.Graphs · concepts/Lax323828/Graphs.lean · lax-323828

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 graph on nn vertices is a symmetric Boolean adjacency matrix with zero diagonal. Its vertices are 0,…,n−10,\ldots,n-1. We encode it by nn one-bits, one zero-bit, and its complete adjacency matrix in row-major order. The encoding has length n+1+n2n+1+n^2, so polynomial time in its length is equivalent to polynomial time in the number of vertices.

    The clique number ω(G)\omega(G) is the maximum cardinality of a clique.

    Concept map
    1 concept; 13 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Clique
    2import Mathlib.Data.List.FinRange
    3
    4/-!
    5---
    6title: Finite graphs and their binary encoding
    7type: definition
    8---
    9A graph on nn vertices is a symmetric Boolean adjacency matrix with zero
    10diagonal. Its vertices are 0,…,n−10,\ldots,n-1. We encode it by nn one-bits,
    11one zero-bit, and its complete adjacency matrix in row-major order.
    12The encoding has length n+1+n2n+1+n^2, so polynomial time in its length is
    13equivalent to polynomial time in the number of vertices.
    14
    15The clique number ω(G)\omega(G) is the maximum cardinality of a clique.
    16-/
    17
    18namespace Lax323828.Graphs
    19
    20/-- A simple graph represented by a symmetric Boolean adjacency matrix with zero diagonal. -/
    21structure Graph (n : ℕ) where
    22 /-- Whether the two labeled vertices are adjacent. -/
    23 adjacent : Fin n → Fin n → Bool
    24 /-- No vertex is adjacent to itself. -/
    25 loopless : ∀ v, adjacent v v = false
    26 /-- Adjacency is unchanged when the endpoints are exchanged. -/
    27 symmetric : ∀ u v, adjacent u v = adjacent v u
    28
    29/-- Read the Boolean matrix as a mathematical simple graph. -/
    30def Graph.simpleGraph {n : ℕ} (G : Graph n) : SimpleGraph (Fin n) where
    31 Adj u v := G.adjacent u v = true
    32 symm := ⟨fun u v h ↦ (G.symmetric u v).symm.trans h⟩
    33 loopless := ⟨fun v h ↦ Bool.noConfusion ((G.loopless v).symm.trans h)⟩
    34
    35/-- The vertex count in unary, a separator, and the adjacency matrix in row order. -/
    36def Graph.encode {n : ℕ} (G : Graph n) : List Bool :=
    37 List.replicate n true ++ [false] ++
    38 (List.finRange n).flatMap (fun u ↦ (List.finRange n).map (G.adjacent u))
    39
    40/-- The maximum number of pairwise adjacent vertices. -/
    41noncomputable def Graph.cliqueNumber {n : ℕ} (G : Graph n) : ℕ :=
    42 G.simpleGraph.cliqueNum
    43
    44end Lax323828.Graphs
    45
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…