圖同構：以完整映射表逐項核對雙射與鄰接當且僅當

目標與範圍

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)|。

逐步主鏈

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))

f(1)=a,\ f(2)=c,\ f(3)=b,\ f(4)=d

f:V(G)\to V(H)\ \text{is a function}

f(1),f(2),f(3),f(4)=a,c,b,d

f(u)=f(v)\Rightarrow u=v

V(H)=\{a,b,c,d\}

a=f(1),\ b=f(3),\ c=f(2),\ d=f(4)

f\ \text{injective},\ f\ \text{surjective}

f\ \text{bijective};\ f^{-1}:\ a\mapsto 1,\ b\mapsto 3,\ c\mapsto 2,\ d\mapsto 4

\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}

\{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\}

\{u,v\}\in E(G)\ ?

\{1,2\},\{2,3\},\{3,4\},\{1,4\}\in E(G);\ \{1,3\},\{2,4\}\notin E(G)

\{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)

\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}

f\ \text{bijective},\ \text{iff on all 6 pairs}

f:G\to H\ \text{is an isomorphism},\ G\cong H

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}

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

\{1,4\}\notin E(P)

\{f(1),f(4)\}=\{a,d\}\in E(H)\Rightarrow f\ \text{is not an isomorphism}\ P\to H

|E(P)|=3,\ |E(H)|=4

\text{no isomorphism}\ P\to H\ \text{exists}

\deg\ \text{in}\ G\ \text{and}\ H

\{2,2,2,2\}=\{2,2,2,2\}

局部子步與引理

\{u,v\}\in E(G)

\{\varphi(u),\varphi(v)\}\in E(H)

\{\varphi(u),\varphi(v)\}=\{\varphi(u'),\varphi(v')\}

\{u,v\}=\{u',v'\}

\{p,q\}\in E(H)

\{\varphi^{-1}(p),\varphi^{-1}(q)\}\in E(G)\ \Rightarrow\ |E(G)|=|E(H)|

逐步反向審查

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