P4中maximal與maximum的分界

目標與範圍

完整核選邊與端點，再分清三種匹配性質。

所有選邊皆以原圖edge index表示。

已知條件與符號

• work

• G1 — V={0,1,2,3}；e0={0,1}、e1={1,2}、e2={2,3}是全部邊。M={e1}，N={e0,e2}。

• V,E — 完整頂點與邊集合
• M,N — 候選邊集合

規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。

• mko_definition · cited — 完整有限無向簡單圖上核每條選邊存在及端點互斥。另分清matching、maximal、maximum與perfect；較大matching witness可否證maximum，但單一matching不給最優性。 · mko-graph-matching
• work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 matching選原邊且不同選邊端點互斥；maximal不能再加邊；maximum基數為全體matching中最大；perfect覆蓋每個頂點一次。

逐步主鏈

M=\{e_1\}

M\subseteq E,\quad\operatorname{ends}(e_1)=\{1,2\}

|M|=1

M\text{ is a matching}

e_0\cap e_1=\{1\},\quad e_2\cap e_1=\{2\}

M\cup\{e_0\},M\cup\{e_2\}\text{ are invalid}

\forall e\in E\setminus M:\ M\cup\{e\}\text{ invalid}

M\text{ is inclusion-maximal}

N=\{e_0,e_2\}\subseteq E

\{0,1\}\cap\{2,3\}=\varnothing

N\text{ matching},\quad|N|=2>|M|=1

M\text{ is not maximum}

\bigcup_{e\in N}\operatorname{ends}(e)=V

N\text{ is perfect}

2|Q|\le|V|=4\quad\text{for every matching }Q

|Q|\le2=|N|

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S07, work — 此上界明示，沒有只因perfect名稱便省證。
• S07 · premise_audit · G1, S06, work — M只覆蓋1、2，故不perfect。
• S06 · premise_audit · G1, S05, work — 不需要先求所有matchings才能否定M最優。
• S05 · premise_audit · G1, S04, work — M與N不需互為子集合才能比較基數。
• S04 · premise_audit · G1, S03, work — 不偷換局部不可擴張為全域比較。
• S03 · premise_audit · G1, S02, work — 已窮盡E減M，沒有其他可加邊。
• S02 · premise_audit · G1, S01, work — 空真不是省略edge存在性。
• S01 · premise_audit · G1, work — 不存在edge index不能作matching。

錯誤控制與反例

edge index

只用e0、e1、e2，先核存在再核端點。

三種責任

matching核合法、maximal核可加、maximum核全域上界。

• M maximal故maximum。 → reject — N有兩邊，大於M一邊。
• {e0,e1}是matching。 → reject — 兩邊共有端點1。
• maximum必唯一。 → reject — 例如四圈兩組相對邊都可為maximum；此性質不保證唯一。

結論與限制

M為maximal但非maximum；N為perfect且maximum。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 22060fb56bf6f78f3fa82bf3167fab58e9952536d67a4ce7133e8e015f9d26c7
• original source SHA-256: 4cbd728a4a404d039a883891cd08ccedaba32b8a02eb68156ade1d3055bfc564
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

同源完整 JSON（含公式、AST、反控制與修訂記錄）