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

目標與範圍

設實數數列 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。

逐步主鏈

(a_n)

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

n\in\mathbb{N}

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

s_0

s_0=5+3\cdot 0=5

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

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

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

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

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

a_n=5+3n

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

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

L=4

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

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

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

c_3

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

c_3-c_2

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

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}

局部子步與引理

a_0=5

a_0=s_0

a_n=s_n

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

逐步反向審查

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