含孤立點的二分證書

目標與範圍

核兩部的全部責任，區分失敗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的兩部，每邊跨部。

逐步主鏈

V,E

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

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

A\cap B=\varnothing

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

A\cup B=V

\{0,1\}\in E

0\in A,\quad1\in B

\{1,2\}\in E

1\in B,\quad2\in A

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

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

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)

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

G\text{ is bipartite}

局部子步與引理

本稿無局部子步。

逐步反向審查

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