reduceRS2VC
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that the reduction runs in polynomial time.
- Does not define the Recognizes predicate on RS instances.
- Does not address approximation ratios or parameterized complexity.
formal statement (Lean)
24@[simp] def reduceRS2VC : ConstraintInstance → VertexCover.Instance := toVC
proof body
Definition body.
25
26/-- Correctness is immediate from the definition. -/