rs_pres_holds
plain-language theorem explainer
The lemma establishes existence of an RS-preserving reduction from constraint instances to vertex cover instances by supplying explicit size maps and a reduction function. Researchers embedding NP problems into the Recognition Science framework would cite it to anchor the complexity side of the RSVC construction. The proof is a direct term that packages the size-and-reduce wrapper as a witness for the nonempty proposition.
Claim. There exists a nonempty RS-preserving structure from RS constraint instances to vertex cover instances, where the size of an instance $A$ equals the number of its vertices plus constraints, the size of an instance $B$ equals the number of its vertices plus edges, and the reduction map is the explicit function that sends constraint instances to the corresponding edge-cover instances.
background
The RSVC module treats an RS constraint instance as a collection of vertices and constraints that is mapped onto a graph whose edges must be covered. An RS-preserving structure consists of two size functions (one per domain) together with a reduction map that carries instances forward while preserving the relevant recognition measure. The upstream definition rs_preserving_RS2VC supplies concrete sizeA, sizeB and the reduce map; the companion definition rs_pres_prop packages the claim that at least one such structure exists as a Prop.
proof idea
The proof is a one-line term-mode wrapper that directly supplies the rs_preserving_RS2VC definition as the inhabitant of the Nonempty type required by rs_pres_prop.
why it matters
The result closes the existence claim for an RS-preserving reduction inside the complexity module, thereby supplying a concrete bridge between constraint instances and vertex cover. It supports the larger program of transporting recognition-theoretic properties across polynomial reductions. No downstream theorems are recorded yet; the lemma therefore functions as a foundational interface rather than a derived step in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.