Lax Lean Archive

A Word-Sized Encoding of the Constructed Graphs

Lax920634.WordEncoding · concepts/Lax920634/WordEncoding.lean · lax-920634

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 is encoded by its order followed by one matching endpoint per vertex, in numerical vertex order. Consecutive ports in each cloud supply the path edges. Thus the encoding has exactly one more word than the graph has vertices. It determines the entire simple graph, including loop removal and merging of coincident edges.

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

    Lean source view on GitHub

    1import Lax920634.GraphEncoding
    2
    3/-!
    4---
    5title: A Word-Sized Encoding of the Constructed Graphs
    6type: definition
    7---
    8A graph is encoded by its order followed by one matching endpoint per vertex,
    9in numerical vertex order. Consecutive ports in each cloud supply the path
    10edges. Thus the encoding has exactly one more word than the graph has
    11vertices. It determines the entire simple graph, including loop removal and
    12merging of coincident edges.
    13
    14# Formalization notes
    15
    16The row number determines the base vertex and port by division and remainder
    17by the fixed degree. This encoding uses machine words for vertex labels,
    18rather than unary coordinates. The requested order is supplied as one word.
    19-/
    20
    21namespace Lax920634.WordEncoding
    22
    23open ZigZagConstruction GraphEncoding
    24
    25/-- The complete matching table, with its graph order as a header. -/
    26def table (k : ℕ) : List ℕ := order k ::
    27 (List.range (order k)).map (matchingNeighbor k)
    28
    29/-- Construct the word encoding for the same size selector as the binary constructor. -/
    30def construct (n : ℕ) : List ℕ := table (selectedLevel n)
    31
    32/-- Decode the matching table at its declared graph order. Path edges are determined by row numbers. -/
    33def decode (n : ℕ) (tape : List ℕ) : SimpleGraph (Fin n) :=
    34 SimpleGraph.fromRel (fun u v =>
    35 (u.val / degree = v.val / degree ∧ u.val+1 = v.val) ∨
    36 v.val = (tape.tail[u.val]?).getD 0)
    37
    38end Lax920634.WordEncoding
    39
    Formalization notes

    The row number determines the base vertex and port by division and remainder by the fixed degree. This encoding uses machine words for vertex labels, rather than unary coordinates. The requested order is supplied as one word.

    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…