# 複利模型：本金 1000、每年 2%、三年的餘額與單利比較

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

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

derivation-mko-compound-interest-01 · production-20261019-adopted-96



## 目標與範圍

在期別為一年、每期利率 i=1/50（2%）、期間內無存提款與費用的模型中，以歸納證明 B_n=B_0(1+i)^n，算出 B_0=1000 時三年後的餘額 132651/125（即 1061.208）與利息；與單利 B_0(1+ni)=1060 比較，並以 Bernoulli 不等式證明複利餘額對每個 n 都不小於單利；說明期別混用與期間現金流如何使單一冪次公式失效。

只在 MKO 的模型假設下計算：期別、利率與期數單位一致，利率固定，無現金流、稅費或四捨五入，本金為非負精確有理數且 1+i>0（假設 a1、a2）。這些計算不是投資建議、報價或市場預測。不處理現值、名目與有效利率的換算或年金；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- nat_induction
- eq_replace
- order_basics
- square_nonneg
- distributive


- G1 — 期別為一年，利息在每年年末計入；每期利率 i 固定；模型期間內沒有存款、提款、費用、稅或四捨五入（MKO 假設 a1）。
- G2 — B_0=1000，i=1/50（每年 2%），期數 n=3；更新規則 B_(n+1)=(1+i)B_n（假設 a2：本金非負、1+i>0）。
- G3 — 比較用的單利模型：S_n=B_0(1+ni)。
- G4 — 兩個對照情境：(a) 若 2% 其實是每季利率，三年是 12 季；(b) 第一年末計息後存入 100。


- B_n — 第 n 期期末餘額
- B_0 — 本金
- i — 每期利率
- 1+i — 每期累積因子
- S_n=B_0(1+ni) — 單利模型的餘額





## 規則與來源


- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- 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。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- 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）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_ci_def · cited — 在期別、計息時點與每期利率 i 已固定，且期間內無存提款或費用時，複利餘額以 B_(n+1)=(1+i)B_n 更新。若累積因子 1+i>0，n 期後為 B_0(1+i)^n。 · mko-compound-interest
- mko_ci_notes · cited — 利息金額是期末餘額減本金；若有定期存款、提款、費用或變動利率，就不是本條目的單一冪次模型。年利率、月利率與名目／有效利率不能混用；必須先固定期別與轉換慣例。 · mko-compound-interest
- nat_power_def · prerequisite — 自然數次冪的遞迴定義：a^0=1，a^(n+1)=a^n·a。
- L_balance · lemma — 在 G1、G2 的模型中，對每個自然數 n，B_n=B_0(1+i)^n。
- L_bernoulli · lemma — Bernoulli 不等式：若 i≥−1，則對每個自然數 n，(1+i)^n≥1+ni。





## 逐步主鏈

S01 · definition操作前

\text{fixed period, rate, timing; no cash flows}

操作後

B_{n+1}=(1+i)B_n,\ B_0=1000,\ i=\tfrac{1}{50}

條件：1+i>0

規則：mko_ci_def · 依賴：G1, G2

葉節點依據：mko_ci_def + def_intro

依 MKO 寫出模型：每期先把目前餘額乘以同一個累積因子 1+i。模型的適用前提是期別、計息時點與利率都已固定，且期間內沒有任何現金流、費用或四捨五入（G1）。



S02 · equivalent操作前

1+i=1+\tfrac{1}{50}

操作後

1+i=\tfrac{51}{50}>0

條件：無

規則：frac_rules · 依賴：G2

葉節點依據：frac_rules + numeric_evaluation + order_basics

累積因子 1+1/50=51/50，是正數，符合 MKO 假設 a2 的 1+i>0；本金 1000 也非負。



S03 · implies操作前

B_{n+1}=(1+i)B_n

操作後

\forall n\in\mathbb{N}:\ B_n=B_0(1+i)^n

條件：無

規則：L_balance · 依賴：S01, L_balance

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

依引理 L_balance（在 S03.1 到 S03.3 以數學歸納法證明）：反覆乘同一個因子 n 次得到冪次公式。



S04 · implies操作前

B_0=1000

操作後

B_1=1020,\ B_2=\tfrac{5202}{5},\ B_3=\tfrac{132651}{125}

條件：無

規則：numeric_evaluation · 依賴：S01, S02

葉節點依據：numeric_evaluation + frac_rules

依更新規則逐期計算：1000·51/50=1020；1020·51/50=5202/5（即 1040.4）；(5202/5)·51/50=132651/125（即 1061.208）。全程精確，沒有四捨五入。



S05 · equivalent操作前

B_0(1+i)^3=1000\left(\tfrac{51}{50}\right)^3

操作後

1000\cdot\tfrac{132651}{125000}=\tfrac{132651}{125}=B_3

條件：無

規則：power_laws · 依賴：S03, S04

葉節點依據：power_laws + frac_rules + numeric_evaluation

依閉式：51³=132651，50³=125000，1000·132651/125000=132651/125，與 S04 的逐期計算一致。



S06 · equivalent操作前

B_3-B_0

操作後

\tfrac{132651}{125}-1000=\tfrac{7651}{125}

條件：無

規則：mko_ci_notes · 依賴：S05, mko_ci_notes

葉節點依據：frac_rules + numeric_evaluation

依 MKO，利息金額是期末餘額減本金：132651/125−125000/125=7651/125，即 61.208。



S07 · equivalent操作前

S_3=B_0(1+3i)

操作後

S_3=1000\left(1+\tfrac{3}{50}\right)=1060

條件：無

規則：numeric_evaluation · 依賴：G3, G2

葉節點依據：numeric_evaluation + frac_rules

單利只對本金計息：1000·(53/50)=1060，利息 60。單利是另一個模型，不是複利模型的精確等式改寫。固定 n 時，(1+i)^n 的一次項為 1+ni，因此單利式可作小 i 的一階近似；本題仍比較兩個模型的精確數值，不把它們視為相等。



S08 · equivalent操作前

B_3-S_3=B_0\left[(1+i)^3-(1+3i)\right]

操作後

B_0(3i^2+i^3)=\tfrac{151}{125}

條件：無

規則：distributive · 依賴：S05, S07

葉節點依據：distributive + power_laws + numeric_evaluation

展開 (1+i)³=1+3i+3i²+i³（N10 為多項式恆等式），減去 1+3i 得 3i²+i³，這就是「利息再生利息」的部分。代入：1000·(3/2500+1/125000)=6/5+1/125=151/125（即 1.208），與 132651/125−1060 一致。



S09 · implies操作前

i\ge -1

操作後

\forall n\in\mathbb{N}:\ (1+i)^n\ge 1+ni

條件：i\ge -1

規則：L_bernoulli · 依賴：L_bernoulli

葉節點依據：nat_induction + order_basics + square_nonneg

依引理 L_bernoulli（在 S09.1 到 S09.3 以歸納證明）。這把 S08 的單一比較推廣到所有期數。



S10 · implies操作前

(1+i)^n\ge 1+ni,\ B_0\ge 0

操作後

\forall n:\ B_n\ge S_n;\ B_1=S_1=1020,\ B_3-S_3=\tfrac{151}{125}>0

條件：B_0\ge 0

規則：order_basics · 依賴：S03, S09, G2, G3

葉節點依據：order_basics + L_bernoulli

兩邊同乘非負數 B_0=1000：B_n=B_0(1+i)^n≥B_0(1+ni)=S_n 對每個 n 成立。n=0 與 n=1 時兩者相等（B_1=S_1=1020），n=3 時差 151/125>0。所以「複利不少於單利」對所有 n 成立，但不是每期都嚴格較多。



S11 · implies操作前

2\%\ \text{per quarter},\ 3\ \text{years}=12\ \text{quarters}

操作後

1000\left(\tfrac{51}{50}\right)^{12}\ge 1000\left(1+\tfrac{12}{50}\right)=1240>\tfrac{132651}{125}

條件：\text{period}=\text{quarter}

規則：mko_ci_notes · 依賴：G4, S03, S09, mko_ci_notes

葉節點依據：mko_ci_notes + L_bernoulli + numeric_evaluation

依 MKO，期別與期數必須一致。若 2% 是每季利率，三年有 12 期，餘額是 1000·(51/50)^12；依 Bernoulli 不等式它至少是 1240，遠大於年利率解讀下的 1061.208。同樣的「2%、三年」因期別不同而給出不同答案，所以必須先固定期別。



S12 · implies操作前

\text{deposit }100\ \text{at end of year 1}

操作後

(1020+100)\left(\tfrac{51}{50}\right)^2=\tfrac{145656}{125}\neq\tfrac{1459161}{1250}=1100\left(\tfrac{51}{50}\right)^3

條件：無

規則：mko_ci_notes · 依賴：G4, S04, mko_ci_notes

葉節點依據：mko_ci_notes + numeric_evaluation + power_laws

第一年末計息後存入 100：餘額變成 1120，再以 51/50 複利兩年，得 145656/125（即 1165.248）。若誤把本金當作 1100 套用單一冪次公式，得 1459161/1250（即 1167.3288），兩者不同。有期間現金流時已不是 MKO 的單一冪次模型，需要逐筆追蹤現金流。



S13 · implies操作前

\text{proved facts}

操作後

B_3=\tfrac{132651}{125},\ \text{interest }\tfrac{7651}{125},\ B_n\ge S_n\ \forall n

條件：無

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

葉節點依據：and_intro_elim

合併結論：B_n=B_0(1+i)^n；三年後餘額 132651/125，利息 7651/125；單利為 1060；對所有 n 複利不少於單利；期別混用與期間存款都使單一冪次公式不適用。這些是模型計算，不是投資建議或市場預測。







## 局部子步與引理

S03.1 · induction_base操作前

n=0

操作後

B_0=B_0\cdot 1=B_0(1+i)^0

條件：無

規則：nat_induction · 依賴：nat_power_def

葉節點依據：nat_power_def + mul_one

基底：(1+i)^0=1，所以 B_0(1+i)^0=B_0。



S03.2 · induction_step操作前

B_n=B_0(1+i)^n

操作後

B_{n+1}=(1+i)B_0(1+i)^n=B_0(1+i)^{n+1}

條件：無

規則：eq_replace · 依賴：S01, nat_power_def

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

歸納步：假設 B_n=B_0(1+i)^n。由更新規則 B_(n+1)=(1+i)B_n，代入歸納假設並以乘法交換結合律重排為 B_0((1+i)^n(1+i))，依次冪定義即 B_0(1+i)^(n+1)。



S03.3 · implies操作前

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

操作後

\forall n:\ B_n=B_0(1+i)^n

條件：無

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

葉節點依據：nat_induction

依數學歸納原理對所有 n 成立。S03.1 到 S03.3 合起來證得引理 L_balance。



S09.1 · induction_base操作前

n=0

操作後

(1+i)^0=1\ge 1=1+0\cdot i

條件：無

規則：nat_induction · 依賴：nat_power_def

葉節點依據：nat_power_def + mul_zero

基底：兩邊都等於 1，不等式成立（等號）。



S09.2 · induction_step操作前

(1+i)^n\ge 1+ni

操作後

(1+i)^{n+1}\ge(1+ni)(1+i)=1+(n+1)i+ni^2\ge 1+(n+1)i

條件：1+i\ge 0; n\ge 0

規則：order_basics · 依賴：nat_power_def, order_basics, square_nonneg

葉節點依據：order_basics + square_nonneg + distributive

歸納步：假設 (1+i)^n≥1+ni。兩邊同乘非負數 1+i（因 i≥−1）保持不等號方向：(1+i)^(n+1)=(1+i)^n(1+i)≥(1+ni)(1+i)。展開得 1+(n+1)i+ni²（N11），而 ni²≥0（n≥0 且平方非負），所以 ≥1+(n+1)i。



S09.3 · implies操作前

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

操作後

\forall n:\ (1+i)^n\ge 1+ni

條件：i\ge -1

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

葉節點依據：nat_induction

依數學歸納原理對所有 n 成立。S09.1 到 S09.3 合起來證得引理 L_bernoulli。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S03, S05, S06, S07, S10, S11, S12, and_intro_elim — 目標 G：本稿目標的各項判定。足夠條件 H：所列各步已證（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。
- S12 · premise_audit · S04, mko_ci_notes, numeric_evaluation — 需要第一年末的餘額 1020 與存款時點；結論只說明單一冪次公式不適用，不提出現金流模型。
- S11 · premise_audit · S03, S09, mko_ci_notes — 只需要冪次公式與 Bernoulli 下界；此步只說明期別錯置的後果，不換算名目與有效利率。
- S10 · premise_audit · S03, S09, order_basics — 需要 B_0≥0；若本金為負，不等號方向會反轉，但那不在 MKO 的範圍內。
- S09.3 · premise_audit · S09.1, S09.2, nat_induction — 兩個前提由 S09.1、S09.2 提供。
- S09.2 · premise_audit · order_basics, square_nonneg, distributive, nat_power_def — 關鍵條件是 1+i≥0：乘以負數會反轉不等號。這正是引理要求 i≥−1 的原因。
- S09.1 · premise_audit · nat_power_def, mul_zero — 只用到零次冪與 0·i=0。
- S09 · premise_audit · L_bernoulli — 依賴該引理；本例 i=1/50≥−1。
- S08 · inverse_equivalence · distributive, numeric_evaluation — 展開是恆等式，代值是精確計算，雙向成立。
- S07 · inverse_equivalence · numeric_evaluation, frac_rules — 精確計算，雙向相同。
- S06 · inverse_equivalence · frac_rules, numeric_evaluation — 加回 1000 即得 B_3，雙向成立。
- S05 · inverse_equivalence · power_laws, frac_rules, numeric_evaluation — 精確計算，雙向是同一個數。
- S04 · premise_audit · S01, numeric_evaluation — 每期只由前一期決定；精確有理數計算可獨立重算。
- S03.3 · premise_audit · S03.1, S03.2, nat_induction — 兩個前提由 S03.1、S03.2 提供。
- S03.2 · premise_audit · G2, eq_replace, mul_assoc, mul_comm, nat_power_def — 需要每期使用同一個 i；若某期有存款或利率改變，第一個等號就不成立。
- S03.1 · premise_audit · nat_power_def, mul_one — 只用到零次冪與乘法單位元。
- S03 · premise_audit · L_balance — 依賴該引理；引理用到利率不隨期改變。
- S02 · inverse_equivalence · frac_rules, numeric_evaluation — 精確有理數計算，雙向相同；正負由分子分母皆正得出。
- S01 · premise_audit · G1, G2, mko_ci_def — 此步只寫出模型，不推出新事實；任何違反 G1 的情況都不屬於此模型（見 S11、S12）。





## 錯誤控制與反例

單利與複利不能混同MKO 指出的誤解之一：B_0(1+ni) 是單利，B_0(1+i)^n 是複利。三年後兩者差 151/125，來自 3i²+i³ 這部分「利息的利息」；依 Bernoulli 不等式，複利對每個 n 都不少於單利，n=0、1 時相等。

期別與利率單位要一致MKO 指出的另一個誤解是混用不同期別的利率。同樣的「2%、三年」，年利率給出 1061.208，季利率給出至少 1240（S11）。計算前必須確定利率是每什麼期的利率，以及總共有幾期。

有現金流就不是單一冪次模型S12 中第一年末存入 100 後，正確餘額是 145656/125，而不是把本金當 1100 的 1459161/1250。存款、提款、費用、稅、變動利率或四捨五入都會破壞 S03.2 的歸納步，因為更新不再是單純乘以同一因子。


- 本金 1000、年複利 2%、三年後的餘額是 1000(1+3·0.02)=1060 → reject — 那是單利；複利為 1000(51/50)³=132651/125=1061.208（S05）。
- 若 2% 是季利率，三年後餘額仍是 1000(1.02)³ → reject — 三年是 12 季，應為 1000(1.02)^12，且至少 1240（S11）。
- 第一年末存入 100 後，三年後餘額是 1100·(1.02)³ → reject — 存款只複利兩年：(1020+100)(1.02)²=145656/125，與 1459161/1250 不同（S12）。
- 對每個 n，複利餘額都嚴格大於單利餘額 → reject — n=0 與 n=1 時兩者相等，例如 B_1=S_1=1020（S10）。





## 結論與限制

在每年 2%、年末計息、無現金流的模型中，歸納證明 B_n=1000·(51/50)^n；三年後 B_3=132651/125=1061.208，利息 7651/125=61.208。單利 1000(1+3/50)=1060，差額 1000(3i²+i³)=151/125。Bernoulli 不等式證明對所有 n 有 B_n≥S_n，n=0、1 時相等。若 2% 是季利率則三年為 12 期，餘額至少 1240；若第一年末存入 100，餘額為 145656/125，不能以單一冪次公式計算。以上不是投資建議。


- N12 是 n=0 到 30 的有限核對，只涵蓋這些期數；對所有 n 的結論由 S09 的歸納證明。
- 現值折現、名目與有效利率換算、年金與現金流時點屬於 MKO 的 formal next。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 40a7814824c3f040be3cac68187574b75fa4bc4de6b05d465c54acd3cd9c8741
- original source SHA-256: 1484cf0ee66f4257f1254bcbb2872828ba4fb74c4c8367c12c4072a75908034b
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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




