reduceRS2VC
plain-language theorem explainer
The map reduceRS2VC sends an RS constraint instance to its corresponding vertex cover instance by equating constraints with edges. Researchers working on reductions in the Recognition Science complexity layer cite this when chaining RS problems to classical NP-complete problems. It is realized as a one-line definition that delegates entirely to the forgetful map toVC.
Claim. For an RS constraint instance $A = (V, C, k)$, the reduction yields the vertex cover instance with the same vertex list $V$, edge list $C$, and parameter $k$.
background
An RS constraint instance is the structure holding a list of vertices, a list of pairwise constraints, and an integer $k$. The forgetful map toVC converts this structure into a Vertex Cover instance by setting edges equal to the constraint list. The module treats RS constraint instances as objects whose satisfiability reduces to the existence of a vertex cover of size $k$. Upstream, VertexCover.Instance is the plain record with vertices, edges, and $k$ over natural numbers.
proof idea
The definition is a one-line wrapper that applies the forgetful map toVC to the input ConstraintInstance.
why it matters
This reduction supplies the map used by reduce_correct, which states that an RS instance is recognized exactly when its image under the map admits a vertex cover. It is also the reduce field inside the RS-preserving wrapper rs_preserving_RS2VC that records size functions for both sides. The construction therefore closes the reduction step that links RS recognition to the classical vertex cover problem while preserving the polynomial size measures required by the surrounding complexity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.