Covers
Covers asserts that a list S of naturals meets every edge of an Instance I by containing at least one endpoint of each edge. Researchers formalizing bounded-search problems inside Recognition Science cite the predicate when they construct HasCover or prove trivial cases such as the empty-edge instance. The definition is a direct universal quantification that delegates the per-edge test to the auxiliary EdgeCovered predicate.
claimLet $S$ be a list of natural numbers and let $I$ be an instance consisting of a vertex list, an edge list of pairs, and a 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$ belongs to $S$.
background
The module treats complexity pairs as functions of input size and encodes the vertex-cover decision problem over natural-number vertices. An Instance is the structure that packages a vertex list, an edge list of pairs, and the integer bound $k$. EdgeCovered holds for a list $S$ and an edge $e$ precisely when $S$ contains the first or second component of $e$. Upstream imports supply ledger-factorization and phi-forcing structures that calibrate the J-cost function used throughout the Recognition Science development.
proof idea
The declaration is a direct definition whose body is the universal quantifier over the edge list of $I$. It applies the sibling predicate EdgeCovered to each edge in turn. No lemmas or tactics are required; the body is the predicate itself.
why it matters in Recognition Science
Covers supplies the core relation that defines HasCover, the existence statement asserting a cover of length at most the instance bound $k$. It therefore anchors the formalization of the vertex-cover problem inside the library. The surrounding module draws on nucleosynthesis tiers and spectral-emergence structures, linking complexity bounds to the phi-ladder and the eight-tick octave of the forcing chain.
scope and limits
- Does not decide whether any given instance admits a cover of size at most $k$.
- Does not encode NP-completeness reductions from other problems.
- Does not impose ordering or uniqueness requirements on the list $S$.
- Does not relate cover size to physical constants such as the fine-structure constant.
formal 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. -/