# Discrete exponential growth: proving x_n=x_0·r^n from x_(n+1)=r·x_n by induction

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-discrete-exponential-growth/)

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-discrete-exponential-growth-01 · production-20261019-adopted-96



## Goal and scope

In the model x_(n+1)=r·x_n with a fixed time step and constant factor r≥0, prove by induction that x_n=x_0·r^n for every natural number n, and explain that the recurrence and the closed form describe the same sequence; with x_0=8 and r=3/2 compute x_1 to x_4 and compare with the closed form; describe the behaviour for r>1, r=1, 0≤r<1 and x_0=0; decide that the data 8, 12, 18, 26 fit no fixed-factor model starting at x_0=8; and explain why the per-step factor 3/2 is not the continuous growth rate 1/2.

Algebra within the specified model only (MKO assumptions a1 and a2): initial values and factors are exact rationals, and r stays constant throughout. The conclusions are algebraic results within the model, not proof that data fit the model and not empirical forecasts of a biological population. S12 uses only a series lower bound for the exponential function to show that a discrete factor differs from a continuous rate; no continuous-time model is built. The canonical MKO and its English edition are not changed.





## Givens and symbols


- nat_induction
- eq_congruence
- mul_assoc
- mul_comm
- forall_elim


- G1 — Time steps are fixed, n starts at 0, and the factor r stays constant throughout (MKO assumption a1).
- G2 — Model: x_(n+1)=r·x_n for every natural number n; x_0 and r are exact rationals with r≥0 (assumption a2).
- G3 — Main instance: x_0=8, r=3/2. Comparison instances: x_0=8, r=1/2; and x_0=0.
- G4 — Given observed data: d_0=8, d_1=12, d_2=18, d_3=26.


- x_n — the quantity at time step n
- r — the constant factor per step, r≥0
- x_0 — the initial value
- r^n — natural-number power, r^0=1, r^(n+1)=r^n·r
- d_0,d_1,d_2,d_3 — the given observed data





## 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_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- 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_one · prerequisite — Multiplicative identity: 1·u=u.
- 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.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- 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.
- iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- 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.
- 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.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- 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.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_exp_model · cited — Fix a time step and a nonnegative constant r. The discrete exponential model is x_(n+1)=r*x_n. From initial x_0, repeated substitution or induction gives x_n=x_0*r^n. This is an algebraic result within the specified model, not proof that observed data fit it. · mko-discrete-exponential-growth
- mko_exp_cases · cited — Independent append-only source erratum (owner-adopted in this local revision; not merged or published): r>1 multiplies each step by a fixed factor greater than 1, not necessarily by 2. Nonzero magnitudes increase; positive state values increase and negative state values decrease. For r=1 values stay fixed; for 0<r<1 nonzero magnitudes shrink; for r=0 states are zero from the first step onward. A zero initial state stays zero. The original citation and canonical MKO are preserved unchanged. · mko-discrete-exponential-growth
- nat_power_def · prerequisite — Recursive definition of natural-number powers: for every rational r, r^0=1 and r^(n+1)=r^n·r (so 0^0=1 is part of this definition).
- exp_lower_bound · prerequisite — For u≥0 every term of eᵘ=Σ_(k≥0) uᵏ/k! is nonnegative, so eᵘ≥1+u+u²/2.
- L_closed_form · lemma — In the model G2, x_n=x_0·r^n for every natural number n.





## Main derivation

S01 · definitionBefore

\text{fixed step, constant factor }r\ge 0

After

x_{n+1}=r\,x_n\ (n\in\mathbb{N}),\ x_0\ \text{given}

Conditions: r\ge 0

Rule: mko_exp_model · Uses: G1, G2

Leaf basis: mko_exp_model + def_intro

State the model as in the MKO: each step multiplies the current quantity by the same nonnegative factor r. G1 requires fixed steps and an r that does not change over time; these are assumptions of the model, not conclusions from any data.



S02 · definitionBefore

r^n

After

r^0=1,\ r^{n+1}=r^n\cdot r

Conditions: none

Rule: nat_power_def · Uses: nat_power_def

Leaf basis: nat_power_def + def_intro

Make the meaning of powers precise: r^n is the product of n copies of r, defined formally by recursion. The definition also applies to r=0, so 0^0=1 and the closed form makes sense when r=0.



S03 · impliesBefore

x_{n+1}=r\,x_n,\ x_0

After

\forall n\in\mathbb{N}:\ x_n=x_0\,r^n

Conditions: none

Rule: L_closed_form · Uses: S01, S02, L_closed_form

Leaf basis: nat_induction + nat_power_def + mul_assoc + mul_comm

By Lemma L_closed_form (proved by induction in S03.1 to S03.3), the recurrence implies the closed form for all n, not just for the few terms that were computed.



S04 · impliesBefore

\forall n:\ x_n=x_0\,r^n

After

x_n=8\left(\tfrac{3}{2}\right)^n

Conditions: x_0=8,\ r=\tfrac{3}{2}\ge 0

Rule: forall_elim · Uses: S03, G3

Leaf basis: forall_elim

The lemma holds for any x_0 and r≥0; substituting the main instance x_0=8, r=3/2 gives x_n=8·(3/2)^n.



S05 · impliesBefore

x_0=8,\ x_{n+1}=\tfrac{3}{2}x_n

After

x_1=12,\ x_2=18,\ x_3=27,\ x_4=\tfrac{81}{2}

Conditions: none

Rule: numeric_evaluation · Uses: G2, G3

Leaf basis: numeric_evaluation + eq_replace

Compute step by step from the recurrence: 8·3/2=12, 12·3/2=18, 18·3/2=27, 27·3/2=81/2.



S06 · equivalentBefore

8\left(\tfrac{3}{2}\right)^4

After

8\cdot\tfrac{81}{16}=\tfrac{81}{2}=x_4

Conditions: none

Rule: power_laws · Uses: S04, S05

Leaf basis: power_laws + frac_rules + numeric_evaluation

The closed form at n=4: (3/2)^4=81/16 and 8·81/16=81/2, agreeing with the recursive computation of S05. This is a numerical cross-check of S03, not its proof.



S07 · equivalentBefore

y_n=x_0\,r^n

After

y_0=x_0,\ y_{n+1}=r\,y_n

Conditions: none

Rule: nat_power_def · Uses: S03, S02

Leaf basis: nat_power_def + mul_assoc + mul_comm + iff_intro

The other direction: the closed-form sequence y_n=x_0·r^n satisfies the recurrence with the same initial value, since y_0=x_0·1=x_0 and y_(n+1)=x_0·r^n·r=r·y_n. Together with S03 (any sequence satisfying the recurrence and initial value equals the closed form), the recurrence with initial value and the closed form describe the same sequence, both ways, which is the equivalence in the MKO's second paragraph.



S08 · impliesBefore

x_{n+1}-x_n=(r-1)x_n,\ r=\tfrac{3}{2}

After

x_{n+1}-x_n=\tfrac{1}{2}x_n>0

Conditions: x_n=8(\tfrac{3}{2})^n>0

Rule: mko_exp_cases · Uses: S04, mko_exp_cases

Leaf basis: distributive + order_basics + mko_exp_cases

x_(n+1)−x_n=r·x_n−x_n=(r−1)x_n. In the main instance r−1=1/2, and x_n=8·(3/2)^n is a product of positive numbers, so x_n>0; hence each step strictly increases, and the increment itself is proportional to x_n: this is the 'growth by a factor' of r>1.



S09 · impliesBefore

x_0=8,\ r=\tfrac{1}{2}

After

x_n=8\left(\tfrac{1}{2}\right)^n:\ 8,4,2,1,\tfrac{1}{2};\ x_{n+1}-x_n=-\tfrac{1}{2}x_n<0

Conditions: 0\le r<1

Rule: mko_exp_cases · Uses: S03, G3, mko_exp_cases

Leaf basis: L_closed_form + order_basics + mko_exp_cases

Comparison instance r=1/2: by L_closed_form, x_n=8·(1/2)^n, with first five terms 8, 4, 2, 1, 1/2; x_(n+1)−x_n=(1/2−1)x_n=−x_n/2<0, halving at each step. This is the shrinking case 0≤r<1. The general classification does not add an assumption x0≥0: by the closed form, for r>0, x_n has the sign of x0 and x_(n+1)−x_n=(r−1)x_n. Thus for r>1 the sequence strictly increases when x0>0 and strictly decreases when x0<0; its magnitude grows by the factor r for nonzero x0. For 0<r<1 the magnitude shrinks, with positive initial values decreasing and negative initial values increasing. For r=0, x1 and all later values are 0. The constant cases r=1 and x0=0 are handled in S10.



S10 · impliesBefore

r=1\ \text{or}\ x_0=0

After

r=1:\ x_n=x_0;\ \ x_0=0:\ x_n=0\cdot r^n=0

Conditions: none

Rule: mko_exp_cases · Uses: S03, mko_exp_cases

Leaf basis: L_closed_form + mul_zero + mul_one

For r=1, 1^n=1, so x_n=x_0 and the sequence is constant. For x_0=0 and any r≥0 (including r=0, with 0^0=1 by definition), x_n=0·r^n=0, so the sequence is all zeros.



S11 · impliesBefore

d=(8,12,18,26),\ \text{fixed-}r\ \text{model with }x_0=8

After

r=\tfrac{3}{2}\ \text{forced},\ x_3=27\neq 26:\ \text{no fixed-}r\ \text{model fits}

Conditions: d_0=8\neq 0

Rule: contradiction · Uses: G4, S03

Leaf basis: contradiction + mul_inverse_nonzero + L_closed_form

Assume some fixed-factor model x_(n+1)=r·x_n with x_0=8 matches all four data. From x_1=12=r·8 and 8≠0, r=12/8=3/2 (S11.1). By L_closed_form the model gives x_3=8·(3/2)^3=27, but d_3=26, a contradiction (S11.2). So no fixed-r model matches all four data. The first three data have ratios 3/2, which looks like a fixed factor, but that does not determine the fourth period.



S12 · impliesBefore

r=\tfrac{3}{2}\ \text{per step},\ \text{continuous }x(t)=x_0e^{kt}

After

e^{k}=\tfrac{3}{2}\ \text{needed};\ e^{1/2}\ge\tfrac{13}{8}>\tfrac{3}{2},\ \text{so }k\neq\tfrac{1}{2}

Conditions: u=\tfrac{1}{2}\ge 0

Rule: exp_lower_bound · Uses: G1, exp_lower_bound

Leaf basis: exp_lower_bound + order_basics

A per-step factor 3/2 means a 50% increase per step. For the worked nonzero initial state x_0=8, agreement of x(t)=x_0·e^(kt) with the model at integer times permits cancellation of x_0 at time 1, giving e^k=3/2. If x_0=0 both trajectories are zero and their agreement does not determine k; the following factor comparison concerns the nonzero trajectory. Taking the 50% directly as the continuous rate k=1/2 is wrong: by the series bound e^(1/2)≥1+1/2+1/8=13/8, and 13/8>3/2, so e^(1/2)≠3/2. A discrete factor and a continuous growth rate are different quantities; no continuous model is built here.



S13 · impliesBefore

\text{proved facts}

After

x_n=x_0r^n\ \forall n;\ x_4=\tfrac{81}{2};\ \text{data }(8,12,18,26)\ \text{fit no fixed }r

Conditions: none

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

Leaf basis: and_intro_elim

Combine the conclusions: in the model x_n=x_0·r^n for all n, equivalent to the recurrence; in the main instance x_4=81/2; for nonzero initial values the magnitude grows when r>1 and shrinks when 0<r<1, with the numerical monotonicity depending on the initial sign; r=0 gives zero from the first step, r=1 is constant, and x_0=0 stays zero; the data 8, 12, 18, 26 fit no fixed-factor model; the per-step factor is not a continuous rate.







## Substeps and lemmas

S03.1 · induction_baseBefore

n=0

After

x_0=x_0\cdot 1=x_0\,r^0

Conditions: none

Rule: nat_induction · Uses: S02

Leaf basis: nat_power_def + mul_one

Base: let P(n) be x_n=x_0·r^n. Since r^0=1 and x_0·1=x_0, P(0) holds.



S03.2 · induction_stepBefore

x_n=x_0\,r^n

After

x_{n+1}=r\,x_n=r\,(x_0\,r^n)=x_0\,(r^n\cdot r)=x_0\,r^{n+1}

Conditions: none

Rule: eq_replace · Uses: S01, S02

Leaf basis: eq_replace + mul_assoc + mul_comm + nat_power_def

Inductive step: assume P(n). By the recurrence x_(n+1)=r·x_n; replace x_n by x_0·r^n, rearrange by commutativity and associativity of multiplication to x_0·(r^n·r), which by the definition of powers is x_0·r^(n+1); so P(n+1) holds.



S03.3 · impliesBefore

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

After

\forall n\in\mathbb{N}:\ x_n=x_0\,r^n

Conditions: none

Rule: nat_induction · Uses: S03.1, S03.2

Leaf basis: nat_induction

By the principle of induction, P(n) holds for every natural number n. S03.1 to S03.3 together prove Lemma L_closed_form.



S11.1 · equivalentBefore

12=r\cdot 8

After

r=\tfrac{12}{8}=\tfrac{3}{2}

Conditions: 8\neq 0

Rule: mul_inverse_nonzero · Uses: G4, G2

Leaf basis: mul_inverse_nonzero + eq_congruence + frac_rules

Multiply both sides by 1/8 (since 8≠0): r=12/8=3/2.



S11.2 · impliesBefore

x_3=8\left(\tfrac{3}{2}\right)^3

After

x_3=27\neq 26=d_3

Conditions: none

Rule: numeric_evaluation · Uses: S11.1, S03, G4

Leaf basis: numeric_evaluation + power_laws

8·27/8=27, while d_3=26; the numbers differ, contradicting the assumption that the model fits the data. Also d_3/d_2=26/18=13/9≠3/2, showing that the ratio at the third step differs.







## Reverse audits


- S13 · sufficient_goal_reduction · S03, S07, S08, S09, S10, S11, S12, and_intro_elim — Goal G: the determinations in the goal. Sufficient condition H: S03 and S07 to S12, 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 · exp_lower_bound, order_basics — It needs only the lower bound for e^u and a rational comparison; this step proves only k≠1/2 and does not compute k.
- S11.2 · premise_audit · numeric_evaluation, S11.1 — Exact computation; one mismatching data point suffices to rule out the fixed-factor model.
- S11.1 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — Multiplying by 1/8 and by 8 undo each other, so both directions hold.
- S11 · premise_audit · S03, contradiction, mul_inverse_nonzero — Solving for r needs d_0≠0; the conclusion rules out only fixed-r models starting at x_0=8, not other models (such as a time-varying r).
- S10 · premise_audit · S03, mul_zero, mko_exp_cases — Both special cases are substitutions into L_closed_form; they use that powers of 1 are 1 and that multiplying by zero gives zero.
- S09 · premise_audit · S03, mko_exp_cases, order_basics — In the positive-initial-value instance x0=8, r=1/2, every value is positive and the sequence never reaches 0 in finitely many steps. The general sign classification follows separately from the closed form and the difference identity; r=0 reaches 0 at the first step.
- S08 · premise_audit · S04, distributive, order_basics, mko_exp_cases — It needs x_n>0; with x_0=0 there is no growth even when r>1 (S10).
- S07 · inverse_equivalence · nat_power_def, S03, mul_assoc, mul_comm — One direction is S03 and the other is the direct substitution in this step; both directions have reasons.
- S06 · inverse_equivalence · power_laws, frac_rules, numeric_evaluation — Exact rational arithmetic; both sides are the same number.
- S05 · premise_audit · G2, numeric_evaluation — Each term is determined by the previous one, with exact rational arithmetic; these four terms are not claimed to prove the closed form by themselves.
- S04 · premise_audit · S03, forall_elim — Universal instantiation needs only that the substituted values meet the conditions, r=3/2≥0.
- S03.3 · premise_audit · S03.1, S03.2, nat_induction — The two premises come from S03.1 and S03.2, with n arbitrary in the inductive step.
- S03.2 · premise_audit · G2, eq_replace, mul_assoc, mul_comm, nat_power_def — It needs the recurrence at this n, the inductive hypothesis and commutativity and associativity of multiplication; r must not depend on n, or the first equality would fail.
- S03.1 · premise_audit · nat_power_def, mul_one — It uses only r^0=1 and the multiplicative identity; it also holds for r=0.
- S03 · premise_audit · L_closed_form — It depends on the lemma, which uses only the recurrence of G2 and the definition of powers.
- S02 · premise_audit · nat_power_def — Only a definition is introduced; no new fact is derived.
- S01 · premise_audit · G1, G2, mko_exp_model — This step only states the model and derives no new fact; all later conclusions hold within this model only.





## Error controls and negative controls

A few periods of growth do not make the factor fixed foreverOne misconception named by the MKO: the data 8, 12, 18 have ratios 3/2, but the fourth value is 26, not 27 (S11). L_closed_form is an algebraic result under the assumption that r is fixed; whether data fit the model must be checked separately, and the model itself proves no fit.

A discrete factor is not a continuous rateAnother misconception named by the MKO: treating the per-step factor 3/2 (a 50% increase) as a continuous rate k=1/2 gives a per-step factor e^(1/2)≥13/8, larger than 3/2 (S12). The two need an explicit conversion and cannot be swapped directly.

The inductive step needs the same rThe first equality in S03.2 uses x_(n+1)=r·x_n with r independent of n. If the factor changes with time (r_n), the product is r_0·r_1 and so on up to r_(n−1), no longer r^n; checking the closed form at a few values cannot replace the induction.


- 8, 12, 18 each multiply by 3/2, so the fourth period must be 27 → reject — The given fourth value is 26; a fixed factor is a model assumption that data need not obey (S11).
- A per-step factor 3/2 equals a continuous growth rate 1/2 → reject — e^(1/2)≥13/8>3/2, so k=1/2 gives a per-step factor larger than 3/2 (S12).
- Since the closed form matches the recurrence for n=0 to 4, x_n=8·(3/2)^n has been proved for all n → reject — Finitely many numerical checks cannot prove a universal statement; the proof is the induction of S03.
- r=3/2>1, so the sequence grows whatever the initial value → reject — With x_0=0, x_n=0 for every n (S10).





## Result and limitations

In the model x_(n+1)=r·x_n with fixed r≥0, induction proves x_n=x_0·r^n for all n, and the closed form also satisfies the recurrence, so both describe the same sequence. With x_0=8 and r=3/2, x_1 to x_4 are 12, 18, 27, 81/2, agreeing with the closed form. For nonzero initial values the magnitude grows when r>1 and shrinks when 0<r<1; the numerical sequence respectively increases or decreases for a positive initial value, with opposite directions for a negative one. For r=0 it is zero from the first step, for r=1 it is constant, and for x_0=0 it stays zero. The data 8, 12, 18, 26 force r=3/2 but contradict the prediction x_3=27, so they fit no fixed-factor model starting at 8. The per-step factor 3/2 is not the continuous growth rate 1/2, since e^(1/2)≥13/8>3/2.


- N6 is a finite check for n=0 to 20 only; the closed form for all n is proved by the induction of S03.
- Logistic models, time-varying factors and model calibration belong to the MKO's formal next step.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: d241eac2e24aeedd4c822c1586a4997617fbe5ca988f7a3c508da4081980817f
- original source SHA-256: 31bb4abc1099f94cff294e388d438434f5734c98c44377638bc50ff98ef5d26e
- 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-discrete-exponential-growth-01.json)