# 含孤立點的二分證書

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

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

derivation-mko-bipartite-graph-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

核兩部的全部責任，區分失敗partition與非二分。

有限無向簡單圖；允許空部但仍需cover。





## 已知條件與符號


- work


- G1 — V={0,1,2,3}，E={{0,1},{1,2}}；候選A={0,2,3}，B={1}。


- V,E — 完整頂點與邊集合
- A,B — 兩個部





## 規則與來源


- mko_definition · cited — 核完整頂點cover、兩部互斥及全部邊跨部。失敗partition不證非二分；奇cycle可作否證。孤立頂點可置任一部，空部是否允許須明示。 · mko-bipartite-graph
- work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 二分證書是互斥且聯集為V的兩部，每邊跨部。





## 逐步主鏈

S01 · implies操作前

V,E

操作後

E\subseteq\{\{u,v\}:u,v\in V,\ u\ne v\}

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

兩邊皆有合法不同端點，3為孤立點。



S02 · implies操作前

A=\{0,2,3\},\quad B=\{1\}

操作後

A\cap B=\varnothing

條件：無

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

葉節點依據：work

四個頂點沒有跨部重複。



S03 · implies操作前

A\cup B=\{0,1,2,3\}

操作後

A\cup B=V

條件：無

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

葉節點依據：work

孤立點3也被納入，完整cover。



S04 · implies操作前

\{0,1\}\in E

操作後

0\in A,\quad1\in B

條件：無

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

葉節點依據：work

第一邊兩端跨部。



S05 · implies操作前

\{1,2\}\in E

操作後

1\in B,\quad2\in A

條件：無

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

葉節點依據：work

第二邊跨部，全部邊已窮盡。



S06 · implies操作前

A'=\{0,1\},\quad B'=\{2,3\}

操作後

\{0,1\}\subseteq A'\implies(A',B')\text{ invalid}

條件：無

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

葉節點依據：work

另一候選失敗但原圖仍有上面合法證書。



S07 · implies操作前

H:0-1-2-0\quad\text{(separate triangle)}

操作後

c(0)\ne c(1)\ne c(2)\implies c(2)=c(0),\ c(2)\ne c(0)

條件：無

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

葉節點依據：work

若三角形只有兩部，沿前兩邊迫使0、2同部，末邊矛盾。



S08 · implies操作前

A\cap B=\varnothing,\quad A\cup B=V,\quad\text{all edges cross}

操作後

G\text{ is bipartite}

條件：無

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

葉節點依據：mko_definition

合併全部資格完成原圖二分證書。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, mko_definition — 無邊圖可用(V,empty)但不能漏頂點。
- S07 · premise_audit · G1, S06, work — 這個奇圈反證針對另一完整圖，不混入原圖。
- S06 · premise_audit · G1, S05, work — 無效候選不能否定存在某個有效候選。
- S05 · premise_audit · G1, S04, work — 0與2可同部因它們不相鄰。
- S04 · premise_audit · G1, S03, work — 只核頂點數不會證此邊責任。
- S03 · premise_audit · G1, S02, work — 漏孤立點也會使partition失敗。
- S02 · premise_audit · G1, S01, work — 同一頂點不得同屬兩部。
- S01 · premise_audit · G1, work — 圖只有這兩邊，沒有暗藏0至2的邊。





## 錯誤控制與反例

全頂點孤立3仍必分配到一部。

存在量詞合法證書證存在；失敗一案不證不存在。


- 可漏掉孤立3。 → reject — 兩部聯集就不等V。
- A'失敗故圖非二分。 → reject — A、B已是合法partition。
- 三角形也可兩部。 → reject — 沿三邊交替會迫使首尾同部又相鄰。





## 結論與限制

A={0,2,3}、B={1}證原圖二分。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bd3b9a767549e7cefb60cebc2278fb332f5bac033b84321bd0c2eb7004197c3c
- original source SHA-256: b94470821c9e899e02832a1b63f4ceaf9869bac586a0967c66175e03ad73bf37
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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