Covers_nil_edges
plain-language theorem explainer
Any vertex list covers a Vertex Cover instance whose edge list is empty. Researchers formalizing base cases for complexity reductions in Recognition Science cite this lemma when graphs contain no edges. The proof is a short tactic script that unfolds the Covers definition and uses the empty-edges hypothesis to make the universal quantifier hold vacuously.
Claim. Let $I$ be a Vertex Cover instance with $I.edges = []$. Then for every list $S$ of vertices, the predicate Covers$(S,I)$ holds, where Covers$(S,I)$ asserts that every edge in the (empty) list $I.edges$ is covered by $S$.
background
The module treats complexity pairs as functions of input size. An Instance is a structure with a list of vertices, a list of edges as pairs of natural numbers, and a natural number $k$ that bounds cover size. The Covers predicate on a list $S$ and instance $I$ requires that for every edge $e$ in $I.edges$, the set $S$ contains at least one endpoint of $e$ (via the auxiliary EdgeCovered relation).
proof idea
The proof introduces an arbitrary edge $e$ together with a membership hypothesis $he$ that $e$ lies in the edge list. It then applies simpa with the Covers definition and the hypothesis that the edge list equals the empty list, discharging the goal by vacuous truth.
why it matters
This lemma supplies the trivial base case for coverage when an instance has no edges, supporting inductive or reduction arguments inside the Complexity.VertexCover module. No downstream uses are recorded, so it functions as an early scaffolding step for larger claims about vertex cover in Recognition Science. It parallels the discrete constraint modeling seen in the ILG action $S$ and the forcing-chain constructions elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.