Instance
plain-language theorem explainer
The Instance structure encodes a vertex cover problem over natural-number vertices together with a target cover size k. Researchers studying reductions from Recognition Science constraint instances to NP-complete problems cite this definition as the codomain of toVC. It is introduced by a direct structure declaration with Repr derivation and no proof body.
Claim. A vertex cover instance consists of a list of vertices $V$, a list of edges $E$ as pairs of naturals, and a natural number $k$, such that one seeks a subset of size at most $k$ covering every edge in $E$.
background
The module defines complexity pairs as functions of input size. Instance supplies the concrete record type for the vertex cover side of such pairs. The local setting treats vertex cover as the image of an RS constraint instance under the forgetful map that identifies constraints with edges. Upstream results supply auxiliary membership predicates (contains from StakeGraph and Interval) and the active-edge constant A used in related size calculations.
proof idea
Direct structure definition; no tactics or lemmas applied.
why it matters
Instance is the target type of reduceRS2VC and the codomain of toVC, which together establish the RS-preserving reduction to vertex cover. It therefore supports rs_pres_prop and the downstream claims that RS recognition reduces to an NP-complete problem. The definition closes the structural half of the reduction without invoking the J-cost, phi-ladder, or T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.