HasCover
The definition asserts that a Vertex Cover instance admits a cover set of size at most its bound k. Researchers mapping Recognition Science constraints to the vertex cover decision problem cite this predicate when establishing reductions. It is introduced directly as an existential quantification over covering lists.
claimLet $I$ be a vertex cover instance with vertex list $V$, edge list $E$, and bound $k$. Then there exists a list $S$ of natural numbers such that $|S| ≤ k$ and every edge in $E$ has at least one endpoint in $S$.
background
The module treats complexity pairs as functions of input size. An Instance records a list of vertices, a list of edges as pairs of natural numbers, and a bound k. The sibling predicate Covers requires that for every edge in the instance, at least one endpoint belongs to the candidate set S.
proof idea
As a definition, HasCover is introduced directly by the existential statement over a list S of length at most k that satisfies Covers. No lemmas or tactics are invoked; the body is the literal quantifier.
why it matters in Recognition Science
HasCover supplies the target predicate for Recognizes in the RSVC reduction, where an RS constraint instance is accepted precisely when its vertex-cover image satisfies HasCover. It anchors the combinatorial core of the vertex-cover decision problem inside the Recognition Science complexity layer and enables the immediate correctness result reduce_correct.
scope and limits
- Does not compute a minimum-size cover for any concrete instance.
- Does not establish NP-completeness or hardness results.
- Does not restrict vertex labels beyond natural numbers.
- Does not address approximation ratios or parameterized complexity.
Lean usage
def recognizes (A : ConstraintInstance) : Prop := HasCover (toVC A)formal statement (Lean)
31def HasCover (I : Instance) : Prop :=
proof body
Definition body.
32 ∃ S : List Nat, S.length ≤ I.k ∧ Covers S I
33
34/-- A trivial example with no edges is always covered by the empty set. -/