toVC
toVC supplies the canonical embedding of an RS constraint instance into a vertex cover instance by treating the constraint list as the edge list. Complexity researchers working on reductions inside the Recognition Science framework cite this map when linking RS recognition to the vertex cover decision problem. The implementation is a direct one-line record construction that copies vertices and k while renaming constraints to edges.
claimThe map sending a constraint instance $A$ (with vertices, constraints as pairs of naturals, and parameter $k$) to the vertex cover instance having the same vertices, the same $k$, and edges exactly equal to the constraints of $A$.
background
ConstraintInstance is the structure with fields vertices : List Nat, constraints : List (Nat × Nat), and k : Nat, representing an RS constraint instance whose constraints are to be covered. VertexCover.Instance is the parallel structure whose edges field receives those constraints. The module sets the local context as the reduction of RS constraint satisfaction to vertex cover for recognition purposes.
proof idea
The definition is a direct record construction that sets vertices := A.vertices, edges := A.constraints, k := A.k. It is a one-line wrapper performing the field renaming from constraints to edges with no additional lemmas or tactics required.
why it matters in Recognition Science
toVC is the core reduction step feeding Recognizes, which accepts an instance precisely when its image under toVC admits a vertex cover, and reduceRS2VC, which is defined directly as toVC. It implements the RS-to-Vertex-Cover reduction inside the complexity layer of the Recognition Science framework, supporting the polynomial-time and recognition claims developed in the surrounding module.
scope and limits
- Does not prove NP-completeness or hardness of the RS constraint problem.
- Does not supply a solver or approximation algorithm for either instance type.
- Does not incorporate RS constants such as phi or the eight-tick octave.
- Does not extend to infinite vertex sets or weighted variants.
Lean usage
def exampleUse (A : ConstraintInstance) : VertexCover.Instance := toVC Aformal statement (Lean)
16@[simp] def toVC (A : ConstraintInstance) : VertexCover.Instance :=
proof body
Definition body.
17{ vertices := A.vertices, edges := A.constraints, k := A.k }
18
19/-- RS recognizer: instance is accepted iff its Vertex Cover image has a cover. -/