Lax Lean Archive

Numbering finite graphs and the size of their encoding

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

proven

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

    Theorem

    A bijective numbering of the vertices of a finite simple graph gives a Boolean adjacency matrix on 0,…,n−10,\ldots,n-1 with the same clique number. Its binary encoding has exactly n+1+n2n+1+n^2 bits. These facts connect abstract consistency graphs to the input representation used by approximation algorithms.

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

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 cliqueNumber_numbered proven

    2 encoding_length proven

    Lean source view on GitHub

    1import Lax323828.Graphs
    2
    3/-!
    4---
    5title: Numbering finite graphs and the size of their encoding
    6type: theorem
    7---
    8A bijective numbering of the vertices of a finite simple graph gives a
    9Boolean adjacency matrix on 0,…,n−10,\ldots,n-1 with the same clique number.
    10Its binary encoding has exactly n+1+n2n+1+n^2 bits. These facts connect abstract
    11consistency graphs to the input representation used by approximation
    12algorithms.
    13-/
    14
    15namespace Lax323828.GraphEncoding
    16
    17open Graphs
    18
    19/-- Transfer adjacency along the vertex numbering `e` to obtain a Boolean matrix. -/
    20def numbered {α : Type} {n : ℕ} (G : SimpleGraph α) [DecidableRel G.Adj]
    21 (e : Fin n ≃ α) : Graph n where
    22 adjacent u v := decide (G.Adj (e u) (e v))
    23 loopless v := decide_eq_false (G.loopless.irrefl (e v))
    24 symmetric u v := decide_eq_decide.mpr (G.adj_comm (e u) (e v))
    25
    26/-- Relabeling the vertices preserves the largest clique size. -/
    27axiom cliqueNumber_numbered {α : Type} [Fintype α] {n : ℕ}
    28 (G : SimpleGraph α) [DecidableRel G.Adj] (e : Fin n ≃ α) :
    29 (numbered G e).cliqueNumber = G.cliqueNum
    30
    31/-- The encoding contains the unary vertex count, one separator, and `n²` matrix entries. -/
    32axiom encoding_length {n : ℕ} (G : Graph n) :
    33 G.encode.length = n + 1 + n * n
    34
    35end Lax323828.GraphEncoding
    36
    Show ProofShow Proof
    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…