# 圖同構：以完整映射表逐項核對雙射與鄰接當且僅當 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-graph-isomorphism/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-graph-isomorphism-01 · production-20261019-adopted-96 ## 目標與範圍 G 的頂點為 1、2、3、4，邊為 {1,2}、{2,3}、{3,4}、{1,4}；H 的頂點為 a、b、c、d，邊為 {a,c}、{b,c}、{b,d}、{a,d}。證明映射 f：1↦a、2↦c、3↦b、4↦d 是圖同構 G→H；說明雙射 g：1↦a、2↦b、3↦c、4↦d 不是同構；並證明路徑 P（邊 {1,2}、{2,3}、{3,4}）與 H 不同構，即使 f 把 P 的每條邊都送到 H 的邊。 只在 MKO 的範圍內：完整給出的有限無向簡單圖邊集合與完整映射表（假設 a1）。本稿逐項核對同構的兩項資格，並一般地證明「同構誘導邊集合之間的雙射」引理，用它作為不變量否證；度數多重集相同只當作必要線索（假設 a2）。不處理 walk、path、連通分量或圖著色的一般理論，不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - graph_basics - function_def - injective_surjective_def - finite_counting_basics - finite_forall - G1 — G：V(G)={1,2,3,4}，E(G)={{1,2},{2,3},{3,4},{1,4}}（完整列出）。 - G2 — H：V(H)={a,b,c,d}，E(H)={{a,c},{b,c},{b,d},{a,d}}（完整列出）。 - G3 — 映射表 f：f(1)=a、f(2)=c、f(3)=b、f(4)=d。 - G4 — 對照：映射表 g：g(1)=a、g(2)=b、g(3)=c、g(4)=d；路徑圖 P：V(P)={1,2,3,4}，E(P)={{1,2},{2,3},{3,4}}。 - V(G),\ E(G) — G 的頂點集合與邊集合 - \{u,v\} — 無序頂點對；u≠v 時是可能的邊 - f,\ g — 兩張從 V(G) 到 V(H) 的映射表 - P — 路徑圖：頂點 1 到 4，邊 {1,2}、{2,3}、{3,4} - f^{-1} — 雙射 f 的反函數 - \deg(v) — 頂點 v 的度數 ## 規則與來源 - graph_basics · prerequisite — （簡單無向）圖：G=(V,E)，E 中每條邊是 V 中兩個相異頂點的無序對；頂點度數是與它相連的邊數；握手引理 Σ_v deg(v)=2|E|。 - function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。 - injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。 - finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。 - iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - mko_iso_def · cited — 圖同構f:V(G)到V(H)須為雙射，且對所有不同u,v，{u,v}為G的邊當且僅當{f(u),f(v)}為H的邊。只保邊而不保非邊不足。 · mko-graph-isomorphism - finite_forall · prerequisite — 有限全稱：對有限集合 D，「對所有 t∈D，Φ(t)」等價於把 D 的每個元素逐一代入所得命題的合取；列表必須完整。 - L_edge_bij · lemma — 若 φ:V(G)→V(H) 是有限簡單圖的同構，則 {u,v}↦{φ(u),φ(v)} 是 E(G) 到 E(H) 的雙射，因此 |E(G)|=|E(H)|。 ## 逐步主鏈 S01 · definition操作前 f:V(G)\to V(H)\ \text{is an isomorphism} 操作後 f\ \text{bijective}\ \land\ \forall u\neq v:\ (\{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H)) 條件：無 規則：mko_iso_def · 依賴：G1, G2, G3 葉節點依據：mko_iso_def + def_unfold 依 MKO 展開同構的定義：兩項資格必須都成立。第一項是 f 為雙射；第二項是對每一對相異頂點，「在 G 中相鄰」與「像在 H 中相鄰」同真同假。第二項是當且僅當：邊要送到邊，非邊也要送到非邊。 S02 · implies操作前 f(1)=a,\ f(2)=c,\ f(3)=b,\ f(4)=d 操作後 f:V(G)\to V(H)\ \text{is a function} 條件：無 規則：function_def · 依賴：G1, G2, G3 葉節點依據：function_def 映射表對 V(G) 的四個頂點各給恰好一個值，而且每個值都在 V(H) 中，所以 f 是 V(G) 到 V(H) 的函數。表是完整的（假設 a1），沒有未定義的頂點。 S03 · implies操作前 f(1),f(2),f(3),f(4)=a,c,b,d 操作後 f(u)=f(v)\Rightarrow u=v 條件：無 規則：injective_surjective_def · 依賴：S02 葉節點依據：injective_surjective_def + finite_forall 四個像 a、c、b、d 兩兩相異（共 C(4,2)=6 組比較），所以相異頂點的像必相異，等價地 f(u)=f(v) 推出 u=v：f 是單射。 S04 · implies操作前 V(H)=\{a,b,c,d\} 操作後 a=f(1),\ b=f(3),\ c=f(2),\ d=f(4) 條件：無 規則：injective_surjective_def · 依賴：S02, G2 葉節點依據：injective_surjective_def + exists_intro + finite_forall 對 V(H) 的每個元素找到原像：a=f(1)、b=f(3)、c=f(2)、d=f(4)。所以 f 是滿射。 S05 · implies操作前 f\ \text{injective},\ f\ \text{surjective} 操作後 f\ \text{bijective};\ f^{-1}:\ a\mapsto 1,\ b\mapsto 3,\ c\mapsto 2,\ d\mapsto 4 條件：無 規則：and_intro_elim · 依賴：S03, S04 葉節點依據：and_intro_elim + injective_surjective_def 單射且滿射即雙射，並有唯一反函數 f⁻¹，由映射表反讀得到。第一項資格成立。 S06 · equivalent操作前 \forall u\neq v\in V(G):\ (\{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H)) 操作後 \text{the iff for each of the}\ \tbinom42=6\ \text{unordered pairs} 條件：無 規則：finite_forall · 依賴：S01, G1, finite_forall 葉節點依據：finite_forall + forall_elim + finite_counting_basics 條件對 (u,v) 與 (v,u) 是同一個命題，因為 {u,v}={v,u} 且 {f(u),f(v)}={f(v),f(u)}。相異頂點的有序對恰好是 6 個無序對各取兩種順序，所以全稱條件等價於對 6 個無序對 {1,2}、{1,3}、{1,4}、{2,3}、{2,4}、{3,4} 逐一成立。 S07 · equivalent操作前 \{u,v\}\mapsto\{f(u),f(v)\} 操作後 \{1,2\}\mapsto\{a,c\},\ \{1,3\}\mapsto\{a,b\},\ \{1,4\}\mapsto\{a,d\},\ \{2,3\}\mapsto\{b,c\},\ \{2,4\}\mapsto\{c,d\},\ \{3,4\}\mapsto\{b,d\} 條件：無 規則：function_def · 依賴：S06, G3 葉節點依據：function_def + eq_replace 對 6 個無序對查表求像。例如 {2,3} 的像是 {f(2),f(3)}={c,b}={b,c}。因 f 是單射，每個像仍是兩個相異頂點的集合。 S08 · case_split操作前 \{u,v\}\in E(G)\ ? 操作後 \{1,2\},\{2,3\},\{3,4\},\{1,4\}\in E(G);\ \{1,3\},\{2,4\}\notin E(G) 條件：無 規則：case_analysis · 依賴：G1, S06 葉節點依據：case_analysis + graph_basics 把 6 個無序對依「是否為 G 的邊」分成兩類：四條邊與兩條非邊。因為 E(G) 是完整列出的，未列出的對就是非邊。 S09 · implies操作前 \{f(u),f(v)\}\in E(H)\ ? 操作後 \{a,c\},\{b,c\},\{b,d\},\{a,d\}\in E(H);\ \{a,b\},\{c,d\}\notin E(H) 條件：無 規則：graph_basics · 依賴：G2, S07 葉節點依據：graph_basics + set_operations_def 對 S07 的 6 個像查 H 的完整邊表：{a,c}、{b,c}、{b,d}、{a,d} 在表中；{a,b}、{c,d} 不在表中，所以是 H 的非邊。 S10 · implies操作前 \text{edge status of}\ \{u,v\}\ \text{in}\ G\ \text{and of its image in}\ H 操作後 \{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H)\ \text{for all 6 pairs} 條件：無 規則：iff_intro · 依賴：S07, S08, S09 葉節點依據：iff_intro + case_analysis + finite_forall 逐對比較：G 的四條邊 {1,2}、{2,3}、{3,4}、{1,4} 的像 {a,c}、{b,c}、{b,d}、{a,d} 都是 H 的邊；G 的兩條非邊 {1,3}、{2,4} 的像 {a,b}、{c,d} 都是 H 的非邊。每一對的兩邊同真或同假，所以每一對的當且僅當都成立。 S11 · implies操作前 f\ \text{bijective},\ \text{iff on all 6 pairs} 操作後 f:G\to H\ \text{is an isomorphism},\ G\cong H 條件：無 規則：mko_iso_def · 依賴：S01, S05, S06, S10 葉節點依據：mko_iso_def + and_intro_elim 雙射由 S05 得到；S06 把全稱鄰接條件化成 6 對，S10 對 6 對都成立。依 S01 的定義，f 是同構，所以 G≅H。這個結論只依賴完整映射表與完整邊表，不依賴度數或圖形外觀。 S12 · implies操作前 g(1)=a,\ g(2)=b,\ \{1,2\}\in E(G) 操作後 \{g(1),g(2)\}=\{a,b\}\notin E(H)\Rightarrow g\ \text{not an isomorphism} 條件：無 規則：contradiction · 依賴：S01, G1, G2, G4 葉節點依據：contradiction + quantifier_negation + injective_surjective_def g 的四個像 a、b、c、d 相異且涵蓋 V(H)，所以 g 也是雙射。但 {1,2} 是 G 的邊，其像 {a,b} 不是 H 的邊，當且僅當在這一對失敗。全稱條件只要一個反例就被否定，所以 g 不是同構。可見雙射本身不夠。 S13 · implies操作前 f\ \text{on}\ P:\ \{1,2\},\{2,3\},\{3,4\}\mapsto\{a,c\},\{b,c\},\{b,d\} 操作後 \text{every edge of}\ P\ \text{goes to an edge of}\ H 條件：無 規則：graph_basics · 依賴：G4, G3, G2 葉節點依據：graph_basics + function_def 把 f 看成 V(P) 到 V(H) 的雙射：P 的三條邊的像 {a,c}、{b,c}、{b,d} 都在 E(H) 中。所以 f 「保邊」。這正是 MKO 警告的情況：保邊還不夠。 S14 · implies操作前 \{1,4\}\notin E(P) 操作後 \{f(1),f(4)\}=\{a,d\}\in E(H)\Rightarrow f\ \text{is not an isomorphism}\ P\to H 條件：無 規則：contradiction · 依賴：S13, G4, G2 葉節點依據：contradiction + quantifier_negation {1,4} 不是 P 的邊（P 的邊表完整），但其像 {a,d} 是 H 的邊。當且僅當的「⇐」方向失敗，所以 f 不是 P 到 H 的同構。只核原邊映成邊就宣稱同構是錯的。 S15 · implies操作前 |E(P)|=3,\ |E(H)|=4 操作後 \text{no isomorphism}\ P\to H\ \text{exists} 條件：3\neq 4 規則：L_edge_bij · 依賴：G2, G4 葉節點依據：L_edge_bij + contrapositive + numeric_evaluation 依引理 L_edge_bij（S15.1 到 S15.3 證明），任何同構 φ:P→H 都給出 E(P) 到 E(H) 的雙射，因此 |E(P)|=|E(H)|。但 3≠4，取逆否，不存在任何同構 P→H，不只是 f 不行。邊數這個不變量不符就足以否證。 S16 · implies操作前 \deg\ \text{in}\ G\ \text{and}\ H 操作後 \{2,2,2,2\}=\{2,2,2,2\} 條件：無 規則：graph_basics · 依賴：G1, G2, S11 葉節點依據：graph_basics + numeric_evaluation G 中 N(1)={2,4}、N(2)={1,3}、N(3)={2,4}、N(4)={1,3}；H 中 N(a)={c,d}、N(b)={c,d}、N(c)={a,b}、N(d)={a,b}；所有度數都是 2，握手引理核對 4·2=2·4。度數多重集相符與 S11 一致。一般而言它只是必要條件，C6 與兩個三角形反駁一般充分性；但本題是四頂點、度數全為 2 的簡單圖，這個特殊條件確實迫使兩圖都是 C4。本稿選用 S11 的完整映射直接作證，沒有使用這個分類路徑。 ## 局部子步與引理 S15.1 · implies操作前 \{u,v\}\in E(G) 操作後 \{\varphi(u),\varphi(v)\}\in E(H) 條件：\varphi\ \text{isomorphism} 規則：mko_iso_def · 依賴：mko_iso_def, injective_surjective_def 葉節點依據：mko_iso_def + injective_surjective_def 設 φ 為同構、{u,v} 為 G 的邊，則 u≠v，單射給 φ(u)≠φ(v)，而當且僅當的「⇒」方向給 {φ(u),φ(v)}∈E(H)。所以這個對應確實把 E(G) 送進 E(H)。 S15.2 · implies操作前 \{\varphi(u),\varphi(v)\}=\{\varphi(u'),\varphi(v')\} 操作後 \{u,v\}=\{u',v'\} 條件：\varphi\ \text{bijective} 規則：injective_surjective_def · 依賴：S15.1, injective_surjective_def 葉節點依據：injective_surjective_def + function_def 把反函數 φ⁻¹ 逐元素作用在兩個相等的二元集合上：φ⁻¹ 送 {φ(u),φ(v)} 到 {u,v}，送 {φ(u′),φ(v′)} 到 {u′,v′}，所以兩個邊相同。邊的對應是單射。 S15.3 · implies操作前 \{p,q\}\in E(H) 操作後 \{\varphi^{-1}(p),\varphi^{-1}(q)\}\in E(G)\ \Rightarrow\ |E(G)|=|E(H)| 條件：\varphi\ \text{isomorphism} 規則：mko_iso_def · 依賴：S15.1, S15.2, mko_iso_def, finite_counting_basics 葉節點依據：mko_iso_def + injective_surjective_def + finite_counting_basics 給 H 的邊 {p,q}，令 u=φ⁻¹(p)、v=φ⁻¹(q)，則 u≠v 且 {φ(u),φ(v)}={p,q}∈E(H)；當且僅當的「⇐」方向給 {u,v}∈E(G)，它被送到 {p,q}。所以邊的對應是滿射。結合 S15.1、S15.2，它是有限集合 E(G) 到 E(H) 的雙射，依有限計數 |E(G)|=|E(H)|。S15.1 到 S15.3 合起來證得引理 L_edge_bij。 ## 逐步反向審查 - S16 · premise_audit · G1, G2, graph_basics — 本稿只把此步記為與結論一致的不變量核對；S11 的直接映射證明不依賴它。若補上四頂點 2-正則簡單圖必為 C4 的分類論證，也可另成證明路徑。 - S15.3 · premise_audit · mko_iso_def, finite_counting_basics — 滿射這一步正是用到「非邊對應非邊」那一半的當且僅當；只保邊的映射不保證這一步。此子步不使用 L_edge_bij。 - S15.2 · premise_audit · injective_surjective_def — 需要 φ⁻¹ 存在，即 φ 為雙射；此子步不使用 L_edge_bij。 - S15.1 · premise_audit · mko_iso_def, injective_surjective_def — 只用到當且僅當的一個方向與單射；此子步不使用 L_edge_bij。 - S15 · premise_audit · L_edge_bij, contrapositive — 用的是「同構 ⇒ 邊數相等」的逆否；反向「邊數相等 ⇒ 同構」不成立，不宣稱。 - S14 · premise_audit · G4, G2, contradiction — 這只否證 f 這張表；P 與 H 是否完全不同構，需要 S15 的不變量論證。 - S13 · premise_audit · G4, G3, G2 — 只核了「⇒」方向；不宣稱非邊也被保持（S14 證明它沒有被保持）。 - S12 · premise_audit · G1, G2, G4, contradiction — 否證只需一個失敗的對；此步不宣稱 G 與 H 不同構（S11 已證同構），只說 g 這張表不是同構。 - S11 · sufficient_goal_reduction · S01, S05, S06, S10 — 目標 G：f 是同構。足夠條件 H：f 雙射且 6 對的當且僅當都成立；H⇒G 由 S01、S06。H 由 S02 到 S10 正向證成，沒有把 G 當作前提。 - S10 · premise_audit · S08, S09, iff_intro, case_analysis — 邊的情況給出「⇒」方向，非邊的情況給出「⇐」方向（逆否形式：G 的非邊對應 H 的非邊）。缺少任何一類都不能得到當且僅當。 - S09 · premise_audit · G2, S07, graph_basics — 只需逐一查表；非邊的判定依賴 E(H) 列表完整（假設 a1）。 - S08 · premise_audit · G1, case_analysis — 兩類涵蓋全部 6 對，且互斥；需要 E(G) 列表完整，否則「未列出」不代表非邊。 - S07 · inverse_equivalence · function_def, S05 — 查表是等值代換；用 f⁻¹ 可把每個像倒推回原來的對，雙向成立。 - S06 · inverse_equivalence · finite_forall, set_extensionality — 全稱推出每個實例（∀ 消去）；6 個實例列表完整時，全部成立推出全稱。雙向成立。 - S05 · premise_audit · S03, S04, injective_surjective_def — 雙射只是第一項資格；它本身不推出同構（S12 的 g 也是雙射）。 - S04 · premise_audit · S02, G2, injective_surjective_def — 每個 V(H) 元素都只需一個原像；四個元素都已列出。 - S03 · premise_audit · S02, injective_surjective_def — 六組比較全部完成；只宣稱單射，不由此推出鄰接條件。 - S02 · premise_audit · G3, function_def — 需要每個頂點恰有一筆映射紀錄、值在 V(H) 中；兩者都可直接從表讀出。 - S01 · premise_audit · mko_iso_def — 此步只展開定義，不推出新事實；之後先核雙射（S02 到 S05），再核鄰接條件（S06 到 S10）。 ## 錯誤控制與反例 只保邊不夠MKO 指出的常見誤解是只核原邊映成邊就宣稱同構。f 把 P 的三條邊都送到 H 的邊（S13），但非邊 {1,4} 被送到邊 {a,d}（S14）。當且僅當的兩個方向都要核：邊對應邊，非邊對應非邊。 度數序列相同不是證明六頂點環 C6 與兩個不相交的三角形都是六個頂點、六條邊、每點度數 2，但不同構：兩個三角形中有三個兩兩相鄰的頂點，C6 沒有，而同構把兩兩相鄰的三點送到兩兩相鄰的三點。所以不變量相符只是必要條件；本稿的同構結論來自 S11 的逐對核對。 雙射與鄰接要分開核g 是雙射卻不是同構（S12）；另一方面，若映射表把兩個頂點送到同一點，某個 {u,v} 的像就只剩一個頂點，根本不是候選邊。MKO 的順序是先核雙射，再核全部無序頂點對。 - 對任意兩個有限無向簡單圖，只要度數多重集相同，就足以推出兩圖同構 → reject — C6 與兩個不相交三角形的度數多重集相同卻不同構，否定這個一般主張。本題四頂點且度數全2是特殊情形，確實迫使兩圖都是C4；本稿仍以S11映射表直接證明G≅H。 - f 把 P 的每條邊都送到 H 的邊，所以 f 是 P 到 H 的同構 → reject — 非邊 {1,4} 被送到 H 的邊 {a,d}。 - g 是 V(G) 到 V(H) 的雙射，所以 g 是同構 → reject — {1,2}∈E(G) 但 {g(1),g(2)}={a,b}∉E(H)。 - P 與 H 都有四個頂點，所以適當選映射表就能讓它們同構 → reject — 依 L_edge_bij，同構需要邊數相等，但 |E(P)|=3≠4=|E(H)|。 ## 結論與限制 f：1↦a、2↦c、3↦b、4↦d 是雙射，且 6 個無序頂點對的鄰接當且僅當全部成立，所以 f 是同構，G≅H。雙射 g 在 {1,2}↦{a,b} 失敗，不是同構。f 把路徑 P 的每條邊送到 H 的邊，卻把非邊 {1,4} 送到邊 {a,d}；而且依引理 L_edge_bij，|E(P)|=3≠4=|E(H)|，P 與 H 不同構。 - 錯誤控制中「同構保持兩兩相鄰的三點」只作說明，由當且僅當條件直接得到，未列為編號步驟。 - finite_forall 是本稿的前提，不在本稿中由更基本的邏輯規則推出。 ## 驗證及來源綁定 5 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: a7cc7455e8b911e77e5121725e1be4abeed121e79d85845f5c53dcd1836af658 - original source SHA-256: 9d22ff5f2bd20224ad3785c20866dd5d700d99fedad9037b43fd496881eceb3e - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-graph-isomorphism-01.json)