Vertex covers and deletion certificates on a star

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

C=\{1,2,3\}\subseteq V

C\text{ is a unique-vertex candidate subset}

01\cap C=\{1\}

01\text{ covered}

02\cap C=\{2\}

02\text{ covered}

03\cap C=\{3\}

03\text{ covered; }C\text{ is a cover}

C\setminus\{1\},C\setminus\{2\},C\setminus\{3\}

01,02,03\text{ respectively become uncovered}

D=\{0\}

01\cap D=02\cap D=03\cap D=\{0\}

C\subseteq C'\subseteq V,\quad e\cap C\ne\varnothing

e\cap C'\ne\varnothing

E=\varnothing

\varnothing\text{ is a cover}

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 edge

For each failed cover give an edge with both endpoints outside.

All deletions

Delete 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)