Covers
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove NP-completeness of the decision problem.
- Does not link cover size k to any phi-power mass formula.
- Does not supply an algorithm or approximation guarantee.
- Does not address weighted or parameterized variants.
Lean usage
lemma Covers_nil_edges (S : List Nat) (I : Instance) (h_edges : I.edges = []) : Covers S I := by intro e he; simpa [Covers, h_edges] using heformal statement (Lean)
27def Covers (S : List Nat) (I : Instance) : Prop :=
proof body
Definition body.
28 ∀ e, e ∈ I.edges → EdgeCovered S e
29
30/-- There exists a vertex cover of size ≤ k. -/