pith. machine review for the scientific record. sign in
lemma proved term proof high

hasCover_of_nil_edges

show as:
view Lean formalization →

If a vertex cover instance has an empty edge list then the empty vertex set satisfies the cover predicate and the size bound. Researchers formalizing NP-completeness reductions or exact solvers for vertex cover cite this vacuous base case. The proof is a direct term-mode construction that supplies the empty list and discharges the covering condition by simplification on the empty edge set.

claimLet $I$ be a vertex cover instance consisting of a vertex list, an edge list, and bound $k$. If the edge list of $I$ is empty, then there exists a list $S$ of vertices such that the length of $S$ is at most $k$ and every edge of $I$ is incident to a vertex in $S$.

background

The module introduces a vertex cover instance as a structure containing a list of natural-number vertices, a list of edges as pairs of naturals, and a natural-number bound $k$. The predicate Covers $S$ $I$ asserts that every edge in the instance is incident to at least one vertex in $S$. HasCover $I$ is the existential statement that some list $S$ satisfies both the length bound and the Covers predicate.

proof idea

The proof is a term-mode wrapper that refines the witness to the empty list, applies simplification to confirm the length bound, and then uses a contradiction on the empty edge list to discharge the universal quantifier in Covers.

why it matters in Recognition Science

The lemma supplies the trivial empty-edge case that closes the definition of HasCover. It supports downstream reasoning about vertex cover within the complexity module, though no direct parent theorems are recorded. The result aligns with the framework's pattern of establishing exact base cases before scaling to larger input sizes.

scope and limits

formal statement (Lean)

  56lemma hasCover_of_nil_edges (I : Instance) (h_edges : I.edges = []) : HasCover I := by

proof body

Term-mode proof.

  57  refine ⟨[], by simp, ?_⟩
  58  intro e he
  59  simpa [Covers, h_edges] using he
  60
  61end VertexCover
  62
  63end Complexity
  64
  65end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.