Compound-interest model: principal 1000 at 2% per year for three years, compared with simple interest

Goal and scope

In the model with one-year periods, rate i=1/50 (2%) per period and no deposits, withdrawals or fees, prove B_n=B_0(1+i)^n by induction, compute the balance after three years from B_0=1000, namely 132651/125 (that is 1061.208), and the interest; compare with simple interest B_0(1+ni)=1060 and prove by Bernoulli's inequality that the compound balance is never below the simple one for any n; explain how mixing period units and cash flows during the period break the single-power formula.

Computes only under the MKO's assumptions: period, rate and number of periods use the same unit, the rate is fixed, there are no cash flows, taxes, fees or rounding, the principal is a nonnegative exact rational and 1+i>0 (assumptions a1 and a2). These calculations are not investment advice, quotes or market predictions. Present value, conversion between nominal and effective rates, and annuities are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• nat_induction
• eq_replace
• order_basics
• square_nonneg
• distributive

• G1 — The period is one year and interest is credited at the end of each year; the rate i per period is fixed; there are no deposits, withdrawals, fees, taxes or rounding during the modeled interval (MKO assumption a1).
• G2 — B_0=1000, i=1/50 (2% per year), number of periods n=3; update rule B_(n+1)=(1+i)B_n (assumption a2: nonnegative principal and 1+i>0).
• G3 — Simple-interest model for comparison: S_n=B_0(1+ni).
• G4 — Two contrast scenarios: (a) if the 2% were a quarterly rate, three years would be 12 quarters; (b) a deposit of 100 is made at the end of year 1, after interest is credited.

• B_n — balance at the end of period n
• B_0 — principal
• i — rate per period
• 1+i — accumulation factor per period
• S_n=B_0(1+ni) — balance under simple interest

Rules and sources

• 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₀.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• 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.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• 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.
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• 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.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_ci_def · 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
• mko_ci_notes · cited — The interest amount is the final balance minus the principal; with regular deposits, withdrawals, fees or variable rates the single-power model of this entry no longer applies. Annual, monthly, nominal and effective rates must not be mixed; the period and conversion convention must be fixed first. · mko-compound-interest
• nat_power_def · prerequisite — Recursive definition of natural-number powers: a^0=1 and a^(n+1)=a^n·a.
• L_balance · lemma — In the model of G1 and G2, B_n=B_0(1+i)^n for every natural number n.
• L_bernoulli · lemma — Bernoulli's inequality: if i≥−1 then (1+i)^n≥1+ni for every natural number n.

Main derivation

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

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

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

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

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

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

B_0=1000

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

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

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

B_3-B_0

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

S_3=B_0(1+3i)

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

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

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

i\ge -1

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

(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

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

\text{proved facts}

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

Substeps and lemmas

n=0

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

B_n=B_0(1+i)^n

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

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

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

n=0

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

(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

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

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

Reverse audits

• S13 · sufficient_goal_reduction · S03, S05, S06, S07, S10, S11, S12, and_intro_elim — Goal G: the determinations in the goal. Sufficient condition H: the listed steps, each already proved (H⇒G by conjunction introduction). H is derived forwards from the givens; G is never used as a premise.
• S12 · premise_audit · S04, mko_ci_notes, numeric_evaluation — It needs the year-1 balance 1020 and the timing of the deposit; the conclusion only shows that the single-power formula does not apply and does not propose a cash-flow model.
• S11 · premise_audit · S03, S09, mko_ci_notes — It needs only the power formula and the Bernoulli lower bound; it shows the effect of a mismatched period and does not convert between nominal and effective rates.
• S10 · premise_audit · S03, S09, order_basics — It needs B_0≥0; with a negative principal the inequality would reverse, but that is outside the MKO's scope.
• S09.3 · premise_audit · S09.1, S09.2, nat_induction — The two premises come from S09.1 and S09.2.
• S09.2 · premise_audit · order_basics, square_nonneg, distributive, nat_power_def — The key condition is 1+i≥0: multiplying by a negative number would reverse the inequality. That is exactly why the lemma requires i≥−1.
• S09.1 · premise_audit · nat_power_def, mul_zero — It uses only the zeroth power and 0·i=0.
• S09 · premise_audit · L_bernoulli — It depends on the lemma; here i=1/50≥−1.
• S08 · inverse_equivalence · distributive, numeric_evaluation — The expansion is an identity and the substitution is exact, so both directions hold.
• S07 · inverse_equivalence · numeric_evaluation, frac_rules — Exact computation, the same both ways.
• S06 · inverse_equivalence · frac_rules, numeric_evaluation — Adding back 1000 gives B_3, so both directions hold.
• S05 · inverse_equivalence · power_laws, frac_rules, numeric_evaluation — Exact computation; both sides are the same number.
• S04 · premise_audit · S01, numeric_evaluation — Each period depends only on the previous one; the exact rational arithmetic can be recomputed independently.
• S03.3 · premise_audit · S03.1, S03.2, nat_induction — The two premises come from S03.1 and S03.2.
• S03.2 · premise_audit · G2, eq_replace, mul_assoc, mul_comm, nat_power_def — It needs the same i in every period; with a deposit or a rate change in some period, the first equality fails.
• S03.1 · premise_audit · nat_power_def, mul_one — It uses only the zeroth power and the multiplicative identity.
• S03 · premise_audit · L_balance — It depends on the lemma, which uses that the rate does not change from period to period.
• S02 · inverse_equivalence · frac_rules, numeric_evaluation — Exact rational arithmetic, the same both ways; positivity follows from a positive numerator and denominator.
• S01 · premise_audit · G1, G2, mko_ci_def — This step only states the model and derives no new fact; any situation violating G1 is outside the model (see S11 and S12).

Error controls and negative controls

Simple and compound interest must not be confused

One misconception named by the MKO: B_0(1+ni) is simple interest and B_0(1+i)^n is compound interest. After three years they differ by 151/125, coming from the 'interest on interest' part 3i²+i³; by Bernoulli's inequality compound is never below simple for any n, with equality at n=0 and 1.

The period and the rate unit must agree

Another misconception named by the MKO is mixing rates of different periods. The same '2%, three years' gives 1061.208 with an annual rate and at least 1240 with a quarterly rate (S11). Before computing, fix what period the rate refers to and how many periods there are.

With cash flows it is not the single-power model

In S12, after a deposit of 100 at the end of year 1, the correct balance is 145656/125, not 1459161/1250 from treating the principal as 1100. Deposits, withdrawals, fees, taxes, variable rates or rounding all break the inductive step of S03.2, because an update is no longer a plain multiplication by the same factor.

• With principal 1000 at 2% compounded yearly, the balance after three years is 1000(1+3·0.02)=1060 → reject — That is simple interest; compound gives 1000(51/50)³=132651/125=1061.208 (S05).
• If 2% is a quarterly rate, the balance after three years is still 1000(1.02)³ → reject — Three years are 12 quarters, so it is 1000(1.02)^12, at least 1240 (S11).
• After a deposit of 100 at the end of year 1, the balance after three years is 1100·(1.02)³ → reject — The deposit compounds for two years only: (1020+100)(1.02)²=145656/125, unlike 1459161/1250 (S12).
• For every n the compound balance is strictly greater than the simple balance → reject — At n=0 and n=1 they are equal, for example B_1=S_1=1020 (S10).

Result and limitations

In the model with 2% per year credited at year end and no cash flows, induction proves B_n=1000·(51/50)^n; after three years B_3=132651/125=1061.208 and the interest is 7651/125=61.208. Simple interest gives 1000(1+3/50)=1060, a difference of 1000(3i²+i³)=151/125. Bernoulli's inequality proves B_n≥S_n for all n, with equality at n=0 and 1. If the 2% were quarterly, three years would be 12 periods and the balance at least 1240; with a deposit of 100 at the end of year 1 the balance is 145656/125, which is not given by the original no-cash-flow single-power model. None of this is investment advice.

• N12 is a finite check for n=0 to 30 only; the statement for all n is proved by the induction of S09.
• Present-value discounting, nominal and effective rate conversion, annuities and cash-flow timing belong to the MKO's formal next step.

Verification and source binding

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

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

Same-source full JSON (formulas, ASTs, controls and revision log)