EdgeCovered_comm
plain-language theorem explainer
EdgeCovered_comm asserts symmetry of edge coverage under endpoint swap for any list S of natural numbers. Complexity researchers modeling vertex cover instances as undirected graphs in the Recognition framework would cite it to ensure consistent treatment of pairs. The proof is a one-line wrapper that applies simplification with the EdgeCovered definition and disjunction commutativity.
Claim. For a list $S$ of natural numbers and natural numbers $u,v$, the predicate that $S$ covers the pair $(u,v)$ holds if and only if $S$ covers the pair $(v,u)$, where coverage of a pair means at least one endpoint lies in $S$.
background
The Complexity.VertexCover module addresses complexity pairs as functions of input size. EdgeCovered is defined so that a list $S$ covers an edge pair when InCover holds for the first or second component. This lemma appears among sibling results on Covers, HasCover, and trivial instances. It depends directly on the EdgeCovered definition and on the ILG action functional S, though the latter supplies only module context.
proof idea
This is a one-line wrapper proof that invokes simp with the EdgeCovered unfolding and Or.comm.
why it matters
The lemma supplies a basic symmetry property for undirected edges in vertex cover modeling inside the Recognition framework. It supports consistent handling of graph instances that may later connect to larger complexity results, though no downstream uses are recorded. It closes a minor gap in the complexity scaffolding without touching the core forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.