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

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

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

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

r^n

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

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

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

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

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

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

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

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

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

y_n=x_0\,r^n

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

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

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

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

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

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

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

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

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

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

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

\text{proved facts}

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

Substeps and lemmas

n=0

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

x_n=x_0\,r^n

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

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

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

12=r\cdot 8

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

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

x_3=27\neq 26=d_3

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 forever

One 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 rate

Another 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 r

The 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)