# 有限簡單無向圖：鄰居、度數與握手公式

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-graph/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-graph-01 · production-20261019-adopted-96



## 目標與範圍

設 V={1,2,3,4,5}，邊以端點對清單輸入：(1,2)、(2,1)、(2,3)、(3,4)、(2,4)、(4,2)，每一項表示一條無向邊。把輸入正規化為邊集合 E，求每個頂點的鄰居集合 N(v) 與度數 deg(v)，核對度數和等於 2|E|，並對每個有限簡單無向圖證明握手公式 Σ_{v∈V} deg(v)=2|E|。

在 MKO 的範圍內工作：有限頂點集合、二元素子集合作為邊、沒有自環與重邊、允許空圖。以雙重計數證明握手公式；雙重計數原理（有限集合按分量分組計數）作為前提。不處理有向圖、多重圖、自環計數、連通性或樹；不從畫法推論相鄰性；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- set_extensionality
- set_builder
- finite_counting_basics
- finite_sum_rules
- numeric_evaluation
- graph_defs


- G1 — V={1,2,3,4,5}，頂點標籤互異（MKO 假設 a1）。
- G2 — 輸入清單依序為 (1,2)、(2,1)、(2,3)、(3,4)、(2,4)、(4,2)；每一項 (u,v) 表示無向邊 {u,v}，無向邊不區分端點順序（MKO 假設 a2）。
- G3 — 另一個圖 G₀=({1,2,3},∅) 用來檢查空邊集合的邊界。


- G=(V,E) — 有限簡單無向圖
- \{u,v\} — 以 u、v 為端點的無向邊（u≠v）
- N(v) — v 的鄰居集合 {u∈V ∣ {u,v}∈E}
- \deg(v) — v 的度數 |N(v)|
- E_v — 含 v 的邊所成集合 {e∈E ∣ v∈e}
- I — 關聯對集合 {(v,e)∈V×E ∣ v∈e}





## 規則與來源


- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- 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。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_graph_def · cited — 有限簡單無向圖 G=(V,E) 由有限頂點集合 V 與其二元素子集合構成的邊集合 E 組成。沒有自環或重邊；N(v)={u∈V:{u,v}∈E}，deg(v)=|N(v)|，所有頂點度數和為 2|E|。 · mko-graph
- graph_defs · prerequisite — 定義部分（不含度數和的結論）：G=(V,E)，V 有限，E 的每個元素是 V 的二元素子集合 {u,v}（u≠v）；N(v)={u∈V ∣ {u,v}∈E}；deg(v)=|N(v)|。
- two_element_set · prerequisite — {u,v}={v,u}；u≠v 時 {u,v} 恰有兩個元素；{u,u}={u} 只有一個元素；z∈{u,v} 當且僅當 z=u 或 z=v。
- roster_membership · prerequisite — 列舉集合的成員關係：對以列舉給出的有限集合 S={s_i ∣ 1≤i≤n}，z∈S 當且僅當存在 i 使 z=s_i。
- double_counting · prerequisite — 雙重計數：對有限集合 X、Y 與 I⊆X×Y，|I|=Σ_{x∈X} |{y∈Y ∣ (x,y)∈I}|=Σ_{y∈Y} |{x∈X ∣ (x,y)∈I}|（I 依第一或第二分量分成互斥的切片，再用互斥有限集合的加法原理）。
- L_handshake · lemma — 對每個有限簡單無向圖 G=(V,E)，Σ_{v∈V} deg(v)=2|E|。





## 逐步主鏈

S01 · implies操作前

(1,2),(2,1),(2,3),(3,4),(2,4),(4,2)

操作後

\text{each entry has two distinct endpoints in}\ V

條件：無

規則：mko_graph_def · 依賴：G1, G2, mko_graph_def

葉節點依據：mko_graph_def + roster_membership + two_element_set

依 MKO 假設 a1，每條邊的兩個端點都要在 V 中且相異。逐項檢查：出現的端點 1、2、3、4 都在 V 中，六項的兩端分別是 1≠2、2≠1、2≠3、3≠4、2≠4、4≠2。所以每一項都表示一條合法的無向邊，沒有自環。



S02 · equivalent操作前

\{1,2\},\{2,1\},\{2,3\},\{3,4\},\{2,4\},\{4,2\}

操作後

E=\{\{1,2\},\{2,3\},\{3,4\},\{2,4\}\}

條件：無

規則：set_extensionality · 依賴：S01, two_element_set, set_extensionality

葉節點依據：set_extensionality + two_element_set

把每一項換成無向邊 {u,v}。{1,2} 與 {2,1} 有相同元素，依集合相等是同一條邊；{2,4} 與 {4,2} 也一樣。E 是集合，重複的元素只算一次，所以 E={{1,2},{2,3},{3,4},{2,4}}。正規化不製造新邊，也不刪掉任何不同的邊。



S03 · implies操作前

E=\{\{1,2\},\{2,3\},\{3,4\},\{2,4\}\}

操作後

|E|=4

條件：無

規則：finite_counting_basics · 依賴：S02, set_extensionality, finite_counting_basics

葉節點依據：set_extensionality + finite_counting_basics

四條邊兩兩不同：{1,2} 含 1 而其他三條都不含 1；{2,3} 含 3 而不含 4；{3,4} 含 4 而不含 2；{2,4} 含 2 而不含 3。所以四者是不同的集合，|E|=4，不是輸入清單的 6 項。|E| 也不超過 V 的二元素子集合個數 C(5,2)=10（N4）。



S04 · equivalent操作前

N(1)=\{u\in V\mid\{u,1\}\in E\}

操作後

N(1)=\{2\}

條件：無

規則：graph_defs · 依賴：S02, graph_defs

葉節點依據：graph_defs + set_extensionality + two_element_set

u∈N(1) 當且僅當 {u,1}∈E。E 中含 1 的邊只有 {1,2}，而 {u,1}={1,2} 且 u≠1 推出 u=2。所以 N(1)={2}。



S05 · equivalent操作前

N(2)=\{u\in V\mid\{u,2\}\in E\}

操作後

N(2)=\{1,3,4\}

條件：無

規則：graph_defs · 依賴：S02, graph_defs

葉節點依據：graph_defs + set_extensionality + two_element_set

E 中含 2 的邊是 {1,2}、{2,3}、{2,4}，另一端分別是 1、3、4；{3,4} 不含 2，而 {2,5} 不在 E 中。所以 N(2)={1,3,4}。清單中 (2,4) 與 (4,2) 都出現，但 4 在 N(2) 中只算一次。



S06 · equivalent操作前

N(3),\ N(4)

操作後

N(3)=\{2,4\},\ N(4)=\{2,3\}

條件：無

規則：graph_defs · 依賴：S02, graph_defs

葉節點依據：graph_defs + set_extensionality + two_element_set

含 3 的邊是 {2,3}、{3,4}，所以 N(3)={2,4}；含 4 的邊是 {3,4}、{2,4}，所以 N(4)={2,3}。



S07 · equivalent操作前

N(5)=\{u\in V\mid\{u,5\}\in E\}

操作後

N(5)=\varnothing

條件：無

規則：graph_defs · 依賴：S02, graph_defs

葉節點依據：graph_defs + set_extensionality

E 的四條邊都不含 5，所以沒有 u 使 {u,5}∈E，N(5)=∅。5 是孤立頂點，但它仍是 V 的元素，也是圖的一部分。



S08 · implies操作前

N(1),N(2),N(3),N(4),N(5)

操作後

\deg(1)=1,\ \deg(2)=3,\ \deg(3)=2,\ \deg(4)=2,\ \deg(5)=0

條件：無

規則：graph_defs · 依賴：S04, S05, S06, S07, graph_defs

葉節點依據：graph_defs + finite_counting_basics

deg(v)=|N(v)|，即不同鄰居的個數：|{2}|=1、|{1,3,4}|=3、|{2,4}|=2、|{2,3}|=2、|∅|=0。孤立頂點的度數為零。



S09 · implies操作前

\sum_{v\in V}\deg(v),\ 2|E|

操作後

1+3+2+2+0=8=2\cdot 4

條件：無

規則：numeric_evaluation · 依賴：S03, S08

葉節點依據：numeric_evaluation + finite_sum_rules

度數和 1+3+2+2+0=8，2|E|=2·4=8，兩者相等。這個例子吻合握手公式，但一個例子不證明一般結論；一般證明在 S10。



S10 · theorem_application操作前

G=(V,E)\ \text{finite simple undirected}

操作後

\sum_{v\in V}\deg(v)=2|E|

條件：V\ \text{finite}; \text{no loops, no multiple edges}

規則：L_handshake · 依賴：S03, S08, L_handshake

葉節點依據：graph_defs + double_counting + two_element_set + finite_sum_rules

引理 L_handshake 對每個有限簡單無向圖成立；它在子步 S10.1 到 S10.3 證明，證明只用 graph_defs 的定義與雙重計數，不用 MKO 陳述中的握手公式本身。用於本例：Σ deg(v)=8=2·4，與 S09 的直接計算一致。



S11 · implies操作前

|E'|=6\ \text{(counting list entries)}

操作後

2\cdot 6=12\neq 8=\sum_{v}\deg(v)

條件：無

規則：contradiction · 依賴：S08, S10, contradiction

葉節點依據：contradiction + numeric_evaluation

若把 (1,2) 與 (2,1)、(2,4) 與 (4,2) 各算成兩條邊，會得到 6 條。但度數由鄰居集合決定（S08），和為 8；而 S10 對簡單圖證明了度數和必等於 2|E|。12≠8，所以「6 條邊」與簡單圖的定義矛盾，是計數錯誤。



S12 · implies操作前

G_0=(\{1,2,3\},\varnothing)

操作後

\deg(v)=0\ \text{for every}\ v,\ \sum_{v}\deg(v)=0=2\cdot 0

條件：無

規則：graph_defs · 依賴：G3, graph_defs, L_handshake

葉節點依據：graph_defs + finite_sum_rules + numeric_evaluation

MKO 允許空圖。取 V₀={1,2,3}、E₀=∅：對每個 v，沒有 {u,v}∈∅，所以 N(v)=∅、deg(v)=0；度數和 0+0+0=0=2·0，與 L_handshake 一致。若 V 也是空集合，度數和是空和 0，仍等於 2·0。



S13 · implies操作前

\text{S02, S03, S08, S10, S12}

操作後

|E|=4,\ (\deg(v))_{v=1}^{5}=(1,3,2,2,0),\ \sum_v\deg(v)=2|E|

條件：無

規則：and_intro_elim · 依賴：S02, S03, S08, S10, S12

葉節點依據：and_intro_elim

彙整：正規化後 E={{1,2},{2,3},{3,4},{2,4}}，|E|=4（S02、S03）；度數依序為 1、3、2、2、0（S08）；握手公式對每個有限簡單無向圖成立，本例 8=2·4（S10）；空邊集合時度數和為 0（S12）。







## 局部子步與引理

S10.1 · implies操作前

E_v=\{e\in E\mid v\in e\}

操作後

|E_v|=\deg(v)

條件：u\neq v\ \text{for every}\ u\in N(v)

規則：graph_defs · 依賴：graph_defs, two_element_set, set_extensionality

葉節點依據：graph_defs + two_element_set + set_extensionality + injective_surjective_def + finite_counting_basics

固定 v，定義 φ(u)={u,v}，把 N(v) 映到 E_v（u∈N(v) 表示 {u,v}∈E，且這條邊含 v）。單射：若 {u,v}={u′,v}，因 u≠v，由 u∈{u′,v} 得 u=u′。滿射：若 e∈E_v，e 是含 v 的二元素集合，所以 e={v,w} 且 w≠v；{w,v}∈E 表示 w∈N(v)，且 φ(w)=e。φ 是雙射，依有限計數 |E_v|=|N(v)|=deg(v)。



S10.2 · implies操作前

\{v\in V\mid v\in e\}\ \text{for}\ e\in E

操作後

|\{v\in V\mid v\in e\}|=|e|=2

條件：無

規則：two_element_set · 依賴：graph_defs, two_element_set

葉節點依據：graph_defs + two_element_set

固定邊 e={u,w}∈E（u≠w，兩端都在 V 中）。屬於 e 的頂點恰是 u 與 w，所以這個集合就是 e，元素個數是 2。



S10.3 · implies操作前

I=\{(v,e)\in V\times E\mid v\in e\}

操作後

\sum_{v\in V}\deg(v)=|I|=\sum_{e\in E}2=2|E|

條件：V,\ E\ \text{finite}

規則：double_counting · 依賴：S10.1, S10.2, double_counting, finite_sum_rules

葉節點依據：double_counting + finite_sum_rules + eq_refl_symm_trans

對關聯對集合 I 做雙重計數：按第一分量分組，v 那一組是 {e ∣ (v,e)∈I}=E_v，大小 deg(v)（S10.1），所以 |I|=Σ_v deg(v)；按第二分量分組，e 那一組是 {v ∣ v∈e}，大小 2（S10.2），所以 |I|=Σ_e 2=2|E|（有限和的常數倍）。兩式都等於 |I|，得 Σ_v deg(v)=2|E|。S10.1 到 S10.3 證得引理 L_handshake。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S02, S03, S08, S10, S12, and_intro_elim — 目標 G：E、各度數、握手公式的核對與一般證明。足夠條件 H：S02、S03、S08、S10、S12；H⇒G 只是合取，H 由 G1 到 G3 正向證成，沒有把 G 當作前提。
- S12 · premise_audit · graph_defs, finite_sum_rules, L_handshake — 需要空和等於 0 的約定（有限和規則）；N5 重算 0+0+0=2·0。
- S11 · premise_audit · S08, S10, contradiction, numeric_evaluation — 此步只說明錯誤計數與已證公式矛盾（N3）；正確的 |E|=4 來自 S02、S03。
- S10.3 · premise_audit · S10.1, S10.2, double_counting, finite_sum_rules, eq_refl_symm_trans — 需要 V、E 有限，雙重計數才適用；空圖時兩邊都是 0，仍成立。
- S10.2 · premise_audit · graph_defs, two_element_set — 需要兩端相異；端點都在 V 中保證 e⊆V。
- S10.1 · premise_audit · graph_defs, two_element_set, injective_surjective_def, finite_counting_basics — 本稿固定無自環的二元素邊模型，這裡的單射論證使用 u≠v。不能一概說允許自環後鄰點與關聯邊的對應必失敗：若以單點集合表示 loop，該對應仍可能雙射；此時後續每條邊恰有兩個端點的計數才不再適用。loop 的度數慣例須另定，本稿不處理。
- S10 · premise_audit · L_handshake, S03, S08 — 需要 G 是有限簡單無向圖（S01、S02 已確認）；有向圖或多重圖不在範圍內。
- S09 · premise_audit · S03, S08, numeric_evaluation — 可獨立重算（N1、N2）；不由此宣稱公式對所有圖成立。
- S08 · premise_audit · S04, S05, S06, S07, graph_defs — 需要每個 N(v) 已以集合正確求出；度數數的是不同鄰居，不是清單中的出現次數。
- S07 · inverse_equivalence · graph_defs, set_extensionality — 兩個集合都沒有元素，相等；這需要檢查 E 的全部四條邊。
- S06 · inverse_equivalence · graph_defs, set_extensionality — 同 S05，對每個候選頂點逐一核對，兩向成立。
- S05 · inverse_equivalence · graph_defs, set_extensionality — 逐一檢查 V 中 u≠2 的四個候選 1、3、4、5，兩向的包含都成立。
- S04 · inverse_equivalence · graph_defs, set_extensionality — 兩個包含都已核對：2∈N(1) 因 {2,1}∈E；其他 u 沒有同時含 1 與 u 的邊。
- S03 · premise_audit · set_extensionality, finite_counting_basics — 計數前必須先確認元素互異；這正是 MKO 第一段強調的重點。
- S02 · inverse_equivalence · set_extensionality, two_element_set — 清單與 E 描述同一個邊集合：清單的每一項都在 E 中，E 的每條邊都出現在清單中，兩向成立。
- S01 · premise_audit · G1, G2, mko_graph_def, two_element_set — 若某項是 (3,3)，它對應 {3,3}={3}，只有一個元素，不是邊；本輸入沒有這種項。此步只核對資格，不計數。





## 錯誤控制與反例

同一條無向邊不要算兩次MKO 指出的誤解之一是把無向邊的兩種排序算成兩條。{1,2}={2,1}、{2,4}={4,2}，所以六項輸入只有四條邊（S02、S03）。若算成 6 條，2·6=12 與度數和 8 不符（S11），握手公式立即揭露這個錯誤。

畫線相交不是頂點MKO 指出的另一個誤解是把示意線相交當成新增頂點。若把 1、2、3、4 畫在 (0,0)、(2,2)、(0,2)、(2,0)，則邊 {1,2} 與 {3,4} 的線段在 (1,1) 相交，但 V 仍是 {1,2,3,4,5}，(1,1) 不是頂點，也不產生新邊。相鄰性只由 E 決定，不由畫法決定。

度數是不同鄰居數，孤立頂點仍要計入deg(2)=|{1,3,4}|=3，不是 2 在清單中出現的次數 5。5 沒有鄰居，deg(5)=0，但 5 仍是頂點，度數和要包含它（加 0）。自環 {v,v}={v} 不是二元素集合，簡單圖中不存在。


- (1,2) 與 (2,1) 是兩條不同的邊，所以 |E|=6 → reject — {1,2}={2,1}；|E|=4，而 2·6=12 與度數和 8 不符。
- 圖上兩條邊的線段相交處是一個新頂點 → reject — 頂點集合 V 是給定的；交叉點只屬於畫法，不在 V 中，也不改變 E。
- 5 沒有鄰居，所以 5 不是圖的頂點 → reject — 5∈V；它是度數 0 的孤立頂點。
- 可以加入邊 {3,3}，使 deg(3) 變成 3 → reject — {3,3}={3} 只有一個元素，不是二元素子集合；簡單圖沒有自環。





## 結論與限制

輸入的六項正規化後只有四條不同的無向邊：E={{1,2},{2,3},{3,4},{2,4}}。鄰居集合為 N(1)={2}、N(2)={1,3,4}、N(3)={2,4}、N(4)={2,3}、N(5)=∅，度數依序為 1、3、2、2、0，度數和 8=2·4=2|E|。對每個有限簡單無向圖，Σ_v deg(v)=2|E|（以雙重計數證明）；空邊集合時度數和為 0。


- 雙重計數原理（double_counting）是本稿的前提，未在此由加法原理逐步推出。
- 本稿不處理握手公式的推論（例如奇度頂點個數為偶數），也不處理有向圖、多重圖或連通性。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 56916889c62315f978ca130e85048a57dac57e96f65188fb5224dbb0fa53182f
- original source SHA-256: 695ff8e49c105f1940c6ba7abe0fe527fc5fa6cc710601419531ac68bc4782e4
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-graph-01.json)