Covers_nil_edges
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of a cover for any instance with a nonempty edge list.
- Does not relate the size of $S$ to the bound $k$.
- Does not address decidability or algorithmic complexity of the Covers predicate.
- Does not invoke or depend on the ILG action $S$ beyond module imports.
formal statement (Lean)
52lemma Covers_nil_edges (S : List Nat) (I : Instance) (h_edges : I.edges = []) : Covers S I := by
proof body
Term-mode proof.
53 intro e he
54 simpa [Covers, h_edges] using he
55