# Compound-interest model: principal 1000 at 2% per year for three years, compared with simple interest [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-compound-interest/) 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-compound-interest-01 · production-20261019-adopted-96 ## 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 uv holds; u0 give uwvw. - 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 S01 · definitionBefore \text{fixed period, rate, timing; no cash flows} After B_{n+1}=(1+i)B_n,\ B_0=1000,\ i=\tfrac{1}{50} Conditions: 1+i>0 Rule: mko_ci_def · Uses: G1, G2 Leaf basis: mko_ci_def + def_intro State the model as in the MKO: each period multiplies the current balance by the same accumulation factor 1+i. The model applies only once the period, interest timing and rate are fixed, with no cash flows, fees or rounding during the interval (G1). S02 · equivalentBefore 1+i=1+\tfrac{1}{50} After 1+i=\tfrac{51}{50}>0 Conditions: none Rule: frac_rules · Uses: G2 Leaf basis: frac_rules + numeric_evaluation + order_basics The accumulation factor 1+1/50=51/50 is positive, meeting 1+i>0 from MKO assumption a2; the principal 1000 is nonnegative too. S03 · impliesBefore B_{n+1}=(1+i)B_n After \forall n\in\mathbb{N}:\ B_n=B_0(1+i)^n Conditions: none Rule: L_balance · Uses: S01, L_balance Leaf basis: nat_induction + nat_power_def + mul_assoc + mul_comm By Lemma L_balance (proved by induction in S03.1 to S03.3): multiplying by the same factor n times gives the power formula. S04 · impliesBefore B_0=1000 After B_1=1020,\ B_2=\tfrac{5202}{5},\ B_3=\tfrac{132651}{125} Conditions: none Rule: numeric_evaluation · Uses: S01, S02 Leaf basis: numeric_evaluation + frac_rules Compute period by period from the update rule: 1000·51/50=1020; 1020·51/50=5202/5 (that is 1040.4); (5202/5)·51/50=132651/125 (that is 1061.208). Everything is exact, with no rounding. S05 · equivalentBefore B_0(1+i)^3=1000\left(\tfrac{51}{50}\right)^3 After 1000\cdot\tfrac{132651}{125000}=\tfrac{132651}{125}=B_3 Conditions: none Rule: power_laws · Uses: S03, S04 Leaf basis: power_laws + frac_rules + numeric_evaluation By the closed form: 51³=132651, 50³=125000, and 1000·132651/125000=132651/125, agreeing with the period-by-period computation of S04. S06 · equivalentBefore B_3-B_0 After \tfrac{132651}{125}-1000=\tfrac{7651}{125} Conditions: none Rule: mko_ci_notes · Uses: S05, mko_ci_notes Leaf basis: frac_rules + numeric_evaluation By the MKO, the interest amount is the final balance minus the principal: 132651/125−125000/125=7651/125, that is 61.208. S07 · equivalentBefore S_3=B_0(1+3i) After S_3=1000\left(1+\tfrac{3}{50}\right)=1060 Conditions: none Rule: numeric_evaluation · Uses: G3, G2 Leaf basis: numeric_evaluation + frac_rules Simple interest pays only on the principal: 1000·(53/50)=1060, with interest 60. Simple interest is a different model, not an exact rewriting of compound interest. For fixed n the linear part of (1+i)^n is 1+ni, so the simple-interest expression can serve as a first-order approximation for small i. This exercise still compares the exact values of the two models rather than identifying them. S08 · equivalentBefore B_3-S_3=B_0\left[(1+i)^3-(1+3i)\right] After B_0(3i^2+i^3)=\tfrac{151}{125} Conditions: none Rule: distributive · Uses: S05, S07 Leaf basis: distributive + power_laws + numeric_evaluation Expand (1+i)³=1+3i+3i²+i³ (N10 checks the polynomial identity) and subtract 1+3i to get 3i²+i³, the 'interest on interest' part. Substituting: 1000·(3/2500+1/125000)=6/5+1/125=151/125 (that is 1.208), agreeing with 132651/125−1060. S09 · impliesBefore i\ge -1 After \forall n\in\mathbb{N}:\ (1+i)^n\ge 1+ni Conditions: i\ge -1 Rule: L_bernoulli · Uses: L_bernoulli Leaf basis: nat_induction + order_basics + square_nonneg By Lemma L_bernoulli (proved by induction in S09.1 to S09.3). It extends the single comparison of S08 to every number of periods. S10 · impliesBefore (1+i)^n\ge 1+ni,\ B_0\ge 0 After \forall n:\ B_n\ge S_n;\ B_1=S_1=1020,\ B_3-S_3=\tfrac{151}{125}>0 Conditions: B_0\ge 0 Rule: order_basics · Uses: S03, S09, G2, G3 Leaf basis: order_basics + L_bernoulli Multiply both sides by the nonnegative B_0=1000: B_n=B_0(1+i)^n≥B_0(1+ni)=S_n for every n. For n=0 and n=1 the two are equal (B_1=S_1=1020), and for n=3 the difference is 151/125>0. So 'compound is at least simple' holds for all n, but not strictly in every period. S11 · impliesBefore 2\%\ \text{per quarter},\ 3\ \text{years}=12\ \text{quarters} After 1000\left(\tfrac{51}{50}\right)^{12}\ge 1000\left(1+\tfrac{12}{50}\right)=1240>\tfrac{132651}{125} Conditions: \text{period}=\text{quarter} Rule: mko_ci_notes · Uses: G4, S03, S09, mko_ci_notes Leaf basis: mko_ci_notes + L_bernoulli + numeric_evaluation By the MKO, the period and the number of periods must agree. If 2% is a quarterly rate, three years are 12 periods and the balance is 1000·(51/50)^12; by Bernoulli's inequality it is at least 1240, far above 1061.208 under the annual reading. The same '2%, three years' gives different answers for different periods, so the period must be fixed first. S12 · impliesBefore \text{deposit }100\ \text{at end of year 1} After (1020+100)\left(\tfrac{51}{50}\right)^2=\tfrac{145656}{125}\neq\tfrac{1459161}{1250}=1100\left(\tfrac{51}{50}\right)^3 Conditions: none Rule: mko_ci_notes · Uses: G4, S04, mko_ci_notes Leaf basis: mko_ci_notes + numeric_evaluation + power_laws Depositing 100 at the end of year 1 after interest makes the balance 1120, which then compounds at 51/50 for two years to 145656/125 (that is 1165.248). Wrongly treating the principal as 1100 in the single-power formula gives 1459161/1250 (that is 1167.3288); the two differ. With cash flows during the interval the MKO's single-power model no longer applies, and each cash flow must be tracked. S13 · impliesBefore \text{proved facts} After B_3=\tfrac{132651}{125},\ \text{interest }\tfrac{7651}{125},\ B_n\ge S_n\ \forall n Conditions: none Rule: and_intro_elim · Uses: S03, S05, S06, S07, S10, S11, S12 Leaf basis: and_intro_elim Combine the conclusions: B_n=B_0(1+i)^n; after three years the balance is 132651/125 and the interest 7651/125; simple interest gives 1060; compound is never below simple for any n; mixing periods or depositing during the interval makes the single-power formula inapplicable. These are model calculations, not investment advice or market predictions. ## Substeps and lemmas S03.1 · induction_baseBefore n=0 After B_0=B_0\cdot 1=B_0(1+i)^0 Conditions: none Rule: nat_induction · Uses: nat_power_def Leaf basis: nat_power_def + mul_one Base: (1+i)^0=1, so B_0(1+i)^0=B_0. S03.2 · induction_stepBefore B_n=B_0(1+i)^n After B_{n+1}=(1+i)B_0(1+i)^n=B_0(1+i)^{n+1} Conditions: none Rule: eq_replace · Uses: S01, nat_power_def Leaf basis: eq_replace + mul_assoc + mul_comm + nat_power_def Inductive step: assume B_n=B_0(1+i)^n. By the update rule B_(n+1)=(1+i)B_n; substitute the hypothesis and rearrange by commutativity and associativity to B_0((1+i)^n(1+i)), which by the definition of powers is B_0(1+i)^(n+1). S03.3 · impliesBefore P(0),\ \forall n\,(P(n)\Rightarrow P(n+1)) After \forall n:\ B_n=B_0(1+i)^n Conditions: none Rule: nat_induction · Uses: S03.1, S03.2 Leaf basis: nat_induction By the principle of induction it holds for all n. S03.1 to S03.3 together prove Lemma L_balance. S09.1 · induction_baseBefore n=0 After (1+i)^0=1\ge 1=1+0\cdot i Conditions: none Rule: nat_induction · Uses: nat_power_def Leaf basis: nat_power_def + mul_zero Base: both sides equal 1, so the inequality holds (with equality). S09.2 · induction_stepBefore (1+i)^n\ge 1+ni After (1+i)^{n+1}\ge(1+ni)(1+i)=1+(n+1)i+ni^2\ge 1+(n+1)i Conditions: 1+i\ge 0; n\ge 0 Rule: order_basics · Uses: nat_power_def, order_basics, square_nonneg Leaf basis: order_basics + square_nonneg + distributive Inductive step: assume (1+i)^n≥1+ni. Multiplying both sides by the nonnegative number 1+i (since i≥−1) keeps the direction: (1+i)^(n+1)=(1+i)^n(1+i)≥(1+ni)(1+i). Expanding gives 1+(n+1)i+ni² (N11), and ni²≥0 (n≥0 and squares are nonnegative), so it is ≥1+(n+1)i. S09.3 · impliesBefore P(0),\ \forall n\,(P(n)\Rightarrow P(n+1)) After \forall n:\ (1+i)^n\ge 1+ni Conditions: i\ge -1 Rule: nat_induction · Uses: S09.1, S09.2 Leaf basis: nat_induction By the principle of induction it holds for all n. S09.1 to S09.3 together prove Lemma L_bernoulli. ## 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 confusedOne 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 agreeAnother 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 modelIn 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-compound-interest-01.json)