A graph with a parameter appended

Lax271696.VertexCover · concepts/Lax271696/VertexCover.lean · lax-271696

definition

Loading review…

Sign in with ORCID

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 parameterized graph problem is handed to the machine as one word: the compressed sparse row block encoding the graph, followed by the single entry k. This file defines that instance format and nothing else.

    Concept map
    4 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax808846.RamComputes
    2import Lax271696.GraphEncoding
    3import Mathlib.Combinatorics.SimpleGraph.VertexCover
    4
    5/-!
    6---
    7title: A graph with a parameter appended
    8type: definition
    9---
    10A parameterized graph problem is handed to the machine as one word: the
    11compressed sparse row block encoding the graph, followed by the single
    12entry *k*. This file defines that instance format and nothing else.
    13
    14# Formalization notes
    15
    16The instance word is the graph block with one entry appended. The
    17compressed sparse row block is self-delimiting — its own header
    18determines its length — so nothing needs to separate it from the
    19parameter, and the split of the word into the two parts is determined
    20by the word itself, not chosen. The parameter comes last so that the
    21graph block sits at the same offsets as in every other statement built
    22on this encoding.
    23
    24The format is defined here, next to the encoding it extends, and the
    25statements made on it live in the proof packages that import it rather
    26than restate it, so that every bound stated over it is a claim about
    27literally the same inputs. Its first consumer is in this submission's
    28own proof package: the bounded search tree of Downey and Fellows, which
    29decides vertex cover within *c* · 2^*k* · (|x|+1) steps over this
    30format.
    31-/
    32
    33namespace Lax271696.VertexCover
    34
    35open Lax808846.Ram Lax808846.RamComputes Lax271696.GraphEncoding
    36
    37/-- The word `x` presents the graph `G` on `n` vertices together with
    38the parameter `k`: a compressed sparse row block encoding `G`, followed
    39by the single entry `k`. -/
    40def EncodesParamInstance (x : List ℕ) (n : ℕ) (G : SimpleGraph (Fin n)) (k : ℕ) : Prop :=
    41 ∃ g, x = g ++ [k] ∧ EncodesGraph g n G
    42
    43end Lax271696.VertexCover
    44
    Formalization notes

    The instance word is the graph block with one entry appended. The compressed sparse row block is self-delimiting — its own header determines its length — so nothing needs to separate it from the parameter, and the split of the word into the two parts is determined by the word itself, not chosen. The parameter comes last so that the graph block sits at the same offsets as in every other statement built on this encoding.

    The format is defined here, next to the encoding it extends, and the statements made on it live in the proof packages that import it rather than restate it, so that every bound stated over it is a claim about literally the same inputs. Its first consumer is in this submission's own proof package: the bounded search tree of Downey and Fellows, which decides vertex cover within c · 2^k · (|x|+1) steps over this format.

    Discussion

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

    Loading discussion…