Instance
A vertex cover instance is encoded as a triple of a vertex list, an edge list, and an integer bound k. Researchers mapping Recognition Science constraints to NP-complete graph problems cite this structure as the target of the reduction. The declaration is a plain data definition with Repr derivation and no proof obligations.
claimAn instance consists of a list $V$ of natural-number vertices, a list $E$ of pairs representing edges, and a natural number $k$, such that the decision problem asks whether there exists a subset of at most $k$ vertices incident to every edge in $E$.
background
The module treats complexity via pairs of size functions on input instances. Vertex cover is encoded directly over natural numbers with lists for vertices and edges. Upstream results supply auxiliary notions such as the containment predicate on intervals and the active-edge count $A=1$ per fundamental tick from IntegrationGap and Masses modules, which set the scale for tick-based counting in the broader framework.
proof idea
The declaration is a structure definition that introduces three fields and derives Repr. No lemmas or tactics are invoked; field accessors are generated automatically by the structure declaration.
why it matters in Recognition Science
This structure is the codomain of the forgetful map toVC from ConstraintInstance and is used inside rs_preserving_RS2VC to bundle size functions with the reduction. It supplies the concrete target problem for showing that RS constraint instances reduce to vertex cover, thereby placing the recognition problem inside the complexity hierarchy. The parent reduction appears in the RSVC module and inherits the module-level convention that complexity is measured by pairs of size functions.
scope and limits
- Does not require vertices to be distinct or edges to reference only listed vertices.
- Does not embed any notion of a cover or solution inside the instance.
- Does not impose bounds on list lengths or edge multiplicity.
Lean usage
def ex : Instance := { vertices := [0,1,2], edges := [(0,1),(1,2)], k := 2 }formal statement (Lean)
14structure Instance where
15 vertices : List Nat
16 edges : List (Nat × Nat)
17 k : Nat
18 deriving Repr
19
20/-- A set `S` covers an edge `(u,v)` if it contains `u` or `v`. -/