三邊圖的全部八個matching候選

目標與範圍

完整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。

逐步主鏈

|E|=3

|\mathcal P(E)|=2^3=8

000

\varnothing\text{ valid, size }0

100,010,001

\{e_0\},\{e_1\},\{e_2\}\text{ valid, size }1

110

e_0\cap e_1=\{1\}\implies\text{invalid}

101

e_0\cap e_2=\varnothing\implies\text{valid, size }2

011

e_1\cap e_2=\{2\}\implies\text{invalid}

111

\{e_0,e_1,e_2\}\text{ invalid since }e_0\cap e_1\ne\varnothing

\text{valid sizes }0,1,1,1,2

\nu(G)=2,\quad\operatorname{Argmax}=\{\{e_0,e_2\}\}

局部子步與引理

本稿無局部子步。

逐步反向審查

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