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

目標與範圍

在固定時間步、常數因子 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。

逐步主鏈

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

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

r^n

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

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

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

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

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

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}

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

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

y_n=x_0\,r^n

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

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_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

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

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

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}

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}

\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

局部子步與引理

n=0

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

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}

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

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

12=r\cdot 8

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

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

x_3=27\neq 26=d_3

逐步反向審查

• 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）。兩者之間需要明確的換算，不能直接互換。

歸納步要用同一個 r

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