星形圖的cover與刪點證書

目標與範圍

逐邊核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中最小基數。

逐步主鏈

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}

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）