Recognizes
plain-language theorem explainer
The recognition predicate accepts an RS constraint instance exactly when the vertex-cover instance obtained by mapping constraints to edges admits a cover of size at most k. Researchers working on reductions between recognition problems inside Recognition Science would cite this definition to establish equivalence with classical vertex cover. It is realized by direct composition of the forgetful map toVC with the HasCover predicate.
Claim. Let $A$ be a constraint instance consisting of a vertex list $V$, a list of pairwise constraints $E$, and an integer bound $k$. The instance is recognized precisely when the vertex-cover instance on edges $E$ admits a subset $S$ of vertices with $|S|leq k$ that intersects every constraint in $E$.
background
ConstraintInstance is the structure carrying a list of vertices, a list of pairwise constraints, and the integer $k$. The auxiliary definition toVC forgets the RS origin and produces a standard VertexCover.Instance by equating constraints with edges. HasCover asserts the existence of a vertex subset $S$ whose cardinality is at most $k$ and that intersects every edge. The module develops the reduction of RS constraint satisfaction to the vertex-cover decision problem. Upstream results include the identity map in ObserverForcing and the active edge count from IntegrationGap, which supply the dimensional and forcing context in which the constraints arise.
proof idea
This definition is a one-line wrapper that applies the forgetful map toVC to the input ConstraintInstance and then invokes the HasCover predicate on the resulting VertexCover.Instance.
why it matters
This definition supplies the acceptance condition for the RS-to-VC reduction and is invoked directly by the correctness theorem reduce_correct. It closes the mapping step in the complexity analysis of Recognition Science constraints, linking the J-cost structures of the foundation to a classical decision problem. The construction sits inside the broader effort to embed RS recognition inside polynomial-time verifiable decision problems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.