# Vertex covers and deletion certificates on a star [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-vertex-cover/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-vertex-cover-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Audit covers edgewise and distinguish minimal from minimum. Basic cover obligations, with no automatic Konig theorem. ## Givens and symbols - work - G1 — V={0,1,2,3}, E={01,02,03}; C={1,2,3}, D={0}. - V,E — complete vertex and edge sets - C,D — vertex subsets ## Rules and sources - mko_definition · cited — Declare finite unique vertices and loop-free duplicate-free unordered edges. Audit every edge; one edge with neither endpoint in C refutes coverage. The empty set covers an edgeless graph, isolated vertices are optional and any superset of a cover remains a cover. Inclusion-minimal means every single vertex deletion destroys coverage; minimum means least cardinality among all covers. Do not conflate those notions or substitute edge cover, independent set or directed-cover conventions. Minimum size is not automatically solved by the basic definition. · mko-vertex-cover - work · prerequisite — A finite simple undirected graph has loop-free duplicate-free unordered edges; graph properties are audited on all declared V and E. A vertex cover is C contained in V with at least one endpoint of every edge in C; inclusion-minimal means every selected-vertex deletion fails, while minimum means least cardinality over all covers. ## Main derivation S01 · impliesBefore C=\{1,2,3\}\subseteq V After C\text{ is a unique-vertex candidate subset} Conditions: none Rule: work · Uses: G1, work Leaf basis: work First qualify C as a duplicate-free subset of V. S02 · impliesBefore 01\cap C=\{1\} After 01\text{ covered} Conditions: none Rule: work · Uses: G1, S01, work Leaf basis: work Endpoint1 covers the first edge. S03 · impliesBefore 02\cap C=\{2\} After 02\text{ covered} Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work Endpoint2 covers the second edge. S04 · impliesBefore 03\cap C=\{3\} After 03\text{ covered; }C\text{ is a cover} Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work The third edge is covered too, exhausting E. S05 · impliesBefore C\setminus\{1\},C\setminus\{2\},C\setminus\{3\} After 01,02,03\text{ respectively become uncovered} Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work Each one-vertex deletion has an uncovered-edge witness, so C is inclusion-minimal. S06 · impliesBefore D=\{0\} After 01\cap D=02\cap D=03\cap D=\{0\} Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work The smaller D covers all edges, refuting minimum cardinality of C. S07 · impliesBefore C\subseteq C'\subseteq V,\quad e\cap C\ne\varnothing After e\cap C'\ne\varnothing Conditions: none Rule: work · Uses: G1, S06, work Leaf basis: work Every cover superset retains the original covered endpoint. S08 · impliesBefore E=\varnothing After \varnothing\text{ is a cover} Conditions: none Rule: work · Uses: G1, S07, work Leaf basis: work With no edges the all-edge condition is vacuous; isolated vertices need not be selected. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07, work — This star has edges, so the edgeless boundary does not make its empty set a cover. - S07 · premise_audit · G1, S06, work — A superset may cease to be minimal; keep the properties separate. - S06 · premise_audit · G1, S05, work — C and D need not be nested. - S05 · premise_audit · G1, S04, work — All three deletion cases are listed. - S04 · premise_audit · G1, S03, work — Covering most edges is insufficient; all are covered here. - S03 · premise_audit · G1, S02, work — Every edge has its own coverage obligation. - S02 · premise_audit · G1, S01, work — At least one endpoint is required, not both. - S01 · premise_audit · G1, work — A vertex cover selects vertices, not edges. ## Error controls and negative controls Counterexample edgeFor each failed cover give an edge with both endpoints outside. All deletionsDelete each of C's three elements once, separately from the global smaller witness. - C is minimal, hence minimum. → reject — Valid D has size 1 versus C's3. - {1,2} covers the star. → reject — Neither endpoint of 03 is selected. - A cover must select both endpoints of every edge. → reject — D selects only center0 and covers all three edges. ## Result and limitations C is an inclusion-minimal cover, but D={0} is smaller, so C is not minimum. ## Verification and source binding 2 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 3e1cb818fce0186d9bc40d27d6db5c6f3685c62c296183c10027a8f6e28ed321 - original source SHA-256: bcf513dc1646f8e2bb4552b8f00156931aa83edb1d0ffa53ca9e3fd932a3f728 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-vertex-cover-01.json)