Covers
plain-language theorem explainer
A definition asserting that list S covers instance I exactly when every edge of I has at least one endpoint in S. Researchers formalizing NP decision problems inside Recognition Science structures cite it when mapping vertex cover onto the phi-ladder. The definition is introduced directly as a universal quantifier over I.edges using the sibling EdgeCovered predicate.
Claim. Let $S$ be a list of natural numbers and let $I$ be a vertex-cover instance with vertex list, edge list, and bound $k$. Then $S$ covers $I$ if and only if, for every edge $e$ in the edge list of $I$, at least one endpoint of $e$ lies in $S$.
background
The module encodes the vertex-cover decision problem over natural-number vertices. Instance is the structure with fields vertices : List Nat, edges : List (Nat × Nat), and k : Nat. EdgeCovered S e holds precisely when InCover S (fst e) or InCover S (snd e). The module doc describes the setting as complexity pairs (functions of input size). Upstream imports supply the J-cost algebra from LedgerFactorization and the tiered emergence from SpectralEmergence, placing the predicate inside the same forcing chain that yields D = 3 and the alpha band.
proof idea
The declaration is a pure definition: Covers S I expands directly to the statement ∀ e, e ∈ I.edges → EdgeCovered S e. It invokes the sibling EdgeCovered definition and the membership predicate on the edge list. No tactics or lemmas are applied; the body is the definitional abbreviation itself.
why it matters
Covers supplies the core relation for HasCover, which asserts existence of an S with length ≤ I.k. It is invoked by the base-case lemmas Covers_nil_edges and hasCover_of_nil_edges. Within Recognition Science the predicate supplies the interface that lets vertex-cover instances sit on the phi-ladder, though the explicit reduction to T5 J-uniqueness and the eight-tick octave remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.