ConstraintInstance
ConstraintInstance supplies the data type for RS constraint problems reduced to vertex cover. Researchers establishing polynomial reductions in Recognition Science complexity cite this structure when mapping RS instances to VertexCover.Instance. The definition is a direct structure declaration with three fields and no separate proof.
claimA structure consisting of a list of vertices $V$, a list of constraints $C$ (pairs of natural numbers), and a parameter $k$, representing an RS instance whose acceptance is decided by whether the image under the forgetful map to VertexCover.Instance admits a cover of size $k$.
background
The RSVC module imports VertexCover and defines reductions from Recognition Science constraints to the vertex cover decision problem. ConstraintInstance is the source type whose fields are vertices, constraints (treated as edges), and $k$. The sibling definition toVC performs the forgetful map by copying vertices to vertices, constraints to edges, and $k$ to $k$. The upstream map from RSNative.Core.Measurement preserves window, protocol, uncertainty and notes under any function $f$, providing the general pattern for structure-preserving maps used elsewhere in the module.
proof idea
Structure definition with three fields; no tactics or lemmas are applied. The declaration introduces the type directly, after which toVC and Recognizes are defined by pattern matching on the fields.
why it matters in Recognition Science
ConstraintInstance is the domain type for reduceRS2VC, rs_preserving_RS2VC and the correctness theorem reduce_correct. These feed the claim that RS recognition reduces to vertex cover while preserving instance size up to a linear factor. The construction supports the larger argument that RS problems lie in NP via the known vertex cover reduction, touching the open question of whether the RS recognition predicate is polynomial-time decidable.
scope and limits
- Does not interpret the meaning of constraints beyond treating them as edges.
- Does not define the Recognizes predicate or any decision procedure.
- Does not establish NP-completeness or any time bound.
- Does not reference phi-ladder, J-cost or other RS-native constants.
Lean usage
def sample : ConstraintInstance := { vertices := [1,2], constraints := [(1,2)], k := 1 }formal statement (Lean)
10structure ConstraintInstance where
11 vertices : List Nat
12 constraints : List (Nat × Nat)
13 k : Nat
14
15/-- Forgetful map to a Vertex Cover instance. -/