# 離散指數成長模型：由 x_(n+1)=r·x_n 歸納證明 x_n=x_0·r^n

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

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

derivation-mko-discrete-exponential-growth-01 · production-20261019-adopted-96



## 目標與範圍

在固定時間步、常數因子 r≥0 的模型 x_(n+1)=r·x_n 中，以數學歸納法證明對每個自然數 n 有 x_n=x_0·r^n，並說明遞迴式與閉式描述同一數列；以 x_0=8、r=3/2 計算 x_1 到 x_4 並與閉式比對；說明 r>1、r=1、0≤r<1 與 x_0=0 的行為；判定資料 8、12、18、26 不符合任何以 x_0=8 開始的固定因子模型；並說明每步因子 3/2 不是連續成長率 1/2。

只在指定模型中作代數推導（MKO 假設 a1、a2）：初值與因子為精確有理數，r 在整段期間不變。結論是模型內的代數結果，不是資料符合模型的證明，也不是生物族群的實測預測。S12 只用指數函數的級數下界來說明離散因子與連續率不同，不建立連續時間模型。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- nat_induction
- eq_congruence
- mul_assoc
- mul_comm
- forall_elim


- G1 — 時間步固定，n 從 0 起算，因子 r 在整段期間保持不變（MKO 假設 a1）。
- G2 — 模型：對每個自然數 n，x_(n+1)=r·x_n；x_0 與 r 為精確有理數，r≥0（假設 a2）。
- G3 — 主例：x_0=8，r=3/2。對照例：x_0=8，r=1/2；以及 x_0=0。
- G4 — 給定的觀測資料：d_0=8，d_1=12，d_2=18，d_3=26。


- x_n — 第 n 個時間步的量
- r — 每步的常數因子，r≥0
- x_0 — 初值
- r^n — 自然數次冪，r^0=1，r^(n+1)=r^n·r
- d_0,d_1,d_2,d_3 — 給定的觀測資料





## 規則與來源


- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_exp_model · cited — 固定一個時間步與非負常數因子 r，離散指數模型由 x_(n+1)=r x_n 定義。給初值 x_0，反覆代入或歸納得到 x_n=x_0 r^n；這是指定模型的代數結果，不是資料自動符合模型的證明。 · mko-discrete-exponential-growth
- mko_exp_cases · cited — 獨立來源追加式勘誤（使用者已採用於本地修訂；未合併或發布）：r>1 是每步乘以大於 1 的固定因子，不一定是加倍；非零初值的絕對值增加，正初值的值增加而負初值的值減少。r=1 時數值不變；0<r<1 時非零數值的絕對值縮小；r=0 時第一步起為零。初值為零時全序列為零。原始引文與 canonical MKO 保留不動。 · mko-discrete-exponential-growth
- nat_power_def · prerequisite — 自然數次冪的遞迴定義：對任何有理數 r，r^0=1，r^(n+1)=r^n·r（因此 0^0=1 是此定義的一部分）。
- exp_lower_bound · prerequisite — 對 u≥0，eᵘ=Σ_(k≥0) uᵏ/k! 的每一項都非負，所以 eᵘ≥1+u+u²/2。
- L_closed_form · lemma — 在模型 G2 中，對每個自然數 n，x_n=x_0·r^n。





## 逐步主鏈

S01 · definition操作前

\text{fixed step, constant factor }r\ge 0

操作後

x_{n+1}=r\,x_n\ (n\in\mathbb{N}),\ x_0\ \text{given}

條件：r\ge 0

規則：mko_exp_model · 依賴：G1, G2

葉節點依據：mko_exp_model + def_intro

依 MKO 寫出模型：每一步把目前的量乘以同一個非負因子 r。G1 要求時間步固定、r 不隨時間改變；這是模型的假設，不是由任何資料推出的。



S02 · definition操作前

r^n

操作後

r^0=1,\ r^{n+1}=r^n\cdot r

條件：無

規則：nat_power_def · 依賴：nat_power_def

葉節點依據：nat_power_def + def_intro

把次冪的意義說清楚：r^n 是 n 個 r 相乘，正式地以遞迴定義。這個定義對 r=0 也適用，所以 0^0=1，閉式在 r=0 時也有意義。



S03 · implies操作前

x_{n+1}=r\,x_n,\ x_0

操作後

\forall n\in\mathbb{N}:\ x_n=x_0\,r^n

條件：無

規則：L_closed_form · 依賴：S01, S02, L_closed_form

葉節點依據：nat_induction + nat_power_def + mul_assoc + mul_comm

依引理 L_closed_form（在 S03.1 到 S03.3 以數學歸納法證明），遞迴式推出閉式，對所有 n 成立，而不是只對算過的幾項成立。



S04 · implies操作前

\forall n:\ x_n=x_0\,r^n

操作後

x_n=8\left(\tfrac{3}{2}\right)^n

條件：x_0=8,\ r=\tfrac{3}{2}\ge 0

規則：forall_elim · 依賴：S03, G3

葉節點依據：forall_elim

引理對任意 x_0 與 r≥0 成立；代入主例 x_0=8、r=3/2 得 x_n=8·(3/2)^n。



S05 · implies操作前

x_0=8,\ x_{n+1}=\tfrac{3}{2}x_n

操作後

x_1=12,\ x_2=18,\ x_3=27,\ x_4=\tfrac{81}{2}

條件：無

規則：numeric_evaluation · 依賴：G2, G3

葉節點依據：numeric_evaluation + eq_replace

依遞迴式逐步計算：8·3/2=12，12·3/2=18，18·3/2=27，27·3/2=81/2。



S06 · equivalent操作前

8\left(\tfrac{3}{2}\right)^4

操作後

8\cdot\tfrac{81}{16}=\tfrac{81}{2}=x_4

條件：無

規則：power_laws · 依賴：S04, S05

葉節點依據：power_laws + frac_rules + numeric_evaluation

閉式在 n=4 的值：(3/2)^4=81/16，8·81/16=81/2，與 S05 的遞迴計算一致。這是對 S03 的數值交叉核對，不是它的證明。



S07 · equivalent操作前

y_n=x_0\,r^n

操作後

y_0=x_0,\ y_{n+1}=r\,y_n

條件：無

規則：nat_power_def · 依賴：S03, S02

葉節點依據：nat_power_def + mul_assoc + mul_comm + iff_intro

反方向：閉式數列 y_n=x_0·r^n 滿足遞迴式與同一初值，因為 y_0=x_0·1=x_0，且 y_(n+1)=x_0·r^n·r=r·y_n。配合 S03（滿足遞迴與初值的數列必等於閉式），遞迴加初值與閉式描述的是同一個數列，雙向成立，這正是 MKO 第二段說的等價。



S08 · implies操作前

x_{n+1}-x_n=(r-1)x_n,\ r=\tfrac{3}{2}

操作後

x_{n+1}-x_n=\tfrac{1}{2}x_n>0

條件：x_n=8(\tfrac{3}{2})^n>0

規則：mko_exp_cases · 依賴：S04, mko_exp_cases

葉節點依據：distributive + order_basics + mko_exp_cases

x_(n+1)−x_n=r·x_n−x_n=(r−1)x_n。主例 r−1=1/2，而 x_n=8·(3/2)^n 是正數的乘積，所以 x_n>0，於是每步嚴格增加，且增量本身與 x_n 成正比：這就是 r>1 的「每步按因子成長」。



S09 · implies操作前

x_0=8,\ r=\tfrac{1}{2}

操作後

x_n=8\left(\tfrac{1}{2}\right)^n:\ 8,4,2,1,\tfrac{1}{2};\ x_{n+1}-x_n=-\tfrac{1}{2}x_n<0

條件：0\le r<1

規則：mko_exp_cases · 依賴：S03, G3, mko_exp_cases

葉節點依據：L_closed_form + order_basics + mko_exp_cases

對照例 r=1/2：依 L_closed_form，x_n=8·(1/2)^n，前五項為 8、4、2、1、1/2；x_(n+1)−x_n=(1/2−1)x_n=−x_n/2<0，每步縮為一半。這是 0≤r<1 的縮放情形。 一般分類不另加 x0≥0 假設：由閉式，r>0 時 x_n 與 x0 同號，且 x_(n+1)−x_n=(r−1)x_n。故 r>1 且 x0>0 時嚴格遞增、x0<0 時嚴格遞減，非零初值的絕對值每步乘 r 而增大；0<r<1 時絕對值縮小，正初值遞減、負初值遞增；r=0 時 x1 及以後全為0。r=1 與 x0=0 的常數情形見 S10。



S10 · implies操作前

r=1\ \text{or}\ x_0=0

操作後

r=1:\ x_n=x_0;\ \ x_0=0:\ x_n=0\cdot r^n=0

條件：無

規則：mko_exp_cases · 依賴：S03, mko_exp_cases

葉節點依據：L_closed_form + mul_zero + mul_one

r=1 時 1^n=1，所以 x_n=x_0，數列不變。x_0=0 時，對任何 r≥0（包括 r=0，依 0^0=1 的定義）x_n=0·r^n=0，序列全為零。



S11 · implies操作前

d=(8,12,18,26),\ \text{fixed-}r\ \text{model with }x_0=8

操作後

r=\tfrac{3}{2}\ \text{forced},\ x_3=27\neq 26:\ \text{no fixed-}r\ \text{model fits}

條件：d_0=8\neq 0

規則：contradiction · 依賴：G4, S03

葉節點依據：contradiction + mul_inverse_nonzero + L_closed_form

假設某個固定因子模型 x_(n+1)=r·x_n、x_0=8 與四個資料都相符。由 x_1=12=r·8 且 8≠0 得 r=12/8=3/2（S11.1）。依 L_closed_form，模型給出 x_3=8·(3/2)^3=27，但 d_3=26，矛盾（S11.2）。所以沒有任何固定 r 的模型同時符合四個資料。前三個資料的比值都是 3/2，看起來像固定因子，但不足以推出第四期。



S12 · implies操作前

r=\tfrac{3}{2}\ \text{per step},\ \text{continuous }x(t)=x_0e^{kt}

操作後

e^{k}=\tfrac{3}{2}\ \text{needed};\ e^{1/2}\ge\tfrac{13}{8}>\tfrac{3}{2},\ \text{so }k\neq\tfrac{1}{2}

條件：u=\tfrac{1}{2}\ge 0

規則：exp_lower_bound · 依賴：G1, exp_lower_bound

葉節點依據：exp_lower_bound + order_basics

每步因子 3/2 表示每步增加 50%。對本題非零初值 x_0=8，若連續時間的 x(t)=x_0·e^(kt) 在整數時間與模型一致，由第 1 步可消去 x_0，得到 e^k=3/2。若 x_0=0，兩者都是零軌跡，不能由軌跡一致推定 k；以下比較的是非零軌跡所需的因子一致。把 50% 直接當作連續成長率 k=1/2 是錯的：依級數下界 e^(1/2)≥1+1/2+1/8=13/8，而 13/8>3/2，所以 e^(1/2)≠3/2。離散因子與連續成長率是不同的量，本稿不建立連續模型。



S13 · implies操作前

\text{proved facts}

操作後

x_n=x_0r^n\ \forall n;\ x_4=\tfrac{81}{2};\ \text{data }(8,12,18,26)\ \text{fit no fixed }r

條件：無

規則：and_intro_elim · 依賴：S03, S06, S07, S08, S09, S10, S11, S12

葉節點依據：and_intro_elim

合併結論：模型中 x_n=x_0·r^n 對所有 n 成立且與遞迴式等價；主例 x_4=81/2；非零初值在 r>1 時絕對值增大、0<r<1 時絕對值縮小，數值單調方向另依初值正負；r=0 時從第一步起為0，r=1 不變，x_0=0 全為零；資料 8、12、18、26 不符合固定因子模型；每步因子不是連續率。







## 局部子步與引理

S03.1 · induction_base操作前

n=0

操作後

x_0=x_0\cdot 1=x_0\,r^0

條件：無

規則：nat_induction · 依賴：S02

葉節點依據：nat_power_def + mul_one

基底：令 P(n) 為 x_n=x_0·r^n。因 r^0=1 且 x_0·1=x_0，P(0) 成立。



S03.2 · induction_step操作前

x_n=x_0\,r^n

操作後

x_{n+1}=r\,x_n=r\,(x_0\,r^n)=x_0\,(r^n\cdot r)=x_0\,r^{n+1}

條件：無

規則：eq_replace · 依賴：S01, S02

葉節點依據：eq_replace + mul_assoc + mul_comm + nat_power_def

歸納步：假設 P(n)。由遞迴式 x_(n+1)=r·x_n，把 x_n 換成 x_0·r^n，再用乘法交換律與結合律重排為 x_0·(r^n·r)，依次冪定義即 x_0·r^(n+1)，所以 P(n+1) 成立。



S03.3 · implies操作前

P(0),\ \forall n\,(P(n)\Rightarrow P(n+1))

操作後

\forall n\in\mathbb{N}:\ x_n=x_0\,r^n

條件：無

規則：nat_induction · 依賴：S03.1, S03.2

葉節點依據：nat_induction

依數學歸納原理，P(n) 對所有自然數 n 成立。S03.1 到 S03.3 合起來證得引理 L_closed_form。



S11.1 · equivalent操作前

12=r\cdot 8

操作後

r=\tfrac{12}{8}=\tfrac{3}{2}

條件：8\neq 0

規則：mul_inverse_nonzero · 依賴：G4, G2

葉節點依據：mul_inverse_nonzero + eq_congruence + frac_rules

兩邊同乘 1/8（因 8≠0）：r=12/8=3/2。



S11.2 · implies操作前

x_3=8\left(\tfrac{3}{2}\right)^3

操作後

x_3=27\neq 26=d_3

條件：無

規則：numeric_evaluation · 依賴：S11.1, S03, G4

葉節點依據：numeric_evaluation + power_laws

8·27/8=27，而 d_3=26；兩數不等，與「模型符合資料」的假設矛盾。另外 d_3/d_2=26/18=13/9≠3/2，同樣顯示第三步的比值不同。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S03, S07, S08, S09, S10, S11, S12, and_intro_elim — 目標 G：本稿目標的各項判定。足夠條件 H：S03、S07 到 S12 各自已證（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。
- S12 · premise_audit · exp_lower_bound, order_basics — 只需要 e^u 的下界與有理數比較；此步只證明 k≠1/2，不計算 k 的值。
- S11.2 · premise_audit · numeric_evaluation, S11.1 — 精確計算；一個不符的資料點就足以否定固定因子模型。
- S11.1 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — 乘 1/8 與乘 8 互為反運算，雙向成立。
- S11 · premise_audit · S03, contradiction, mul_inverse_nonzero — 需要 d_0≠0 才能解出 r；結論只否定以 x_0=8 開始、r 固定的模型，不否定其他模型（例如 r 隨時間改變）。
- S10 · premise_audit · S03, mul_zero, mko_exp_cases — 兩個特例都是 L_closed_form 的代入；用到 1 的冪為 1 與乘以零為零。
- S09 · premise_audit · S03, mko_exp_cases, order_basics — 同一引理的正初值對照例 x0=8、r=1/2 對每個 n 都為正，不會有限步變0；一般符號分類另外由閉式和差分恆等式得出，r=0 則在第一步到0。
- S08 · premise_audit · S04, distributive, order_basics, mko_exp_cases — 需要 x_n>0；若 x_0=0，即使 r>1 也不會成長（S10）。
- S07 · inverse_equivalence · nat_power_def, S03, mul_assoc, mul_comm — 一個方向是 S03，另一個方向是此步的直接代入；兩個方向都有理由。
- S06 · inverse_equivalence · power_laws, frac_rules, numeric_evaluation — 精確有理數計算，雙向是同一個數。
- S05 · premise_audit · G2, numeric_evaluation — 每項只由前一項決定，精確有理數計算；不宣稱這四項本身證明了閉式。
- S04 · premise_audit · S03, forall_elim — 全稱消去只需要代入的值符合條件，r=3/2≥0。
- S03.3 · premise_audit · S03.1, S03.2, nat_induction — 兩個前提由 S03.1、S03.2 提供，n 在歸納步中任意。
- S03.2 · premise_audit · G2, eq_replace, mul_assoc, mul_comm, nat_power_def — 需要遞迴式對這個 n 成立、歸納假設，以及乘法的交換結合律；r 不能隨 n 改變，否則第一個等號不成立。
- S03.1 · premise_audit · nat_power_def, mul_one — 只用到 r^0=1 與乘法單位元；對 r=0 也成立。
- S03 · premise_audit · L_closed_form — 依賴該引理；引理只用到 G2 的遞迴式與次冪定義。
- S02 · premise_audit · nat_power_def — 只引入定義，不推出新事實。
- S01 · premise_audit · G1, G2, mko_exp_model — 此步只寫出模型，不推出新事實；之後所有結論都只在此模型中成立。





## 錯誤控制與反例

幾期成長不代表因子永遠固定MKO 指出的誤解之一：資料 8、12、18 的比值都是 3/2，但第四期是 26 而不是 27（S11）。L_closed_form 是「假設 r 固定」之下的代數結果；資料是否符合模型要另外核對，模型本身不證明適配。

離散因子不是連續成長率MKO 指出的另一個誤解：每步因子 3/2（增加 50%）若直接當作連續率 k=1/2，會得到每步因子 e^(1/2)≥13/8，比 3/2 大（S12）。兩者之間需要明確的換算，不能直接互換。

歸納步要用同一個 rS03.2 的第一個等號用的是 x_(n+1)=r·x_n，其中 r 與 n 無關。若因子隨時間改變（r_n），乘積是 r_0·r_1 一直乘到 r_(n−1)，不再是 r^n；把幾個數值代入閉式成立也不能取代歸納。


- 8、12、18 三期都乘 3/2，所以第四期必定是 27 → reject — 給定資料的第四期是 26；固定因子只是模型假設，資料不必遵守（S11）。
- 每步因子 3/2 等於連續成長率 1/2 → reject — e^(1/2)≥13/8>3/2，所以 k=1/2 給出的每步因子大於 3/2（S12）。
- 因為 n=0 到 4 時閉式都與遞迴相符，所以 x_n=8·(3/2)^n 對所有 n 成立已被證明 → reject — 有限個數值核對不能證明全稱命題；證明來自 S03 的歸納。
- r=3/2>1，所以不論初值為何數列都會成長 → reject — x_0=0 時 x_n=0 對所有 n 成立（S10）。





## 結論與限制

在模型 x_(n+1)=r·x_n（r≥0 固定）中，數學歸納法證明對所有 n 有 x_n=x_0·r^n，且閉式也滿足遞迴式，兩者描述同一數列。x_0=8、r=3/2 時 x_1 到 x_4 為 12、18、27、81/2，與閉式一致。非零初值在 r>1 時絕對值增大、0<r<1 時絕對值縮小；正初值的數值分別遞增、遞減，負初值的數值方向相反。r=0 時從第一步起為0，r=1 時不變，x_0=0 時全為零。資料 8、12、18、26 迫使 r=3/2，卻與預測 x_3=27 不符，所以不符合任何以 8 開始的固定因子模型。每步因子 3/2 不等於連續成長率 1/2，因為 e^(1/2)≥13/8>3/2。


- N6 是 n=0 到 20 的有限核對，只核對這些點；閉式對所有 n 的成立由 S03 的歸納證明。
- logistic 模型、時間變動因子與模型校準屬於 MKO 的 formal next。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: d241eac2e24aeedd4c822c1586a4997617fbe5ca988f7a3c508da4081980817f
- original source SHA-256: 31bb4abc1099f94cff294e388d438434f5734c98c44377638bc50ff98ef5d26e
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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