# 數列：由初始條件與遞迴確定通項，以及索引與有限前綴的陷阱

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

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

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



## 目標與範圍

設實數數列 a:ℕ→ℝ（ℕ 含 0）滿足 a₀=5、a_{n+1}=a_n+3。(1) 證明恰有一個這樣的數列，且 a_n=5+3n；(2) 計算 a₀ 到 a₄ 與 a₁₀，說明 a₀ 是起始項、a₁₀ 是從 1 數起的第 11 個值；(3) 寫出長度 L=4 的有限數列及其索引集合；(4) 說明前綴 5、8、11 不能唯一決定數列。

在 MKO 的範圍內：實數數列是 ℕ→ℝ 的函數，ℕ 含 0（假設 a1）；有限數列明示長度 L 與索引集合，遞迴附初始條件（假設 a2），並採用 MKO 所用的形式 a₀=u、a_{n+1}=a_n+d（u=5、d=3）。存在性以寫出通項來證明，不需引用一般遞迴定理。不處理極限、單調性或級數；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- nat_induction
- function_def
- distributive
- add_assoc
- eq_replace
- numeric_evaluation


- G1 — ℕ 包含 0；實數數列是函數 a:ℕ→ℝ，a_n 表示 a(n)，a₀ 稱為起始項（MKO 假設 a1）。
- G2 — 遞迴與初始條件：a₀=5，且對每個 n∈ℕ，a_{n+1}=a_n+3。
- G3 — 有限數列：長度 L 是非負整數，索引集合為 {n∈ℕ ∣ n<L}，只有這些 n 可用（MKO 假設 a2）。


- a_n — 數列 a 在索引 n 的值 a(n)
- s_n — 候選通項 5+3n
- c_n — 與 a 有相同前綴的另一個數列
- L — 有限數列的長度
- \mathbb{N} — 含 0 的自然數





## 規則與來源


- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- add_zero · prerequisite — 加法單位元：u+0=u。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- mko_seq_def · cited — 在 ℕ 包含 0 的慣例下，實數數列為函數 a:ℕ→ℝ，第 n 項記為 a(n) 或 a_n。有限數列則明示長度 L 及索引集合（從 0 到 L−1 的整數）。 · mko-sequence
- L_unique · lemma — 若數列 a:ℕ→ℝ 滿足 a₀=5 且對每個 n 有 a_{n+1}=a_n+3，則對每個 n∈ℕ，a_n=5+3n。





## 逐步主鏈

S01 · definition操作前

(a_n)

操作後

a:\mathbb{N}\to\mathbb{R},\ a_0=5,\ a_{n+1}=a_n+3

條件：0\in\mathbb{N}

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

葉節點依據：mko_seq_def + function_def

依 MKO，數列就是以 ℕ 為定義域的函數；索引 n 是輸入，a_n 是輸出。題目給的是遞迴式加初始條件，它約束 a 的值，但還沒有說明這樣的 a 存在或唯一，這正是 S02 到 S06 要證明的。



S02 · definition操作前

n\in\mathbb{N}

操作後

s:\mathbb{N}\to\mathbb{R},\ s_n=5+3n

條件：無

規則：def_intro · 依賴：S01

葉節點依據：def_intro + function_def

提出候選數列 s_n=5+3n。對每個自然數 n，5+3n 是唯一確定的實數，所以 s 是 ℕ→ℝ 的函數，也就是一個數列。



S03 · equivalent操作前

s_0

操作後

s_0=5+3\cdot 0=5

條件：無

規則：eq_replace · 依賴：S02

葉節點依據：eq_replace + mul_zero + add_zero

代入 n=0：3·0=0（乘以零），5+0=5（加法單位元），所以 s₀=5，符合初始條件。



S04 · equivalent操作前

s_{n+1}=5+3(n+1)

操作後

s_{n+1}=(5+3n)+3=s_n+3

條件：無

規則：distributive · 依賴：S02

葉節點依據：distributive + add_assoc + mul_one

對任意 n：5+3(n+1)=5+(3n+3)（分配律）=(5+3n)+3（結合律）=s_n+3。所以 s 滿足遞迴，而且是對每個 n 都成立的恆等式。



S05 · implies操作前

s_0=5,\ s_{n+1}=s_n+3

操作後

\exists\ a:\mathbb{N}\to\mathbb{R}\ \text{with}\ a_0=5,\ a_{n+1}=a_n+3

條件：無

規則：exists_intro · 依賴：S02, S03, S04

葉節點依據：exists_intro + and_intro_elim

s 是一個數列（S02），並滿足初始條件（S03）與遞迴（S04），所以至少存在一個滿足 G2 的數列。存在性是直接寫出例子得到的。



S06 · theorem_application操作前

a_0=5,\ a_{n+1}=a_n+3

操作後

a_n=5+3n\ \text{for every}\ n\in\mathbb{N},\ \text{so}\ a=s

條件：無

規則：L_unique · 依賴：S01, S02, L_unique, function_def

葉節點依據：L_unique + function_def + nat_induction

依引理 L_unique（在 S06.1、S06.2 以歸納法證明），任何滿足 G2 的數列在每個索引都等於 s；兩者定義域都是 ℕ、對應域都是 ℝ，依 function_def 得 a=s。配合 S05，恰有一個這樣的數列。



S07 · implies操作前

a_n=5+3n

操作後

a_0=5,\ a_1=8,\ a_2=11,\ a_3=14,\ a_4=17,\ a_{10}=35

條件：無

規則：forall_elim · 依賴：S06

葉節點依據：forall_elim + numeric_evaluation

把 n=0、1、2、3、4、10 代入通項：5、8、11、14、17、35。起始項是 a₀=5（索引 0），不是 a₁。



S08 · implies操作前

a_{10}=35

操作後

a_{10}\ \text{is the 11th value};\ b_k=a_{k-1}\ (k\geq 1)\ \text{gives}\ b_{10}=a_9=32

條件：無

規則：def_unfold · 依賴：S07, G1

葉節點依據：def_unfold + numeric_evaluation

索引 0 到 10 共有 11 個，所以 a₁₀ 是從 1 數起的第 11 個值。若有人改用從 1 起算的記號 b_k=a_{k−1}（k≥1，b₁=a₀=5），他的「第 10 項」b₁₀=a₉=5+27=32，與 a₁₀=35 不同。說「第 10 項」時必須說明索引從 0 還是從 1 起算。



S09 · definition操作前

L=4

操作後

(a_0,a_1,a_2,a_3)=(5,8,11,14),\ \ \text{indices}\ \{0,1,2,3\}

條件：0\leq n<4

規則：mko_seq_def · 依賴：G3, S07, mko_seq_def

葉節點依據：mko_seq_def + set_builder

長度 L=4 的有限數列的索引集合是 {n∈ℕ ∣ n<4}={0,1,2,3}，它是函數 {0,1,2,3}→ℝ，值為 5、8、11、14。索引 4 不允許（4<4 不成立），所以這個有限數列沒有 a₄，雖然無限數列有 a₄=17。



S10 · implies操作前

c_n=5+3n+n(n-1)(n-2)

操作後

c_0=5,\ c_1=8,\ c_2=11

條件：無

規則：mul_zero · 依賴：S07

葉節點依據：mul_zero + add_zero + numeric_evaluation

考慮另一個數列 c_n=5+3n+n(n−1)(n−2)。當 n=0、1、2 時，乘積 n(n−1)(n−2) 中有一個因數是 0，所以乘積為 0，c_n=5+3n。因此 c 與 a 的前綴 5、8、11 完全相同。



S11 · implies操作前

c_3

操作後

c_3=5+9+3\cdot 2\cdot 1=20\neq 14=a_3,\ \text{so}\ c\neq a

條件：無

規則：function_def · 依賴：S07, S10, function_def

葉節點依據：function_def + numeric_evaluation

c₃=5+3·3+3·2·1=14+6=20，而 a₃=14。兩個數列在索引 3 的值不同，依 function_def，c≠a。所以前綴 5、8、11 不能唯一決定數列：至少有兩個不同的數列以它開頭。



S12 · implies操作前

c_3-c_2

操作後

c_3-c_2=20-11=9\neq 3

條件：無

規則：contrapositive · 依賴：S06, S10, S11

葉節點依據：contrapositive + numeric_evaluation

c 滿足 c₀=5，但在 n=2 不滿足遞迴：c₃−c₂=9≠3。這與 S06 一致：滿足初始條件與遞迴的數列只有 a。能唯一決定數列的是規則加初始條件，而不是有限個前幾項。



S13 · implies操作前

S05\ \text{to}\ S09,\ S11

操作後

a_n=5+3n\ \text{unique};\ a_{10}=35;\ (5,8,11,14)\ \text{on}\ \{0,1,2,3\};\ \text{prefix not determining}

條件：無

規則：and_intro_elim · 依賴：S05, S06, S07, S08, S09, S11

葉節點依據：and_intro_elim

目標 (1) 由 S05、S06，(2) 由 S07、S08，(3) 由 S09，(4) 由 S10、S11 完成。







## 局部子步與引理

S06.1 · induction_base操作前

a_0=5

操作後

a_0=s_0

條件：無

規則：eq_refl_symm_trans · 依賴：S02, S03

葉節點依據：eq_refl_symm_trans

歸納基礎：a₀=5（G2 的初始條件），s₀=5（S03），所以 a₀=s₀。



S06.2 · induction_step操作前

a_n=s_n

操作後

a_{n+1}=a_n+3=s_n+3=s_{n+1}

條件：n\in\mathbb{N}\ \text{arbitrary}

規則：eq_replace · 依賴：S04, nat_induction

葉節點依據：eq_replace + nat_induction + forall_elim

設某個 n 有 a_n=s_n。則 a_{n+1}=a_n+3（a 的遞迴）=s_n+3（以歸納假設代換）=s_{n+1}（S04）。依歸納原理（n₀=0），S06.1 與 S06.2 證得引理 L_unique。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S11, and_intro_elim — 目標 G：(1) 到 (4)。足夠條件 H：所列各步成立；H⇒G 由合取引入。H 由定義、歸納與精確計算正向證成，沒有把 G 當作前提。
- S12 · premise_audit · S06, S11, contrapositive — 由 S06 的逆否：c≠a 推出 c 不滿足 G2；這裡也直接找到失敗的位置 n=2。
- S11 · premise_audit · S10, function_def, numeric_evaluation — 一個不同的索引就足以說明兩個數列不同（N10、N11）。
- S10 · premise_audit · mul_zero, S07 — 只對 n=0、1、2 宣稱 c_n=a_n；N9 是這三點的有限核對，恰好涵蓋此步的全部主張。
- S09 · premise_audit · G3, mko_seq_def — 索引集合由 L 決定，從 0 到 L−1，共 L 個；常見錯誤是寫成 1 到 4 或 0 到 4。
- S08 · premise_audit · S07, G1, def_unfold — 兩種慣例描述同一串數，只是標籤平移 1；本稿採 MKO 的從 0 起算。
- S07 · premise_audit · S06, forall_elim, numeric_evaluation — 精確整數計算，可獨立重算（N3 到 N5）。
- S06.2 · premise_audit · S04, eq_replace, nat_induction — 只用同一個 n 的歸納假設；不宣稱反向。
- S06.1 · premise_audit · S03, eq_refl_symm_trans — 基礎只用到初始條件；它不能由遞迴本身推出。
- S06 · premise_audit · L_unique, function_def, S05 — 唯一性需要初始條件與遞迴兩者；只有遞迴而沒有 a₀，例如 a₀=0 也滿足遞迴，得到不同的數列。
- S05 · premise_audit · S03, S04, exists_intro — 這只是存在；「只有一個」在 S06 證明。
- S04 · inverse_equivalence · distributive, add_assoc — 所用的是對所有 n 成立的恆等式，雙向成立；N2 以一次多項式恆等式核對。
- S03 · inverse_equivalence · mul_zero, add_zero, eq_replace — 兩邊是同一個數，等式雙向成立（N1）。
- S02 · premise_audit · def_intro, function_def — 此步只引入名稱；s 是否滿足條件在 S03、S04 核對。
- S01 · premise_audit · G1, G2, mko_seq_def — 此步只寫出定義與條件，不推出新事實。





## 錯誤控制與反例

索引從 0 還是從 1 起算要說清楚MKO 指出的第一個誤解是混淆從 0 或 1 起始的索引。本稿 a₀=5 是起始項，a₁₀=35；若改用 b_k=a_{k−1} 從 1 起算，「第 10 項」是 b₁₀=32。同一串數，兩種標籤給出不同的「第 10 項」，所以必須先說明慣例。

有限前綴不能唯一決定數列MKO 指出的第二個誤解是僅憑一段前綴宣稱找出了唯一數列。5、8、11 之後，a 給 14，c 給 20；事實上任何有限前綴後面都可以接任意的值。能唯一決定數列的是明示的規則（通項或遞迴加初始條件），S06 正是用規則證明唯一性。

有限數列的索引只到 L−1長度 L=4 的有限數列索引是 0、1、2、3，共 4 個。寫成 1 到 4 會丟掉 a₀ 並多出不存在的 a₄；寫成 0 到 4 則有 5 個索引，長度變成 5。a₄=17 屬於無限數列，不屬於這個有限數列。


- 由 5、8、11 可知下一項必定是 14 → reject — c_n=5+3n+n(n−1)(n−2) 有相同前綴，但 c₃=20。
- 在從 1 起算的記號下，第 10 項是 35 → reject — b₁₀=a₉=32；35 是 a₁₀，是第 11 個值。
- 長度 4 的有限數列 (5,8,11,14) 有一項 a₄=17 → reject — 索引只有 0、1、2、3；4<4 不成立。
- 有限數列 (5,8) 與 (8,5) 相同，因為它們的值集合都是 {5,8} → reject — 數列是函數；在索引 0 的值 5≠8。索引次序是資料的一部分。
- c 也滿足 c₀=5 與 c_{n+1}=c_n+3 → reject — c₃−c₂=9≠3。





## 結論與限制

滿足 a₀=5、a_{n+1}=a_n+3 的數列恰有一個，即 a_n=5+3n；a₀ 到 a₄ 為 5、8、11、14、17，a₁₀=35（從 1 數起的第 11 個值；從 1 起算的記號下「第 10 項」是 32）。長度 4 的有限數列是 (5,8,11,14)，索引為 {0,1,2,3}。前綴 5、8、11 也是 c_n=5+3n+n(n−1)(n−2) 的前綴，而 c₃=20≠14，所以前綴不能唯一決定數列。


- N9 是 n=0、1、2 三點的有限核對，恰好是 S10 所宣稱的範圍；N2 是一次多項式恆等式的格點核對，對一次多項式是完整的判定。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: c85cb9781dafa2d70a69996e1317fce43de676cfa862621d70e5f98c2de30736
- original source SHA-256: c85cb9781dafa2d70a69996e1317fce43de676cfa862621d70e5f98c2de30736
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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