# Present value and discounting: proving that discounting inverts compounding, and the three-year present value of 1331

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-present-value-discounting/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

For a fixed rate i per period (1+i>0) and a period count n, prove that (1+i)^n>0, so the present value PV_n(F)=F/(1+i)^n is defined; prove that PV_n and compounding A_n(P)=P(1+i)^n are inverse functions of each other. Then, with i=1/10 per year, n=3 and F=1331, compute the present value 1000, cross-check by year-by-year discounting and a round trip, and explain why writing discounting as a multiplication, or mixing annual and monthly rates, is wrong.

Works inside the MKO's scope: period units, rate conventions and n agree, 1+i>0, and there are no additional cash flows, fees, taxes or rounding during the modeled interval (assumption a1); amounts are nonnegative exact rationals, and the computations are not quotes, investment advice or market forecasts (assumption a2). Multiple cash flows, annuities, variable rates and nominal-to-effective conversion are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


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


- G1 — The fixed rate i per period is rational with 1+i>0; n is a natural number; period units, rate conventions and n agree; there are no additional cash flows, fees, taxes or rounding during the interval (MKO assumption a1). Amounts are nonnegative exact rationals (assumption a2).
- G2 — Definitions: accumulation over n periods A_n(P)=P(1+i)^n; present value of a future amount F, PV_n(F)=F/(1+i)^n.
- G3 — Example: rate i=1/10 per year, n=3 years, future amount F=1331.
- G4 — Period comparison: a monthly rate j=1/100, compounded monthly.


- i — the fixed rate per period (rational), 1+i>0
- n — the number of periods, a natural number
- A_n(P)=P(1+i)^n — accumulation by compounding over n periods
- PV_n(F)=\tfrac{F}{(1+i)^n} — the present value of a future amount F
- \mathbb{Q}_{\ge 0} — the nonnegative rationals





## Rules and sources


- power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
- function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
- composition_def · prerequisite — Composition: for f:A→B and g:B→C, g∘f:A→C is defined by (g∘f)(a)=g(f(a)).
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_pv · cited — Relative to a fixed rate i per period, positive accumulation factor 1+i and period count n, the present value of a future amount F is defined as F/(1+i)^n. This inverts fixed-period-rate compounding. Cash flows, variable rates and fees require a different model. · mko-present-value-discounting
- mko_compound · cited — Fix periods, interest timing and rate i per period, with no deposits, withdrawals or fees during the modeled interval. Compound balance updates are B_(n+1)=(1+i)B_n. For 1+i>0, the balance after n periods is B_0(1+i)^n. · mko-compound-interest
- L_pos_pow · lemma — If a>0, then a^n>0 for every natural number n.
- L_ge1_pow · lemma — If a≥1, then a^n≥1 for every natural number n.





## Main derivation

S01 · definitionBefore

\text{compounding and discounting}

After

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

Conditions: 1+i>0

Rule: mko_pv · Uses: G1, G2, mko_pv, mko_compound

Leaf basis: mko_pv + mko_compound + def_intro

Fix the definitions from the two MKOs: after n periods of compounding the balance is P(1+i)^n; the present value of a future amount F is F/(1+i)^n. Both use the same rate per period i and the same period count n, and the period units must agree (G1).



S02 · impliesBefore

1+i>0

After

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

Conditions: 1+i>0

Rule: L_pos_pow · Uses: G1

Leaf basis: nat_induction + order_basics + power_laws

Prove Lemma L_pos_pow (with a=1+i): every natural-number power of a positive number is positive. Two sub-steps form an induction. N11 is a finite check for a=11/10 and n=0 to 10; the proof itself is the induction.



S03 · impliesBefore

(1+i)^n>0

After

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

Conditions: none

Rule: mul_inverse_nonzero · Uses: S02, S01

Leaf basis: mul_inverse_nonzero + order_basics

A positive number is not 0, so (1+i)^n has a multiplicative inverse and PV_n(F)=F·(1/(1+i)^n) is defined for every F. This is one role of the MKO's requirement of a 'positive accumulation factor 1+i'.



S04 · equivalentBefore

PV_n(A_n(P))

After

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

Conditions: (1+i)^n\neq 0

Rule: frac_rules · Uses: S01, S03

Leaf basis: frac_rules + mul_assoc + mul_inverse_nonzero + mul_one

Compound first, then discount with the same factor and period count: PV_n(A_n(P))=P(1+i)^n·(1/(1+i)^n)=P·1=P. This uses associativity and the multiplicative inverse, under the condition (1+i)^n≠0 (S03).



S05 · equivalentBefore

A_n(PV_n(F))

After

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

Conditions: (1+i)^n\neq 0

Rule: frac_rules · Uses: S01, S03

Leaf basis: frac_rules + mul_assoc + mul_inverse_nonzero + mul_one

The other order: discount first, then compound, A_n(PV_n(F))=F·(1/(1+i)^n)·(1+i)^n=F·1=F.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: injective_surjective_def · Uses: S04, S05, S02, function_def

Leaf basis: injective_surjective_def + composition_def + function_def

Since (1+i)^n is a positive rational (S02, with i rational), A_n and PV_n both map nonnegative rationals to nonnegative rationals. Both composites are the identity, so A_n is a bijection and PV_n is its inverse: this is the precise content of the MKO's 'this inverts fixed-period-rate compounding'.



S07 · equivalentBefore

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

After

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

Conditions: none

Rule: power_laws · Uses: G3, power_laws

Leaf basis: power_laws + numeric_evaluation

The example's accumulation factor: 1+1/10=11/10>0, and (11/10)³=11³/10³=1331/1000 (N1). The period is the year, i is the rate per year and n=3 counts years, so the three agree.



S08 · equivalentBefore

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

After

1000

Conditions: \tfrac{1331}{1000}\neq 0

Rule: frac_rules · Uses: S07, S01, S03

Leaf basis: frac_rules + numeric_evaluation

PV_3(1331)=1331÷(1331/1000)=1331·1000/1331=1000 (N2). In the model with 10% per year, 1331 three years from now corresponds to 1000 now.



S09 · equivalentBefore

A_3(1000)

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S08, S06, S07

Leaf basis: numeric_evaluation

Round-trip check: compounding 1000 for three years with the same factor gives 1331 (N3), returning the original future amount, as S06 predicts.



S10 · equivalentBefore

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

After

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

Conditions: \tfrac{11}{10}\neq 0

Rule: power_laws · Uses: S07, S08, power_laws

Leaf basis: power_laws + frac_rules + numeric_evaluation

Year-by-year discounting: since a³=a·a·a, dividing by a³ is dividing by a three times in a row. 1331→1210→1100→1000 (N4, N5, N6), agreeing with S08. This corresponds to 'discounting back one period each year' and shows that discounting over n periods is one-period discounting repeated n times.



S11 · impliesBefore

i\ge 0,\ F\ge 0

After

PV_n(F)\le F

Conditions: i\ge 0; F\ge 0

Rule: L_ge1_pow · Uses: G1, S03

Leaf basis: L_ge1_pow + order_basics + frac_rules

If i≥0, then a=1+i≥1, and by Lemma L_ge1_pow (two sub-steps) a^n≥1. Then F−PV_n(F)=F(a^n−1)/a^n: the numerator has F≥0 and a^n−1≥0 and the denominator a^n>0, so the difference is ≥0, that is the present value does not exceed the future amount. In the example 1000≤1331 (N13).



S12 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S07, S08

Leaf basis: numeric_evaluation

Writing discounting wrongly as multiplication by the accumulation factor: 1331·1331/1000=1771561/1000 (N7), which is the accumulation A_3(1331) of 1331 over three more years, not the present value; it differs from 1000 (N8). By S06 the present value is the inverse of accumulation, so one must divide by the factor.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G1, G4, S07

Leaf basis: numeric_evaluation + power_laws + order_basics

Period units must agree: with the monthly rate j=1/100 the periods are counted in months, three years is n=36, and the accumulation factor by which to divide is (101/100)^36; it exceeds 1331/1000 for 10% per year over three years (N10), so the two give different present values. Also (101/100)^12>112/100 (N9), so '1% per month' is not '12% per year compounded once a year'. Pairing an annual rate with a count of months (such as (11/10)^36), or treating twelve times a monthly rate as an effective annual rate, violates the unit agreement required by G1.



S14 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S03, S06, S08, S10, S11, S12, S13

Leaf basis: and_intro_elim

Summary: 1+i>0 makes (1+i)^n>0, so the present value is defined (S02, S03); discounting and compounding are inverse functions (S06); at 10% per year the present value of 1331 due in three years is 1000, confirmed by year-by-year discounting and the round trip (S08, S09, S10); for i≥0 the present value does not exceed the future amount (S11); multiplying by the factor or mixing period units goes wrong (S12, S13).







## Substeps and lemmas

S02.1 · induction_baseBefore

n=0

After

a^0=1>0

Conditions: none

Rule: nat_induction · Uses: power_laws

Leaf basis: nat_induction + power_laws

Base: a^0=1, and 1>0.



S02.2 · induction_stepBefore

a^n>0,\ a>0

After

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

Conditions: a>0

Rule: order_basics · Uses: S02.1, power_laws, order_basics

Leaf basis: order_basics + power_laws + mul_zero + nat_induction

Assume a^n>0. By the exponent law a^(n+1)=a^n·a. Multiplying 0<a^n by the positive number a gives 0·a<a^n·a, that is a^(n+1)>0. By induction this holds for every n. S02.1 and S02.2 prove Lemma L_pos_pow.



S11.1 · induction_baseBefore

n=0

After

a^0=1\ge 1

Conditions: none

Rule: nat_induction · Uses: power_laws

Leaf basis: nat_induction + power_laws

Base: a^0=1≥1.



S11.2 · induction_stepBefore

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

After

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

Conditions: a\ge 1

Rule: order_basics · Uses: S11.1, order_basics, power_laws

Leaf basis: order_basics + power_laws + nat_induction

Assume a^n≥1. Since a≥1>0, multiplying a^n≥1 by the positive a gives a^n·a≥a, and with a≥1 transitivity gives a^(n+1)≥1. By induction this holds for every n. S11.1 and S11.2 prove Lemma L_ge1_pow.







## Reverse audits


- S14 · sufficient_goal_reduction · S03, S06, S08, S11 — Goal G: the present value is defined, inverts compounding, and the example's value. Sufficient condition H: S03, S06 and S08 (with S11 as an additional property); H⇒G by conjunction. H is proved forwards from the definitions, exponent laws and induction; G is never used as a premise, and S12, S13 only illustrate wrong methods.
- S13 · premise_audit · G1, G4, numeric_evaluation — These are exact rational comparisons; the formal conversion between nominal and effective rates (the MKO's formal next step) is not treated.
- S12 · premise_audit · numeric_evaluation, S08 — One numeric counterexample suffices to show multiplication is not discounting; it is not claimed that they always differ (they agree when F=0 or n=0).
- S11.2 · premise_audit · order_basics, power_laws, nat_induction — a must be positive to multiply while preserving order, and a≥1 is needed to pass on to 1.
- S11.1 · premise_audit · power_laws, nat_induction — Only a^0=1 is used.
- S11 · premise_audit · L_ge1_pow, S02, order_basics, frac_rules — The assumptions i≥0 and F≥0 are sufficient here. If −1<i<0, n≥1 and F>0, then (1+i)^n<1 and the present value exceeds the future amount, so PV≤F cannot be extended without conditions. Equality still holds when F=0 or n=0.
- S10 · inverse_equivalence · power_laws, frac_rules — x/(abc)=((x/a)/b)/c for nonzero a, b, c, so the two computations agree.
- S09 · inverse_equivalence · numeric_evaluation — An exact computation; it is an instance of S06, not its proof.
- S08 · inverse_equivalence · frac_rules, numeric_evaluation — Dividing by a nonzero fraction is multiplying by its reciprocal; an exact computation, so both sides agree.
- S07 · inverse_equivalence · power_laws, numeric_evaluation — (a/b)^n=a^n/b^n is an exponent law; both sides have the same value.
- S06 · premise_audit · S04, S05, injective_surjective_def, composition_def — Being inverses needs both composites to be the identity; one direction alone gives only injectivity or surjectivity. Using the same i and n ensures a common accumulation factor in this model. Algebraically, the two maps need the same positive factor, not a unique parameterization: for example (1+3)^1=(1+1)^2=4. This does not remove the modeling requirement that period and rate units agree.
- S05 · inverse_equivalence · frac_rules, mul_inverse_nonzero, mul_assoc — As in S04, an identity for all F.
- S04 · inverse_equivalence · frac_rules, mul_inverse_nonzero, mul_assoc — Every move is an identity for all P, so both sides name the same number (N12 checks the degree-one identity for i=1/10, n=3).
- S03 · premise_audit · S02, mul_inverse_nonzero, order_basics — Only nonzero is needed here; positivity additionally ensures that PV maps nonnegative amounts to nonnegative amounts.
- S02.2 · premise_audit · order_basics, power_laws, nat_induction — That multiplying by a positive number preserves order is the key, and it needs a>0.
- S02.1 · premise_audit · power_laws, nat_induction — Only a^0=1 is used.
- S02 · premise_audit · L_pos_pow, G1 — It needs 1+i>0; if 1+i<0, odd powers are negative; if 1+i=0, the power is 0 for n≥1.
- S01 · premise_audit · G1, G2, mko_pv, mko_compound — This step only states the definitions and derives no new fact; whether PV_n is defined is settled in S03.





## Error controls and negative controls

Discount by dividing by the accumulation factor, not multiplying by itThe first mistake named by the MKO is multiplying by the accumulation factor when discounting. 1331·(11/10)³=1771561/1000 is 1331 compounded for three more years (S12); the present value is the inverse of accumulation (S06), namely 1331/(11/10)³=1000. The check: compound the result over the same periods and it must return the original amount (S09).

Period units and counts must agreeThe second mistake named by the MKO is mixing annual rates, monthly rates and different period counts. An annual rate goes with a count of years, a monthly rate with a count of months; (101/100)^12>112/100, so 1% per month is not 12% per year (S13). The formula here applies only when i and n use the same period.

What 1+i>0 does1+i>0 guarantees (1+i)^n>0 (S02), so the division is possible (S03) and present values stay nonnegative. With i=−1, 1+i=0 and discounting over n≥1 periods would divide by 0, which is undefined; it is not 'a present value of 0'.


- At 10% per year, the present value of 1331 due in three years is 1331×1.1³ → reject — That is the accumulation 1771561/1000; the present value is 1331/1.1³=1000.
- With an annual rate of 10%, the present value of F due in 36 months is F/(1.1)^36 → reject — An annual rate goes with years, n=3, not 36; mixing periods violates assumption a1.
- 1% per month compounded monthly is the same as 12% per year compounded once a year → reject — (101/100)^12>112/100 (N9).
- With i=−1, the present value F/(1+i)^n is 0 → reject — 1+i=0 violates 1+i>0; for n≥1 it would divide by 0, which is undefined.





## Result and limitations

When 1+i>0, (1+i)^n>0, the present value PV_n(F)=F/(1+i)^n is defined, and PV_n and compounding A_n(P)=P(1+i)^n are inverse functions. At 10% per year, 1331 due in three years has present value 1331/(11/10)³=1000; year-by-year discounting 1331→1210→1100→1000 and the round trip 1000·(11/10)³=1331 agree. For i≥0 the present value does not exceed the future amount. Writing discounting as multiplication gives the accumulation 1771561/1000 instead, and mismatched periods (an annual rate with a count of months, or 1% monthly taken as 12% annual) give different factors.


- Timing of multiple cash flows, annuities, nominal-to-effective rate conversion and sensitivity analysis belong to the MKO's formal next step and are not treated; all computations are model computations, not quotes or investment advice.
- N11 is a finite check for n=0 to 10; the proof that (1+i)^n>0 for all n is the induction of S02; N12 is a grid check of a degree-one polynomial identity.





## Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-present-value-discounting-01.json)