trivialInstance
plain-language theorem explainer
trivialInstance supplies a minimal vertex cover instance with a single vertex, empty edge list, and parameter zero. Researchers checking base cases for cover predicates in the Complexity domain would cite this construction. The definition is a direct structure literal with no computation or lemmas applied.
Claim. Define the instance $I = (V, E, k)$ where $V = [1]$, $E = []$, and $k = 0$.
background
An Instance is a structure for a vertex cover problem over natural-number vertices, with fields vertices (List Nat), edges (List (Nat × Nat)), and k (Nat). The module places such instances inside complexity pairs treated as functions of input size. The definition depends only on the Instance structure declaration that introduces these three fields.
proof idea
The definition is a direct structure literal that assigns vertices := [1], edges := [], and k := 0. No lemmas or tactics are used.
why it matters
It supplies the input to the lemma trivial_hasCover that proves the empty set covers this instance. In the Recognition framework it supplies the trivial base case inside the Complexity domain for testing cover predicates. It closes the minimal example without engaging the forcing chain, J-uniqueness, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.