Lax Lean Archive

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

Finite graphs and their binary encoding

Lax253009.Graphs · concepts/Lax253009/Graphs.lean · lax-253009

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 claimOpen 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 Lax253009.Graphs
    19
    20structure Graph (n : ℕ) where
    21 adjacent : Fin n → Fin n → Bool
    22 loopless : ∀ v, adjacent v v = false
    23 symmetric : ∀ u v, adjacent u v = adjacent v u
    24
    25def Graph.simpleGraph {n : ℕ} (G : Graph n) : SimpleGraph (Fin n) where
    26 Adj u v := G.adjacent u v = true
    27 symm := ⟨fun u v h ↦ by rw [← G.symmetric]; exact h⟩
    28 loopless := ⟨fun v ↦ by simp [G.loopless]⟩
    29
    30def Graph.encode {n : ℕ} (G : Graph n) : List Bool :=
    31 List.replicate n true ++ [false] ++
    32 (List.finRange n).flatMap (fun u ↦ (List.finRange n).map (G.adjacent u))
    33
    34noncomputable def Graph.cliqueNumber {n : ℕ} (G : Graph n) : ℕ :=
    35 G.simpleGraph.cliqueNum
    36
    37end Lax253009.Graphs
    38
    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…