toVC
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.