reduce_correct
plain-language theorem explainer
The equivalence establishes that an RS constraint instance is recognized exactly when the vertex-cover instance produced by the forgetful map admits a cover of size at most k. Researchers examining reductions between recognition problems in the Recognition Science setting would cite this result to validate the mapping. The proof is a one-line reflexivity that follows from the definitional identity between the two sides.
Claim. Let $A$ be a constraint instance with vertex list, constraint pairs, and integer bound $k$. Then $A$ is recognized if and only if the vertex-cover instance obtained from $A$ via the forgetful map has a subset $S$ of vertices with $|S| ≤ k$ that covers every constraint pair.
background
The module formalizes an RS constraint instance as a structure holding a list of vertices, a list of constraint pairs, and an integer $k$. The Recognizes predicate accepts the instance precisely when its image under the forgetful map to a vertex-cover instance satisfies the cover condition. The reduction reduceRS2VC is defined identically to this forgetful map toVC, so the two predicates coincide by construction. The local setting treats RS constraints as edges that must be covered. Upstream, HasCover asserts the existence of a list $S$ whose length is at most the instance bound and that covers the instance.
proof idea
The proof applies Iff.rfl directly to the stated equivalence. This is a one-line wrapper that exploits the definitional equality: Recognizes A unfolds to HasCover (toVC A) while reduceRS2VC A is toVC A, so the two sides are identical.
why it matters
The theorem certifies the correctness of the reduction from RS constraints to vertex cover, supplying a basic building block for complexity claims inside the Recognition Science framework. It anchors the polynomial mapping step that links recognition predicates to the vertex-cover decision problem. No downstream theorems are recorded yet, leaving open how this equivalence will be invoked in larger arguments about the forcing chain or self-reference structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.