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