# 星形圖的cover與刪點證書

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-vertex-cover/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-vertex-cover-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

逐邊核cover並區分minimal與minimum。

basic cover責任，不自動使用König theorem。





## 已知條件與符號


- work


- G1 — V={0,1,2,3}，E={01,02,03}；C={1,2,3}，D={0}。


- V,E — 完整頂點與邊集合
- C,D — 頂點子集合





## 規則與來源


- mko_definition · cited — graph須明示有限unique vertices與loop-free、duplicate-free unordered edges。cover audit遍歷全部edges；一條兩端皆不在C的edge即為反例。empty-edge graph的empty set是cover；isolated vertices不必加入；任何cover的superset仍為cover。inclusion-minimal表示刪任何一點都不再cover，minimum表示全體covers中cardinality最小，兩者不可混同。本節點不混用edge cover、independent set或directed cover，也不自動求minimum size。 · mko-vertex-cover
- work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 vertex cover為C⊆V且每條邊至少一端在C；inclusion-minimal表示刪任一選點會失效，minimum表示全部covers中最小基數。





## 逐步主鏈

S01 · implies操作前

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

操作後

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

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

先核候選確為V子集且無重複。



S02 · implies操作前

01\cap C=\{1\}

操作後

01\text{ covered}

條件：無

規則：work · 依賴：G1, S01, work

葉節點依據：work

第一邊由端點1覆蓋。



S03 · implies操作前

02\cap C=\{2\}

操作後

02\text{ covered}

條件：無

規則：work · 依賴：G1, S02, work

葉節點依據：work

第二邊由端點2覆蓋。



S04 · implies操作前

03\cap C=\{3\}

操作後

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

條件：無

規則：work · 依賴：G1, S03, work

葉節點依據：work

第三邊也覆蓋，已完成全部E。



S05 · implies操作前

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

操作後

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

條件：無

規則：work · 依賴：G1, S04, work

葉節點依據：work

每個單點刪除都有對應uncovered edge，故C inclusion-minimal。



S06 · implies操作前

D=\{0\}

操作後

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

條件：無

規則：work · 依賴：G1, S05, work

葉節點依據：work

較小D也覆蓋全部邊，否定C為minimum。



S07 · implies操作前

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

操作後

e\cap C'\ne\varnothing

條件：無

規則：work · 依賴：G1, S06, work

葉節點依據：work

任一cover超集仍保有原覆蓋端點。



S08 · implies操作前

E=\varnothing

操作後

\varnothing\text{ is a cover}

條件：無

規則：work · 依賴：G1, S07, work

葉節點依據：work

沒有邊時all-edge條件空真；isolated vertices無須加入。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, work — 本star有邊，不能套空圖結論稱空集cover。
- S07 · premise_audit · G1, S06, work — 超集可能不minimal，兩性質分開。
- S06 · premise_audit · G1, S05, work — C與D不需互為子集。
- S05 · premise_audit · G1, S04, work — 三個刪除案例全列，不只試一點。
- S04 · premise_audit · G1, S03, work — 大多數邊覆蓋不夠，這裡是全部。
- S03 · premise_audit · G1, S02, work — 各edge有自己的覆蓋義務。
- S02 · premise_audit · G1, S01, work — 只需至少一端，不需兩端。
- S01 · premise_audit · G1, work — cover選頂點不是選邊。





## 錯誤控制與反例

反例edge每失敗cover提供一條兩端皆不在集合的邊。

刪點全列C三個元素各刪一次，與全域更小witness分開。


- C minimal故minimum。 → reject — D大小1小於C大小3且合法。
- {1,2}覆蓋此star。 → reject — 03兩端皆不被選。
- cover每邊須兩端都選。 → reject — D只選中心0即覆蓋三邊。





## 結論與限制

C是inclusion-minimal cover，但D={0}更小，故C非minimum。







## 驗證及來源綁定

2 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 3e1cb818fce0186d9bc40d27d6db5c6f3685c62c296183c10027a8f6e28ed321
- original source SHA-256: bcf513dc1646f8e2bb4552b8f00156931aa83edb1d0ffa53ca9e3fd932a3f728
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-vertex-cover-01.json)