rs_preserving_RS2VC
plain-language theorem explainer
Researchers working on complexity reductions inside Recognition Science cite rs_preserving_RS2VC when they need an explicit witness that ConstraintInstance reduces to VertexCover.Instance while preserving polynomial size envelopes. The definition supplies concrete size functions that count vertices plus constraints on the source and vertices plus edges on the target, together with the forgetful map reduceRS2VC. Its construction is a direct record literal that populates the RSPreserving structure without invoking any lemmas.
Claim. The RS-preserving reduction from an RS constraint instance to a vertex cover instance is the structure whose source size map sends an instance to the sum of the lengths of its vertex list and constraint list, whose target size map sends an instance to the sum of the lengths of its vertex list and edge list, and whose reduction function is the forgetful map to a vertex cover instance.
background
ConstraintInstance packages a list of vertices, a list of pairwise constraints, and an integer k. VertexCover.Instance is the parallel structure whose second list holds edges rather than constraints. RSPreserving is the scaffold that bundles two size functions from each problem type to natural numbers, a reduction map between the types, and default polynomial bounds on time and space complexity.
proof idea
This is a definition that directly constructs the RSPreserving record by supplying explicit lambda expressions for the two size functions and setting the reduce field to reduceRS2VC. No lemmas are applied; the construction is immediate from the structure definition of RSPreserving.
why it matters
This definition supplies the concrete witness used by the lemma rs_pres_holds to establish that an RS-preserving reduction exists between the two problem classes. It fills the role of exhibiting a polynomial reduction inside the Recognition Science complexity analysis, consistent with the framework's emphasis on relating different constraint problems via monotone size envelopes. The parent result rs_pres_holds packages this witness into the rs_pres_prop proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.