# All eight subsets for minimum cover on P3

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-minimum-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-minimum-vertex-cover-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Classify every cover and all minimizers.

Bounded exact finite enumeration, with no Konig theorem.





## Givens and symbols


- work


- G1 — V={0,1,2}, E={01,12}.


- V,E — complete vertex and edge sets
- τ(G) — minimum cover cardinality





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — For a fully specified bounded finite simple undirected graph, enumerate every vertex subset and audit every edge to obtain minimum cardinality and all minimizing covers. A nonminimum cover needs an explicit smaller-cover witness. Inclusion-minimal means each single-vertex deletion loses coverage; it does not imply minimum cardinality. Retain edgeless graphs, multiple minimum solutions and minimal-but-nonminimum examples. Do not substitute maximality, edge covers or independent sets, or invoke Konig theorem or weighted/directed variants. · mko-minimum-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 cover intersects every edge in an endpoint; minimum cardinality is least over all valid covers and argmin lists all attaining covers; minimal only forbids deleting a selected vertex.





## Main derivation

S01 · impliesBefore

|V|=3

After

2^3=8\text{ vertex subsets}

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Each vertex is selected or not, giving eight complete candidates.



S02 · impliesBefore

C=\varnothing

After

01\cap C=\varnothing\implies\text{invalid}

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The empty set fails to cover original edge 01.



S03 · impliesBefore

C=\{0\},\quad C=\{2\}

After

12\text{ uncovered},\quad01\text{ uncovered}

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Each endpoint singleton has an explicit uncovered edge.



S04 · impliesBefore

C=\{1\}

After

01\cap C=12\cap C=\{1\}\implies\text{valid, size }1

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

The center singleton covers both edges.



S05 · impliesBefore

C=\{0,1\},\quad C=\{1,2\}

After

\text{both cover }01,12\text{ via vertex }1

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Both two-vertex sets containing the center are covers.



S06 · impliesBefore

C=\{0,2\}

After

01\text{ covered by }0,\quad12\text{ by }2

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The two-point set without the center also covers, and deleting either point fails.



S07 · impliesBefore

C=\{0,1,2\}

After

\text{cover, size }3

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

The final triple covers both edges, completing all eight candidates.



S08 · impliesBefore

\text{valid sizes }1,2,2,2,3

After

\tau(G)=1,\quad\operatorname{Argmin}=\{\{1\}\}

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Take the minimum cardinality over all covers and list all minimizers.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — For an edgeless graph the size-zero minimizer is empty; general graphs may have multiple minima.
- S07 · premise_audit · G1, S06, work — The valid covers are{1},{0,1},{0,2},{1,2},V.
- S06 · premise_audit · G1, S05, work — It is minimal but not minimum because{1} is smaller.
- S05 · premise_audit · G1, S04, work — Deleting their endpoint still leaves a cover, so they are not minimal.
- S04 · premise_audit · G1, S03, work — It gives an upper bound of one while the remaining cases are still classified.
- S03 · premise_audit · G1, S02, work — Both cases are retained.
- S02 · premise_audit · G1, S01, work — The graph has edges, so the edgeless convention does not apply.
- S01 · premise_audit · G1, work — This is not a sample of plausible optimizers.





## Error controls and negative controls

Eight casesCount one empty, three singleton, three pair and one triple case.

Full argminReport not only size 1 but the sole attaining set{1}.


- {0,2} is minimum because every deletion fails. → reject — {1} is a smaller cover.
- {0} is a cover. → reject — Edge 12 is uncovered.
- Minimum covers are always unique. → reject — Either endpoint singleton is minimum on a one-edge graph.





## Result and limitations

Minimum size is 1 with unique minimizer{1};{0,2} is minimal but 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: 0c5dcd41a728ed5ea6c8d3a9073f8c93e7136545d0106b2b4387bb0d79708b0c
- original source SHA-256: 62c1c8fdcda2e9d32b26f78d86b566895ca1e88ad41eac54b7a4454148d6bafb
- 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-minimum-vertex-cover-01.json)