# 三邊圖的全部八個matching候選 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-maximum-matching/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-maximum-matching-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 完整2³枚舉求最大matching與全部witness。 exact小圖枚舉，非一般高效演算法。 ## 已知條件與符號 - work - G1 — V={0,1,2,3}，E由e0={0,1}、e1={1,2}、e2={2,3}構成；bit mask順序為(e0,e1,e2)。 - V,E — 完整頂點與邊集合 - ν(G) — 最大matching基數 ## 規則與來源 本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。 - mko_definition · cited — 本輪對小型完整有限簡單圖exhaustively枚舉全部edge subsets並篩matching，給exact maximum size與witnesses。每個候選先驗matching；maximal不等於maximum，多個maximum可共存。 · mko-maximum-matching - work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 matching選邊端點互斥；maximum是在全部合法matching中基數最大，全部達此值的集合構成argmax。 ## 逐步主鏈 S01 · implies操作前 |E|=3 操作後 |\mathcal P(E)|=2^3=8 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 每邊選或不選，恰八個候選。 S02 · implies操作前 000 操作後 \varnothing\text{ valid, size }0 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 空集合合法matching，基數零。 S03 · implies操作前 100,010,001 操作後 \{e_0\},\{e_1\},\{e_2\}\text{ valid, size }1 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 三個singleton均合法，已核原圖邊存在。 S04 · implies操作前 110 操作後 e_0\cap e_1=\{1\}\implies\text{invalid} 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 第一個二邊候選端點衝突。 S05 · implies操作前 101 操作後 e_0\cap e_2=\varnothing\implies\text{valid, size }2 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 唯一合法二邊候選給大小二下界。 S06 · implies操作前 011 操作後 e_1\cap e_2=\{2\}\implies\text{invalid} 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 最後一個二邊候選也有衝突。 S07 · implies操作前 111 操作後 \{e_0,e_1,e_2\}\text{ invalid since }e_0\cap e_1\ne\varnothing 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 三邊候選包含已知衝突對，因此不合法。 S08 · implies操作前 \text{valid sizes }0,1,1,1,2 操作後 \nu(G)=2,\quad\operatorname{Argmax}=\{\{e_0,e_2\}\} 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 對全部合法候選取最大，並列出此圖全部maximizers。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07, work — 唯一性只由這個完整枚舉得出，不當作一般maximum性質。 - S07 · premise_audit · G1, S06, work — 分類數1+3+3+1=8與總候選數一致。 - S06 · premise_audit · G1, S05, work — 三個二邊子集合全部分類。 - S05 · premise_audit · G1, S04, work — 其兩邊都屬原圖。 - S04 · premise_audit · G1, S03, work — 無效候選不得參與最大值比較。 - S03 · premise_audit · G1, S02, work — 共有三個而非任選一個作代表。 - S02 · premise_audit · G1, S01, work — 不可漏掉empty case。 - S01 · premise_audit · G1, work — mask皆為不同子集合，不是抽樣。 ## 錯誤控制與反例 mask覆蓋保留000到111全部八案。 先資格只在valid matching上取最大，不在所有subsets上取。 - 中間邊singleton是maximum。 → reject — {e0,e2}合法且更大。 - 111因三邊最多故是maximum。 → reject — 它不先滿足matching資格。 - 測過一個二邊候選就足夠列全部maximizers。 → reject — 全部八候選才提供完整分類。 ## 結論與限制 八子集合全分類，maximum size2，唯一witness為{e0,e2}。 ## 驗證及來源綁定 3 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 94fd437d003f1addeeb74ab8d4d231b1284b7766692069ced54c9aceff607234 - original source SHA-256: d891a3efe19c2e43e545e39e1e80e982def72e3a3b37c914e50437febe7b0dae - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-maximum-matching-01.json)