Lax Lean Archive

Selecting and Encoding the Constructed Graphs

Lax920634.GraphEncoding · concepts/Lax920634/GraphEncoding.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

    Given a requested order nn in unary, start at the smallest tower member and advance while its regular-graph order is below 2n2n. At most 2n2n advances suffice. After path replacement this selects a graph of order between nn and a fixed constant times n+1n+1.

    The output lists the paired-port destination of every vertex, in numerical order. A destination is recorded as its base vertex and its port, both in unary. The two possible path neighbors follow directly from the row number. This table determines the entire simple graph, including the removal of loops and duplicate edges.

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

    Lean source view on GitHub

    1import Lax920634.ZigZagConstruction
    2import Mathlib.Data.List.Basic
    3
    4/-!
    5---
    6title: Selecting and Encoding the Constructed Graphs
    7type: definition
    8---
    9Given a requested order nn in unary, start at the smallest tower member and
    10advance while its regular-graph order is below 2n2n. At most 2n2n advances
    11suffice. After path replacement this selects a graph of order between nn
    12and a fixed constant times n+1n+1.
    13
    14The output lists the paired-port destination of every vertex, in numerical
    15order. A destination is recorded as its base vertex and its port, both in
    16unary. The two possible path neighbors follow directly from the row number.
    17This table determines the entire simple graph, including the removal of loops
    18and duplicate edges.
    19
    20# Formalization notes
    21
    22The binary serialization uses balanced brackets: `false` opens a list and
    23`true` closes one. A Boolean is an empty list for `false` and a list containing
    24one empty list for `true`. Records are pairs of unary Boolean words. The
    25whole table is a list of these records. The format is unambiguous; its unary
    26coordinates increase output size only polynomially.
    27-/
    28
    29namespace Lax920634.GraphEncoding
    30
    31open SeedSearch ZigZagConstruction
    32
    33/-- The bounded level-selection loop, carrying the level and current regular order. -/
    34def levelAfter (b n : ℕ) : ℕ → ℕ × ℕ → ℕ × ℕ
    35 | 0, p => p
    36 | j + 1, p =>
    37 let q := levelAfter b n j p
    38 if q.2 < 2 * n then (q.1 + 1, q.2 * b) else q
    39
    40/-- The level selected for a requested order, after at most `2*n` advances. -/
    41def selectedLevel (n : ℕ) : ℕ :=
    42 (levelAfter (seedDegree ^ 4) n (2 * n) (0, seedDegree ^ 4)).1
    43
    44/-- A Boolean serialized as an empty or singleton-empty bracketed list. -/
    45def encodeBit (b : Bool) : List Bool :=
    46 if b then [false, false, true, true] else [false, true]
    47
    48/-- Serialize a Boolean word as a bracketed list of encoded Booleans. -/
    49def encodeWord (w : List Bool) : List Bool := false :: (w.flatMap encodeBit ++ [true])
    50
    51/-- Serialize a pair of natural coordinates, each represented in unary. -/
    52def encodeRecord (p : ℕ × ℕ) : List Bool :=
    53 false :: (encodeWord (List.replicate p.1 true) ++
    54 encodeWord (List.replicate p.2 true) ++ [true])
    55
    56/-- The paired-port destination of each vertex, in canonical row order. -/
    57def records (k : ℕ) : List (ℕ × ℕ) :=
    58 (List.range (order k)).map fun j =>
    59 rotation k (j / degree, j % degree)
    60
    61/-- The binary table encoding of the entire subcubic graph at a specified level. -/
    62def encoding (k : ℕ) : List Bool := false :: ((records k).flatMap encodeRecord ++ [true])
    63
    64/-- The specified deterministic graph construction on a unary size request. -/
    65def construct (input : List Bool) : List Bool := encoding (selectedLevel input.length)
    66
    67end Lax920634.GraphEncoding
    68
    Formalization notes

    The binary serialization uses balanced brackets: falsefalse opens a list and truetrue closes one. A Boolean is an empty list for falsefalse and a list containing one empty list for truetrue. Records are pairs of unary Boolean words. The whole table is a list of these records. The format is unambiguous; its unary coordinates increase output size only polynomially.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…