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

目標與範圍

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

逐步主鏈

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

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

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

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

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

|E|=4

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

N(1)=\{2\}

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

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

N(3),\ N(4)

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

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

N(5)=\varnothing

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

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

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

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

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

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

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

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

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

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

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

局部子步與引理

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

|E_v|=\deg(v)

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

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

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|

逐步反向審查

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