HasCover
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.