圖的 walk 與 simple path：逐對核對、長度與 trail 的區別

目標與範圍

有限無向無 loop 簡單圖 G：V={0,1,2,3,4}，E={{0,1},{1,2},{2,3},{0,3},{1,3},{3,4}}。對頂點序列 W₁=(0,1,2,3,4)、W₂=(0,1,3,1,2)、W₃=(0,2,3)、W₄=(2,3,0,1,3,4)、W₅=(4)、W₆=(1,1) 逐一判定是否為 walk、長度為何、是否為 simple path；並證明 simple path 不重複邊，以及本圖中 simple path 的長度至多為 4。

在 MKO 的範圍內工作：頂點標為 0 到 n−1，完整的無向簡單邊集合與有序頂點序列都明示（假設 a1）；空序列不算 walk，單一頂點是長度 0 的 simple path（假設 a2）。trail 只用來對照 simple path；不處理 cycle、連通分量或有向圖，不改動 canonical MKO 或英文 edition。

已知條件與符號

• graph_basics
• finite_counting_basics
• quantifier_negation
• and_intro_elim
• numeric_evaluation

• G1 — V={0,1,2,3,4}；E={{0,1},{1,2},{2,3},{0,3},{1,3},{3,4}}，共 6 條邊；除此之外沒有其他邊。
• G2 — 待判定的序列：W₁=(0,1,2,3,4)、W₂=(0,1,3,1,2)、W₃=(0,2,3)、W₄=(2,3,0,1,3,4)、W₅=(4)、W₆=(1,1)，以及空序列 ()。

• G=(V,E) — 給定的有限無向簡單圖
• \{p,q\} — 無序頂點對；p≠q 時才可能是邊
• W=(v_i)_{i=0}^{k} — 頂點序列 v₀ 到 v_k，共 k+1 項
• k — walk 的 edge length（連續對的個數）
• W_1,W_2,W_3,W_4,W_5,W_6 — 六個待判定的序列
• n=|V|=5 — 頂點數

規則與來源

• graph_basics · prerequisite — （簡單無向）圖：G=(V,E)，E 中每條邊是 V 中兩個相異頂點的無序對；頂點度數是與它相連的邊數；握手引理 Σ_v deg(v)=2|E|。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• mko_walk_def · cited — 固定有限無向無 loop 簡單圖。頂點序列 (v₀ 到 v_k) 為 walk，若每個連續無序對都是邊；其 edge length 為 k。simple path 是頂點不重複的 walk。walk 可重複頂點或邊，cycle 與 trail 另有額外責任。空序列不作 walk；單頂點序列是長度 0 的 simple path。 · mko-graph-walk-simple-path
• trail_def · prerequisite — trail 是不重複邊的 walk：對所有 0≤i<j≤k−1，{v_i,v_{i+1}}≠{v_j,v_{j+1}}。
• unordered_pair_eq · prerequisite — 無序對相等：{p,q}={r,s} 當且僅當 (p=r 且 q=s) 或 (p=s 且 q=r)。
• inj_size_le · prerequisite — 若有限集合 X 到有限集合 Y 有單射，則 |X|≤|Y|（鴿籠原理）。
• L_path_trail · lemma — 在簡單圖中，每個 simple path 都不重複邊，因此是 trail。

逐步主鏈

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

G\ \text{simple, loop-free};\ \sum_{v}\deg v=2+3+2+4+1=12=2|E|

W=(v_i)_{i=0}^{k}

W\ \text{walk}\iff\forall i\ (0\le i\le k-1):\ \{v_i,v_{i+1}\}\in E;\ \ \text{length}=k;\ \ \text{simple path}\iff\text{walk}\land(i\neq j\Rightarrow v_i\neq v_j)

W_1=(0,1,2,3,4)

\{0,1\},\{1,2\},\{2,3\},\{3,4\}\in E\ \Rightarrow\ W_1\ \text{walk}

W_1\ \text{has}\ 5\ \text{entries}

\operatorname{len}(W_1)=5-1=4

W_1\ \text{walk},\ 0,1,2,3,4\ \text{pairwise distinct}

W_1\ \text{simple path}

W_2=(0,1,3,1,2)

\{0,1\},\{1,3\},\{3,1\},\{1,2\}\in E\ \Rightarrow\ W_2\ \text{walk},\ \operatorname{len}(W_2)=4

v_1=1=v_3\ \text{in}\ W_2

W_2\ \text{walk but not a simple path}

W_3=(0,2,3)

\{0,2\}\notin E\ \Rightarrow\ W_3\ \text{not a walk}

W_4=(2,3,0,1,3,4)

\{2,3\},\{3,0\},\{0,1\},\{1,3\},\{3,4\}\in E,\ \text{pairwise distinct}\ \Rightarrow\ W_4\ \text{trail},\ \operatorname{len}(W_4)=5

v_1=3=v_4\ \text{in}\ W_4

W_4\ \text{trail but not a simple path}

W=(v_i)_{i=0}^{k}\ \text{simple path}

\{v_i,v_{i+1}\}\neq\{v_j,v_{j+1}\}\ \ (0\le i<j\le k-1),\ \text{so}\ W\ \text{is a trail}

W=(v_i)_{i=0}^{k}\ \text{simple path in}\ G,\ |V|=5

k+1\le 5,\ \text{so}\ \operatorname{len}(W)=k\le 4

W_5=(4),\ k=0

W_5\ \text{simple path of length}\ 0;\ \ ()\ \text{not a walk}

W_6=(1,1)

\{1,1\}\notin E\ \Rightarrow\ W_6\ \text{not a walk}

\text{S05},\ \text{S07},\ \text{S08},\ \text{S10},\ \text{S13},\ \text{S14}

W_1,W_5\ \text{simple paths};\ W_2\ \text{walk only};\ W_4\ \text{trail, not simple path};\ W_3,W_6,()\ \text{not walks}

局部子步與引理

\{v_i,v_{i+1}\}=\{v_j,v_{j+1}\},\ 0\le i<j\le k-1

v_i=v_j\ \lor\ v_i=v_{j+1}

v_i=v_j\ \lor\ v_i=v_{j+1},\ \ i<j<j+1

\bot,\ \text{hence no two edges of}\ W\ \text{coincide}

逐步反向審查

• S15 · sufficient_goal_reduction · S05, S07, S08, S10, S11, S12, S13, S14, and_intro_elim — 目標 G 是所有判定與兩個一般性質的合取；足夠條件 H 是各步的結論，H⇒G 由合取引入，每一項都由已知正向證得，沒有把 G 當作前提。
• S14 · premise_audit · S01, graph_basics, quantifier_negation — 依賴「簡單圖的邊是相異頂點的無序對」；若另換允許 loop 的模型，仍須實際含有頂點 1 的 loop 才會使 W₆ 成為長度 1 的 walk；只說允許 loop 不保證結論改變。即使該 loop 存在，W₆ 仍因頂點重複而非 simple path。該模型不在此 MKO 範圍內。
• S13 · premise_audit · mko_walk_def — 空真成立是因為沒有任何 i 滿足 0≤i≤k−1=−1；空序列的排除是協定規定，不是由定義推出。
• S12 · premise_audit · inj_size_le, S02 — 需要項兩兩相異（單射）；對一般 walk 不成立，W₂ 與 W₄ 都可重複頂點。長度 ≤4 只是必要條件，不推出是 simple path（N4、N5）。
• S11.2 · premise_audit · S11.1, contradiction, case_analysis — 兩個情形涵蓋 S11.1 的所有可能；矛盾只用到 simple path 的定義。
• S11.1 · premise_audit · unordered_pair_eq, and_intro_elim — 只取每個情形的第一個合取項，不宣稱反向。
• S11 · premise_audit · L_path_trail, trail_def — 只宣稱 simple path ⇒ trail；反向由 W₄ 否定。
• S10 · premise_audit · S09, quantifier_negation — 一組見證 (i,j)=(1,4) 足以否定頂點兩兩相異；S12 的長度上界給出獨立的交叉核對。
• S09 · premise_audit · S02, trail_def, unordered_pair_eq — trail 需要 walk 加上邊不重複；這裡兩者都已逐一核對（N3 核長度）。
• S08 · premise_audit · G1, quantifier_negation — 「{0,2}∉E」依 G1 的「沒有其他邊」成立；若邊集合不完整，就不能判定不相鄰，這正是假設 a1 要求完整邊集的原因。
• S07 · premise_audit · S06, quantifier_negation — 否定「對所有 i≠j，v_i≠v_j」只需一組見證 (i,j)=(1,3)。
• S06 · premise_audit · S02, unordered_pair_eq, and_intro_elim — 因圖是無向的，{3,1}={1,3}（無序對相等）；若是有向圖，這一步要另外核對方向。
• S05 · premise_audit · S03, mko_walk_def — simple path 需要兩個條件：walk（S03）與項不重複；只有項不重複而不是 walk 不夠（見 S08）。
• S04 · inverse_equivalence · mko_walk_def, numeric_evaluation — 反向：長度 4 加一得項數 5；兩種說法描述同一個序列（N2）。
• S03 · premise_audit · S02, G1, and_intro_elim — 必須核對每一個連續對，不能只核第一對或最後一對；這一步四對都已核對。
• S02 · premise_audit · mko_walk_def, def_unfold — 只展開定義，不推出新事實；之後每個判定都回到這三個條件。
• S01 · premise_audit · G1, graph_basics — 只確認資格與做一致性核對（N1）；握手等式成立不能證明邊清單正確，只能排除部分抄寫錯誤。

錯誤控制與反例

頂點清單不一定是 walk

MKO 指出的誤解之一是把任何頂點清單當成 walk。W₃=(0,2,3) 的三個頂點都在 V 中且彼此相異，但 {0,2} 不是邊，所以不是 walk。判定必須逐一核對每個連續對（S03、S08），而且需要完整的邊集合才能判定「不相鄰」。

長度是邊數，不是頂點數

W₁ 有 5 個頂點，長度是 4。W₂ 有 5 項但只有 4 個不同頂點、3 條不同的邊，長度仍是 4：長度數的是連續對（走過的邊，重複也算），等於項數減一。

trail 不一定是 simple path

W₄ 不重複任何邊，卻兩次經過頂點 3。simple path 禁止的是重複頂點；不重複邊只是較弱的 trail 條件。引理 L_path_trail 只給出 simple path ⇒ trail 這一個方向。

• (0,2,3) 的頂點都在 V 中且不重複，所以它是 simple path → reject — {0,2}∉E，所以它根本不是 walk。
• W₁=(0,1,2,3,4) 有 5 個頂點，所以長度是 5 → reject — 長度是連續對的個數 5−1=4。
• W₄ 沒有重複的邊，所以是 simple path → reject — 頂點 3 出現在索引 1 與索引 4 的項；而且長度 5 超過 simple path 的上界 4。
• (1,1) 是在頂點 1 停留一步、長度為 1 的 walk → reject — {1,1} 不是兩個相異頂點的無序對，無 loop 簡單圖中不是邊。

結論與限制

在 G 中：W₁=(0,1,2,3,4) 是長度 4 的 simple path；W₂=(0,1,3,1,2) 是長度 4 的 walk 但不是 simple path；W₃=(0,2,3) 因 {0,2}∉E 不是 walk；W₄=(2,3,0,1,3,4) 是長度 5 的 trail，但頂點 3 重複，不是 simple path；W₅=(4) 是長度 0 的 simple path；W₆=(1,1) 與空序列不是 walk。每個 simple path 都是 trail，反之不然；本圖中 simple path 的長度至多為 4。

• 本稿以完整邊清單逐對核對；對更大的圖，同樣的判定可寫成演算法，但本稿不分析其複雜度。
• cycle 與連通分量不在本稿範圍內，trail 只用作對照。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 49f77d500fdd6a9edd41755d563203dc6463ebe4857c93350c07bbfd67d26ec3
• original source SHA-256: 658afc79124d38166f5b5ff1eb4fae1b1b76dccfe69d963b6d261be4216f8d9c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）