# P4中maximal與maximum的分界 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-graph-matching/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-graph-matching-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 完整核選邊與端點，再分清三種匹配性質。 所有選邊皆以原圖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覆蓋每個頂點一次。 ## 逐步主鏈 S01 · implies操作前 M=\{e_1\} 操作後 M\subseteq E,\quad\operatorname{ends}(e_1)=\{1,2\} 條件：無 規則：work · 依賴：G1, work 葉節點依據：work M唯一選邊存在於原圖。 S02 · implies操作前 |M|=1 操作後 M\text{ is a matching} 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 只有一邊，任兩不同選邊不共端點條件為空真。 S03 · implies操作前 e_0\cap e_1=\{1\},\quad e_2\cap e_1=\{2\} 操作後 M\cup\{e_0\},M\cup\{e_2\}\text{ are invalid} 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 兩個所有未選邊都與M衝突。 S04 · implies操作前 \forall e\in E\setminus M:\ M\cup\{e\}\text{ invalid} 操作後 M\text{ is inclusion-maximal} 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 不可再加一條邊給maximal，不是最大基數。 S05 · implies操作前 N=\{e_0,e_2\}\subseteq E 操作後 \{0,1\}\cap\{2,3\}=\varnothing 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work N兩邊存在且端點互斥。 S06 · implies操作前 N\text{ matching},\quad|N|=2>|M|=1 操作後 M\text{ is not maximum} 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 更大合法matching是M非maximum的完整見證。 S07 · implies操作前 \bigcup_{e\in N}\operatorname{ends}(e)=V 操作後 N\text{ is perfect} 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work N覆蓋四頂點，每個恰一次。 S08 · implies操作前 2|Q|\le|V|=4\quad\text{for every matching }Q 操作後 |Q|\le2=|N| 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 端點互斥給全域上界，故N也是maximum。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-graph-matching-01.json)