# 現值與折現：證明折現與複利互逆，並算出 1331 的三年現值

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

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

derivation-mko-present-value-discounting-01 · production-20261019-adopted-96



## 目標與範圍

在固定每期利率 i（1+i>0）與期數 n 下，證明 (1+i)^n>0，因此現值 PV_n(F)=F/(1+i)^n 有定義；證明 PV_n 與複利 A_n(P)=P(1+i)^n 互為反函數。再以 i=1/10（每年）、n=3、F=1331 算出現值 1000，用逐年折現與 roundtrip 交叉核對，並說明把折現寫成乘法或混用年率與月率為何錯誤。

在 MKO 的範圍內工作：期別、利率慣例與 n 一致，1+i>0，期間內無額外現金流、費用、稅或四捨五入（假設 a1）；金額為非負精確有理數，計算不是報價、投資建議或市場預測（假設 a2）。不處理多筆現金流、年金、變動利率或名目與有效利率的換算；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- power_laws
- frac_rules
- mul_inverse_nonzero
- order_basics
- nat_induction
- function_def
- numeric_evaluation


- G1 — 固定每期利率 i 為有理數且 1+i>0；n 為自然數；期別單位、利率慣例與 n 一致；期間內無額外現金流、費用、稅或四捨五入（MKO 假設 a1）。金額為非負精確有理數（假設 a2）。
- G2 — 定義：n 期複利累積 A_n(P)=P(1+i)^n；未來金額 F 的現值 PV_n(F)=F/(1+i)^n。
- G3 — 例子：每年利率 i=1/10，期數 n=3 年，未來金額 F=1331。
- G4 — 期別對照：月利率 j=1/100，每月計息。


- i — 每期固定利率（有理數），1+i>0
- n — 期數，自然數
- A_n(P)=P(1+i)^n — n 期複利累積
- PV_n(F)=\tfrac{F}{(1+i)^n} — 未來金額 F 的現值
- \mathbb{Q}_{\ge 0} — 非負有理數





## 規則與來源


- 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）。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- 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。
- 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 都有相同值。
- 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。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- composition_def · prerequisite — 合成：對 f:A→B 與 g:B→C，g∘f:A→C 定義為 (g∘f)(a)=g(f(a))。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_pv · cited — 相對固定每期利率 i、正累積因子 1+i 與期數 n，未來金額 F 的現值定義為 F/(1+i)^n。此式與固定期率複利互逆；現金流、變動利率與費用需另建模型。 · mko-present-value-discounting
- mko_compound · cited — 在期別、計息時點與每期利率 i 已固定，且期間內無存提款或費用時，複利餘額以 B_(n+1)=(1+i)B_n 更新。若累積因子 1+i>0，n 期後為 B_0(1+i)^n。 · mko-compound-interest
- L_pos_pow · lemma — 若 a>0，則對每個自然數 n，a^n>0。
- L_ge1_pow · lemma — 若 a≥1，則對每個自然數 n，a^n≥1。





## 逐步主鏈

S01 · definition操作前

\text{compounding and discounting}

操作後

A_n(P)=P(1+i)^n,\ PV_n(F)=\tfrac{F}{(1+i)^n},\ 1+i>0

條件：1+i>0

規則：mko_pv · 依賴：G1, G2, mko_pv, mko_compound

葉節點依據：mko_pv + mko_compound + def_intro

依兩個 MKO 固定定義：複利 n 期後的餘額為 P(1+i)^n；未來金額 F 的現值為 F/(1+i)^n。兩者用同一個每期利率 i 與同一個期數 n，期別單位必須一致（G1）。



S02 · implies操作前

1+i>0

操作後

\forall n\in\mathbb{N}:\ (1+i)^n>0

條件：1+i>0

規則：L_pos_pow · 依賴：G1

葉節點依據：nat_induction + order_basics + power_laws

證明引理 L_pos_pow（a=1+i）：正數的每個自然數次冪都是正數。以兩個子步做歸納。N11 是對 a=11/10、n=0 到 10 的有限核對，證明本身是歸納。



S03 · implies操作前

(1+i)^n>0

操作後

(1+i)^n\neq 0,\ \tfrac{1}{(1+i)^n}\ \text{exists}

條件：無

規則：mul_inverse_nonzero · 依賴：S02, S01

葉節點依據：mul_inverse_nonzero + order_basics

正數不等於 0，所以 (1+i)^n 有乘法反元素，PV_n(F)=F·(1/(1+i)^n) 對每個 F 都有定義。這就是 MKO 要求「正累積因子 1+i」的作用之一。



S04 · equivalent操作前

PV_n(A_n(P))

操作後

\tfrac{P(1+i)^n}{(1+i)^n}=P

條件：(1+i)^n\neq 0

規則：frac_rules · 依賴：S01, S03

葉節點依據：frac_rules + mul_assoc + mul_inverse_nonzero + mul_one

先複利再以同一因子與期數折現：PV_n(A_n(P))=P(1+i)^n·(1/(1+i)^n)=P·1=P。用到乘法結合律與反元素，條件是 (1+i)^n≠0（S03）。



S05 · equivalent操作前

A_n(PV_n(F))

操作後

\tfrac{F}{(1+i)^n}(1+i)^n=F

條件：(1+i)^n\neq 0

規則：frac_rules · 依賴：S01, S03

葉節點依據：frac_rules + mul_assoc + mul_inverse_nonzero + mul_one

反方向：先折現再複利，A_n(PV_n(F))=F·(1/(1+i)^n)·(1+i)^n=F·1=F。



S06 · implies操作前

PV_n\circ A_n=\mathrm{id},\ A_n\circ PV_n=\mathrm{id}

操作後

PV_n=A_n^{-1}\ \text{on}\ \mathbb{Q}_{\ge 0}

條件：無

規則：injective_surjective_def · 依賴：S04, S05, S02, function_def

葉節點依據：injective_surjective_def + composition_def + function_def

因 (1+i)^n 是正有理數（S02 與 i 為有理數），A_n 與 PV_n 都把非負有理數映到非負有理數。兩個合成都是恆等映射，所以 A_n 是雙射且 PV_n 是它的反函數：這就是 MKO 所說「此式與固定期率複利互逆」的精確內容。



S07 · equivalent操作前

(1+\tfrac{1}{10})^3

操作後

(\tfrac{11}{10})^3=\tfrac{1331}{1000}

條件：無

規則：power_laws · 依賴：G3, power_laws

葉節點依據：power_laws + numeric_evaluation

例子的累積因子：1+1/10=11/10>0，(11/10)³=11³/10³=1331/1000（N1）。期別是「年」，i 是每年利率，n=3 是年數，三者一致。



S08 · equivalent操作前

PV_3(1331)=\tfrac{1331}{1331/1000}

操作後

1000

條件：\tfrac{1331}{1000}\neq 0

規則：frac_rules · 依賴：S07, S01, S03

葉節點依據：frac_rules + numeric_evaluation

PV_3(1331)=1331÷(1331/1000)=1331·1000/1331=1000（N2）。三年後的 1331 在每年 10% 的模型下相當於現在的 1000。



S09 · equivalent操作前

A_3(1000)

操作後

1000\cdot\tfrac{1331}{1000}=1331

條件：無

規則：numeric_evaluation · 依賴：S08, S06, S07

葉節點依據：numeric_evaluation

roundtrip 核對：把 1000 以同一因子複利三年，得 1331（N3），回到原本的未來金額，與 S06 的互逆一致。



S10 · equivalent操作前

\tfrac{1331}{(11/10)^3}

操作後

\tfrac{1331}{11/10}=1210,\ \tfrac{1210}{11/10}=1100,\ \tfrac{1100}{11/10}=1000

條件：\tfrac{11}{10}\neq 0

規則：power_laws · 依賴：S07, S08, power_laws

葉節點依據：power_laws + frac_rules + numeric_evaluation

逐年折現：由 a³=a·a·a，除以 a³ 等於連續除以 a 三次。1331→1210→1100→1000（N4、N5、N6），與 S08 一致。這對應「每年往回折一期」，說明 n 期折現就是一期折現重複 n 次。



S11 · implies操作前

i\ge 0,\ F\ge 0

操作後

PV_n(F)\le F

條件：i\ge 0; F\ge 0

規則：L_ge1_pow · 依賴：G1, S03

葉節點依據：L_ge1_pow + order_basics + frac_rules

若 i≥0，則 a=1+i≥1，依引理 L_ge1_pow（兩個子步）a^n≥1。於是 F−PV_n(F)=F(a^n−1)/a^n：分子 F≥0、a^n−1≥0，分母 a^n>0，所以差 ≥0，即現值不超過未來金額。例子中 1000≤1331（N13）。



S12 · implies操作前

1331\cdot(\tfrac{11}{10})^3

操作後

\tfrac{1771561}{1000}\neq 1000=PV_3(1331)

條件：無

規則：numeric_evaluation · 依賴：S07, S08

葉節點依據：numeric_evaluation

把折現誤寫成乘上累積因子：1331·1331/1000=1771561/1000（N7），這是 1331 再複利三年的累積值 A_3(1331)，不是現值；它不等於 1000（N8）。由 S06，現值是累積的反運算，所以應除以因子。



S13 · implies操作前

\text{monthly rate}\ j=\tfrac{1}{100}

操作後

(1+j)^{12}>\tfrac{112}{100},\ (1+j)^{36}>(\tfrac{11}{10})^3

條件：無

規則：numeric_evaluation · 依賴：G1, G4, S07

葉節點依據：numeric_evaluation + power_laws + order_basics

期別必須一致：月利率 j=1/100 時，期數要以月計，三年是 n=36，折現時所除的累積因子是 (101/100)^36；它大於年利率 10% 三年的 1331/1000（N10），所以兩者給出不同的現值。另外 (101/100)^12>112/100（N9），所以「月 1%」也不等於「年 12% 每年計息一次」。把年利率配上月數（例如 (11/10)^36），或把月利率乘以 12 當作年有效利率，都違反 G1 的單位一致要求。



S14 · implies操作前

1+i>0,\ n\in\mathbb{N}

操作後

PV_n=A_n^{-1};\ PV_3(1331)=1000\ \text{at}\ i=\tfrac{1}{10}

條件：無

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

葉節點依據：and_intro_elim

彙整：1+i>0 使 (1+i)^n>0，現值有定義（S02、S03）；折現與複利互為反函數（S06）；每年 10%、三年後的 1331 現值為 1000，逐年折現與 roundtrip 都核對一致（S08、S09、S10）；i≥0 時現值不超過未來金額（S11）；乘以因子或混用期別都會出錯（S12、S13）。







## 局部子步與引理

S02.1 · induction_base操作前

n=0

操作後

a^0=1>0

條件：無

規則：nat_induction · 依賴：power_laws

葉節點依據：nat_induction + power_laws

基底：a^0=1，而 1>0。



S02.2 · induction_step操作前

a^n>0,\ a>0

操作後

a^{n+1}=a^n\cdot a>0

條件：a>0

規則：order_basics · 依賴：S02.1, power_laws, order_basics

葉節點依據：order_basics + power_laws + mul_zero + nat_induction

設 a^n>0。由指數律 a^(n+1)=a^n·a。由 0<a^n 兩邊乘正數 a 得 0·a<a^n·a，即 a^(n+1)>0。依歸納原理，對所有 n 成立。S02.1 與 S02.2 證得引理 L_pos_pow。



S11.1 · induction_base操作前

n=0

操作後

a^0=1\ge 1

條件：無

規則：nat_induction · 依賴：power_laws

葉節點依據：nat_induction + power_laws

基底：a^0=1≥1。



S11.2 · induction_step操作前

a^n\ge 1,\ a\ge 1

操作後

a^{n+1}=a^n\cdot a\ge a\ge 1

條件：a\ge 1

規則：order_basics · 依賴：S11.1, order_basics, power_laws

葉節點依據：order_basics + power_laws + nat_induction

設 a^n≥1。a≥1>0，把 a^n≥1 兩邊乘正數 a 得 a^n·a≥a，再與 a≥1 傳遞得 a^(n+1)≥1。依歸納原理對所有 n 成立。S11.1 與 S11.2 證得引理 L_ge1_pow。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S03, S06, S08, S11 — 目標 G：現值有定義、與複利互逆、例子的現值。足夠條件 H：S03、S06、S08（S11 為附帶性質）；H⇒G 由合取。H 由定義、指數律與歸納正向證成，沒有把 G 當作前提；S12、S13 只說明錯誤做法。
- S13 · premise_audit · G1, G4, numeric_evaluation — 這些是精確的有理數比較；不處理名目與有效利率的正式換算（MKO 的 formal next）。
- S12 · premise_audit · numeric_evaluation, S08 — 一個數值反例足以說明乘法不是折現；不宣稱兩者在任何情況下都不同（F=0 或 n=0 時相同）。
- S11.2 · premise_audit · order_basics, power_laws, nat_induction — 需要 a 為正才能保序相乘，並需要 a≥1 才能傳遞到 1。
- S11.1 · premise_audit · power_laws, nat_induction — 只用 a^0=1。
- S11 · premise_audit · L_ge1_pow, S02, order_basics, frac_rules — i≥0 與 F≥0 是本步的充分前提；若 −1<i<0、n≥1 且 F>0，則 (1+i)^n<1，現值大於未來金額，故不能不加條件推廣 PV≤F。F=0 或 n=0 時仍為等號。
- S10 · inverse_equivalence · power_laws, frac_rules — x/(abc)=((x/a)/b)/c 對非零 a、b、c 成立，兩種算法同值。
- S09 · inverse_equivalence · numeric_evaluation — 精確計算；這是 S06 的例子，不是它的證明。
- S08 · inverse_equivalence · frac_rules, numeric_evaluation — 除以非零分數等於乘以其倒數；精確計算，兩邊同值。
- S07 · inverse_equivalence · power_laws, numeric_evaluation — (a/b)^n=a^n/b^n 是指數律，兩邊同值。
- S06 · premise_audit · S04, S05, injective_surjective_def, composition_def — 互逆需要兩個方向的合成都是恆等；只有一個方向只給出單射或滿射。本模型以同一個 i 與 n 保證累積因子相同；代數上只需要兩邊使用相同的正累積因子，不要求參數表示唯一。例如 (1+3)^1=(1+1)^2=4。這不取消期別與利率單位必須一致的建模要求。
- S05 · inverse_equivalence · frac_rules, mul_inverse_nonzero, mul_assoc — 同 S04，對所有 F 成立的恆等式。
- S04 · inverse_equivalence · frac_rules, mul_inverse_nonzero, mul_assoc — 每一步都是對所有 P 成立的恆等式，兩邊指同一個數（N12 以 i=1/10、n=3 的一次恆等式核對）。
- S03 · premise_audit · S02, mul_inverse_nonzero, order_basics — 只需要非零；正性另外保證 PV 把非負金額映到非負金額。
- S02.2 · premise_audit · order_basics, power_laws, nat_induction — 乘以正數保序是這一步的關鍵，需要 a>0。
- S02.1 · premise_audit · power_laws, nat_induction — 只用 a^0=1。
- S02 · premise_audit · L_pos_pow, G1 — 需要 1+i>0；若 1+i<0，奇數次冪為負；若 1+i=0，n≥1 時冪為 0。
- S01 · premise_audit · G1, G2, mko_pv, mko_compound — 此步只陳述定義，不推出新事實；PV_n 是否有定義留待 S03。





## 錯誤控制與反例

折現要除以累積因子，不是乘上它MKO 指出的第一個誤解是把折現乘上累積因子。1331·(11/10)³=1771561/1000 是 1331 再複利三年的結果（S12）；現值是累積的反運算（S06），應為 1331/(11/10)³=1000。檢查方法：把結果再複利同樣期數，應回到原金額（S09）。

期別與期數必須一致MKO 指出的第二個誤解是混用年率、月率與不同期數。年利率要配年數，月利率要配月數；(101/100)^12>112/100，所以月 1% 不等於年 12%（S13）。本稿的公式只在 i 與 n 使用同一期別時適用。

1+i>0 的作用1+i>0 保證 (1+i)^n>0（S02），所以可以除（S03），且現值保持非負。i=−1 時 1+i=0，n≥1 的折現要除以 0，沒有定義；這不是「現值為 0」。


- 每年 10%，三年後 1331 的現值是 1331×1.1³ → reject — 那是累積值 1771561/1000；現值是 1331/1.1³=1000。
- 年利率 10%、36 個月後的 F，現值為 F/(1.1)^36 → reject — 年利率要配年數，n=3，不是 36；混用期別違反假設 a1。
- 月利率 1% 每月複利，等同年利率 12% 每年複利一次 → reject — (101/100)^12>112/100（N9）。
- i=−1 時，現值 F/(1+i)^n 為 0 → reject — 1+i=0 違反 1+i>0；n≥1 時要除以 0，沒有定義。





## 結論與限制

當 1+i>0 時，(1+i)^n>0，現值 PV_n(F)=F/(1+i)^n 有定義，且 PV_n 與複利 A_n(P)=P(1+i)^n 互為反函數。每年利率 10%、三年後的 1331，現值為 1331/(11/10)³=1000；逐年折現 1331→1210→1100→1000 與 roundtrip 1000·(11/10)³=1331 都一致。i≥0 時現值不超過未來金額。把折現寫成乘法得到的是累積值 1771561/1000，而期別不一致（年率配月數，或月率 1% 當年率 12%）會給出不同的因子。


- 多筆現金流的時點、年金、名目與有效利率的換算與敏感度分析屬於 MKO 的 formal next，本稿不處理；所有計算只是模型計算，不是報價或投資建議。
- N11 是 n=0 到 10 的有限核對，(1+i)^n>0 對所有 n 的證明是 S02 的歸納；N12 是一次多項式恆等式的網格核對。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: b712d385bc1ee8edccfd1a652e7db341e2a1b9342c4e958af54cc398fe26a0a5
- original source SHA-256: 985912bc73b59962d395f9a20ecb54a42e67fe4bb06bf99ec0459f92ca92d0e0
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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