trivial_hasCover
The lemma establishes that the trivial instance with one vertex and no edges admits a vertex cover of size at most zero. Researchers formalizing NP-completeness reductions or base cases for vertex-cover algorithms would cite it to anchor inductive arguments on graph structure. The proof proceeds by a direct term-mode construction that supplies the empty list, confirms the size bound by decision, and discharges the covering obligation by simplification on the empty edge set.
claimLet $I_0$ be the instance with vertex set $[1]$, edge set empty, and bound $k=0$. Then there exists a list $S$ of vertices such that $|S|≤0$ and every edge of $I_0$ is incident to some vertex in $S$.
background
The module treats complexity pairs as functions of input size. An Instance is a triple consisting of a vertex list, an edge list, and an integer bound $k$. HasCover(I) asserts the existence of a list $S$ of vertices satisfying $|S|≤I.k$ together with the Covers predicate that every edge is incident to $S$. The upstream definition trivialInstance supplies the concrete triple with vertices [1], edges [], and $k=0$, serving as the canonical empty-edge case.
proof idea
The term proof refines the existential quantifier in HasCover with the empty list, applies decide to verify length ≤0, and then uses an intro-simpa sequence to show that the covering condition holds vacuously: any assumed edge leads to an immediate contradiction because the edge list is empty.
why it matters in Recognition Science
This lemma supplies the base case for vertex-cover statements inside the Complexity module. It closes the trivial instance so that larger inductive arguments about Covers and HasCover can proceed without separate handling of the empty-edge graph. No downstream uses are recorded yet, leaving open whether it will anchor reductions or decision procedures elsewhere in the Recognition Science library.
scope and limits
- Does not address instances that contain any edges.
- Does not compute minimum vertex-cover size.
- Does not relate the predicate to approximation ratios or NP-completeness.
- Does not generalize beyond the specific trivialInstance definition.
formal statement (Lean)
37lemma trivial_hasCover : HasCover trivialInstance := by
proof body
Term-mode proof.
38 refine ⟨[], by decide, ?_⟩
39 intro e he
40 simpa using he
41