InCover_cons
This lemma asserts that any vertex x belongs to the covering set formed by prepending x to an arbitrary list xs. It supplies a basic membership fact for inductive constructions in vertex cover arguments within complexity analysis. The proof is a one-line simplification that directly invokes the membership definition of InCover.
claimFor any natural number $x$ and list $xs$ of natural numbers, $x$ belongs to the list $x :: xs$, i.e., the set $x :: xs$ covers the vertex $x$.
background
The Complexity.VertexCover module treats complexity pairs as functions of input size. Its central predicate InCover is defined by membership: a list S covers vertex v precisely when v lies in S. This supplies the elementary fact needed to build covering sets inductively by list cons.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of InCover, reducing the membership claim for the cons constructor to a trivial list fact.
why it matters in Recognition Science
The lemma supplies a foundational membership step inside the vertex-cover development of the Recognition Science complexity module. It supports later arguments that construct explicit covers and aligns with the need for precise set-membership facts when deriving discrete structures from the T0-T8 forcing chain.
scope and limits
- Does not prove coverage of any edges, only vertex membership.
- Does not apply to the empty list or other list constructors.
- Restricted to natural-number vertices and finite lists.
formal statement (Lean)
42@[simp] lemma InCover_cons {x : Nat} {xs : List Nat} : InCover (x :: xs) x := by
proof body
One-line wrapper that applies simp.
43 simp [InCover]
44