# Discrete logistic increment model: invariance of [0,K], fixed points and a short orbit

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-discrete-logistic-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-logistic-growth-01 · production-20261019-adopted-96



## Goal and scope

For the model G(x)=x+r x(1−x/K) with K>0 and 0≤r≤1, prove: if 0≤x≤K then 0≤G(x)≤K, so the whole orbit starting in [0,K] stays in [0,K]; 0 and K are fixed points, and for r>0 they are the only ones. Then compute x1, x2, x3 exactly for K=8, r=1, x0=2, and use an example with r=3 to show that the condition r≤1 cannot be dropped.

Works inside the MKO's scope: K and r fixed, the initial state in [0,K], all computations in exact rationals (assumption a1). Proves one-step invariance and the fixed points and expands only a three-step orbit; infers no stability, convergence or fit to real populations from finite results (assumption a2). Neither the dynamics of the standard logistic map nor solutions of the continuous logistic equation are treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- order_basics
- distributive
- frac_rules
- zero_product
- nat_induction
- eq_congruence
- numeric_evaluation


- G1 — Model (MKO): fix K>0 and 0≤r≤1, G(x)=x+r x(1−x/K), x_(n+1)=G(x_n), initial state x0∈[0,K], all computations in exact rationals.
- G2 — Example: K=8, r=1, x0=2.
- G3 — Comparison (violating r≤1): K=8, r=3, x=6.


- K — the capacity, K>0
- r — the increment rate, 0≤r≤1
- G(x)=x+rx(1-\tfrac{x}{K}) — the one-step update map
- x_n — the state at step n, x_{n+1}=G(x_n)
- [0,K] — the interval proved to be invariant





## Rules and sources


- 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.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- 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.
- zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
- 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.
- 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_assoc · prerequisite — Associativity of multiplication: (uv)w=u(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.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
- 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.
- mko_logistic · cited — This discrete logistic increment model fixes K>0 and 0≤r≤1 and updates x_(n+1)=x_n+r*x_n*(1−x_n/K). If 0≤x_n≤K, the next state remains in [0,K]; 0 and K are fixed points. This is the specified discrete model, not an analytic solution of the continuous logistic equation. · mko-discrete-logistic-growth
- L_gap · lemma — For all real x and K>0: K·(K−G(x))=(K−x)(K−r x).
- L_nonneg_prod · lemma — If u≥0 and v≥0, then uv≥0.





## Main derivation

S01 · definitionBefore

\text{discrete logistic increment model}

After

G(x)=x+rx\left(1-\tfrac{x}{K}\right),\ K>0,\ 0\le r\le 1

Conditions: K>0; 0\le r\le 1

Rule: mko_logistic · Uses: G1, mko_logistic

Leaf basis: mko_logistic + def_intro

Fix the model specified by the MKO: the next state is the current value plus the increment r x(1−x/K). This is one particular discrete model; other maps also called 'logistic' are different models, and the conclusions here do not transfer to them (see the error controls).



S02 · equivalentBefore

G(x)-x

After

\tfrac{rx(K-x)}{K}

Conditions: K\neq 0

Rule: frac_rules · Uses: S01, frac_rules, distributive

Leaf basis: frac_rules + distributive + mul_assoc

The increment is G(x)−x=r x(1−x/K). Since K≠0, 1−x/K=K/K−x/K=(K−x)/K, so the increment equals r x(K−x)/K. This writes the increment as the product of the three factors r, x, K−x divided by the positive number K, which makes its sign easy to read.



S03 · impliesBefore

0\le x\le K,\ 0\le r,\ K>0

After

G(x)-x=\tfrac{rx(K-x)}{K}\ge 0

Conditions: 0\le x\le K; r\ge 0; K>0

Rule: L_nonneg_prod · Uses: S02, G1

Leaf basis: L_nonneg_prod + order_basics

For 0≤x≤K the three factors r≥0, x≥0 and K−x≥0 are all nonnegative. Applying Lemma L_nonneg_prod twice gives r x(K−x)≥0; multiplying by the positive number 1/K keeps the direction, so the increment is ≥0.



S04 · impliesBefore

G(x)-x\ge 0,\ x\ge 0

After

G(x)\ge x\ge 0

Conditions: none

Rule: order_basics · Uses: S03, G1

Leaf basis: order_basics

Adding x to both sides of G(x)−x≥0 gives G(x)≥x; with x≥0, transitivity gives G(x)≥0. The lower bound is proved, and it also shows that on [0,K] an update never decreases the value.



S05 · equivalentBefore

K\cdot(K-G(x))

After

(K-x)(K-rx)

Conditions: K>0

Rule: L_gap · Uses: S01

Leaf basis: distributive + frac_rules

The key identity for the upper bound (Lemma L_gap): the gap between capacity and the next state, multiplied by K, factors exactly as (K−x)(K−r x). This turns 'G(x)≤K' into a question about the signs of two factors.



S06 · impliesBefore

0\le r\le 1,\ 0\le x\le K

After

rx\le x\le K

Conditions: r\le 1; x\ge 0

Rule: order_basics · Uses: G1, order_basics

Leaf basis: order_basics + distributive + L_nonneg_prod

x−r x=(1−r)x, where 1−r≥0 (since r≤1) and x≥0, so by L_nonneg_prod (1−r)x≥0, that is r x≤x; with x≤K this gives r x≤K. This is the only place in the proof where r≤1 is used.



S07 · impliesBefore

K-x\ge 0,\ K-rx\ge 0,\ K>0

After

G(x)\le K

Conditions: K>0

Rule: L_nonneg_prod · Uses: S05, S06, L_nonneg_prod

Leaf basis: L_nonneg_prod + order_basics + L_gap

K−x≥0 (since x≤K) and K−r x≥0 (S06), so by L_nonneg_prod (K−x)(K−r x)≥0; by S05, K(K−G(x))≥0. Since K>0, multiplying by 1/K gives K−G(x)≥0, that is G(x)≤K. The upper bound is proved.



S08 · impliesBefore

0\le x\le K

After

0\le G(x)\le K

Conditions: K>0; 0\le r\le 1

Rule: and_intro_elim · Uses: S04, S07

Leaf basis: and_intro_elim

Combine the lower bound (S04) and the upper bound (S07): one-step invariance holds. This is exactly the MKO's statement 'if 0≤x_n≤K, the next state remains in [0,K]', and the proof holds uniformly for every x in the interval; it is not a finite check.



S09 · impliesBefore

x_0\in[0,K]

After

\forall n\in\mathbb{N}:\ x_n\in[0,K]

Conditions: none

Rule: nat_induction · Uses: S08, G1, nat_induction

Leaf basis: nat_induction + modus_ponens

Induction on n: the base x0∈[0,K] is given by G1; if x_n∈[0,K], then by S08 x_(n+1)=G(x_n)∈[0,K]. So the whole orbit stays in [0,K].



S10 · equivalentBefore

G(x)=x

After

rx(K-x)=0;\ G(0)=0,\ G(K)=K;\ r>0\Rightarrow x\in\{0,K\}

Conditions: K\neq 0

Rule: zero_product · Uses: S02, G1, zero_product

Leaf basis: zero_product + mul_inverse_nonzero + case_analysis

By S02, G(x)=x ⇔ r x(K−x)/K=0 ⇔ r x(K−x)=0 (multiplying or dividing by K≠0). x=0 and x=K make the product zero, so 0 and K are fixed points for every r. If r>0, the zero-product property gives r x(K−x)=0 ⇔ x=0 or x=K, so they are the only fixed points. If r=0, G(x)=x for every x and every point is fixed.



S11 · equivalentBefore

x_0=2,\ K=8,\ r=1

After

x_1=2+2\left(1-\tfrac{2}{8}\right)=\tfrac{7}{2}

Conditions: none

Rule: numeric_evaluation · Uses: G2, S01

Leaf basis: numeric_evaluation + frac_rules

With r=1, G(x)=x+x(1−x/8)=x(2−x/8). x1=2·(2−1/4)=2·7/4=7/2, all in exact fractions (N3).



S12 · equivalentBefore

x_1=\tfrac{7}{2}

After

x_2=\tfrac{7}{2}\left(2-\tfrac{7}{16}\right)=\tfrac{7}{2}\cdot\tfrac{25}{16}=\tfrac{175}{32}

Conditions: none

Rule: numeric_evaluation · Uses: S11

Leaf basis: numeric_evaluation + frac_rules

x1/8=7/16, 2−7/16=25/16, and x2=(7/2)(25/16)=175/32 (N4).



S13 · impliesBefore

x_2=\tfrac{175}{32}

After

x_3=\tfrac{175}{32}\cdot\tfrac{337}{256}=\tfrac{58975}{8192};\ 2<\tfrac{7}{2}<\tfrac{175}{32}<\tfrac{58975}{8192}<8

Conditions: none

Rule: numeric_evaluation · Uses: S12, S09, S04

Leaf basis: numeric_evaluation + frac_rules + order_basics

x2/8=175/256, 2−175/256=337/256, and x3=(175/32)(337/256)=58975/8192 (N5, N6), about 7.199 and below 8 (N7). All four values lie in [0,8] and increase, consistent with S09 (staying in the interval) and S04 (G(x)≥x). These three steps are only an example of consistency; they prove neither that the orbit converges to 8 nor that 8 is stable (MKO assumption a2).



S14 · impliesBefore

K=8,\ r=3,\ x=6

After

G(6)=6+3\cdot 6\cdot\tfrac{1}{4}=\tfrac{21}{2}>8

Conditions: r=3>1

Rule: numeric_evaluation · Uses: G3, S05

Leaf basis: numeric_evaluation + L_gap

The condition r≤1 cannot be dropped: with r=3, r x=18>8=K and S06 fails; L_gap gives 8(8−G(6))=(8−6)(8−18)=−20, so G(6)=8+20/8=21/2>8, which leaves [0,8]. This concrete counterexample shows that S08 depends on r≤1.



S15 · impliesBefore

\text{model with}\ K>0,\ 0\le r\le 1

After

G([0,K])\subseteq[0,K],\ \mathrm{Fix}\supseteq\{0,K\}\ (=\{0,K\}\ \text{if}\ r>0)

Conditions: none

Rule: and_intro_elim · Uses: S08, S09, S10, S13, S14

Leaf basis: and_intro_elim

Summary: [0,K] is invariant under G (S08), so an orbit starting in [0,K] stays there forever (S09); 0 and K are fixed points, and the only ones when r>0 (S10); the example orbit 2, 7/2, 175/32, 58975/8192 agrees with these conclusions (S13); and r≤1 cannot be dropped (S14).







## Substeps and lemmas

S03.1 · impliesBefore

u\ge 0,\ v\ge 0

After

uv\ge 0

Conditions: none

Rule: order_basics · Uses: order_basics, mul_zero

Leaf basis: order_basics + mul_zero + case_analysis

Two cases: if v=0, uv=u·0=0≥0; if v>0, from u≥0, that is 0≤u, multiplying by the positive v gives 0·v≤uv, that is 0≤uv (with equality if u=0). The two cases cover every possibility for v≥0. This proves Lemma L_nonneg_prod.



S05.1 · equivalentBefore

K\cdot G(x)=Kx+rx(K-x)

After

K(K-G(x))=K^2-Kx-rKx+rx^2=(K-x)(K-rx)

Conditions: K\neq 0

Rule: distributive · Uses: S01, distributive, frac_rules

Leaf basis: distributive + add_comm + mul_comm + frac_rules

By S02, K·G(x)=Kx+K·r x(K−x)/K=Kx+r x(K−x). So K(K−G(x))=K²−Kx−rKx+r x². On the other hand (K−x)(K−r x)=K²−rKx−Kx+r x², the same expression. This proves Lemma L_gap.







## Reverse audits


- S15 · sufficient_goal_reduction · S08, S09, S10, S14 — Goal G: the invariance and fixed-point theorem and the necessity of its hypothesis. Sufficient condition H: S08, S09, S10 and the counterexample S14; H⇒G by conjunction. H is proved forwards by algebra and induction; G is never used as a premise, and S13 is only an example.
- S14 · premise_audit · G3, L_gap, numeric_evaluation — One counterexample suffices to show the hypothesis cannot be removed; it is not claimed that every x leaves the interval when r>1 (for example x=0 and x=K stay fixed).
- S13 · premise_audit · numeric_evaluation, S09, S04 — The computation is exact and can be redone; agreement with the theorem is not a proof of it, which is S03 to S09.
- S12 · inverse_equivalence · numeric_evaluation, frac_rules — Exact fraction multiplication; both sides have the same value.
- S11 · inverse_equivalence · numeric_evaluation, frac_rules — Exact rational computation; both sides have the same value.
- S10 · inverse_equivalence · zero_product, mul_inverse_nonzero — Multiplying and dividing by K≠0 undo each other; the zero-product property is two-way. The condition r>0 is used only for the 'only' part.
- S09 · premise_audit · S08, nat_induction, G1 — The induction needs both base and step; it shows only that the orbit is bounded, not that it converges or is stable.
- S08 · premise_audit · S04, S07 — Both bounds are needed; proving only one does not give invariance of the interval.
- S07 · premise_audit · S05, S06, L_nonneg_prod, order_basics — K>0 is needed to divide by K without reversing the inequality; the nonnegativity of the two factors comes from x≤K and S06.
- S06 · premise_audit · L_nonneg_prod, order_basics, G1 — It needs r≤1 and x≥0; for r>1, r x can exceed K (the example in S14 has r x=18>8).
- S05.1 · inverse_equivalence · distributive, frac_rules — Both sides expand to the same polynomial (N2 checks it on the grid for degree ≤2 per variable), so the step holds both ways; K/K=1 needs K≠0.
- S05 · inverse_equivalence · L_gap — Both sides are the same polynomial expression, so the step holds both ways; the proof is in S05.1, and N2 checks it as a polynomial identity.
- S04 · premise_audit · S03, order_basics — It uses that addition preserves order and transitivity; it does not claim G(x)>x (equality holds, for example, at x=0 and x=K).
- S03.1 · premise_audit · order_basics, mul_zero, case_analysis — Only that multiplying by a positive number preserves order and multiplying by zero gives zero; it is not claimed that uv≥0 forces u, v≥0 (a product of two negatives is also nonnegative).
- S03 · premise_audit · L_nonneg_prod, order_basics, G1 — It needs x≤K (so K−x≥0), x≥0, r≥0 and K>0; no converse is claimed. For x>K and r>0, K−x<0 makes the increment negative; when r=0, the increment is 0.
- S02 · inverse_equivalence · frac_rules, distributive — Combining and splitting over a common denominator undo each other given K≠0 (from K>0); N1 cross-checks with the example's numbers.
- S01 · premise_audit · G1, mko_logistic — This step only states the model and the parameter conditions and derives no new fact.





## Error controls and negative controls

Different logistic forms are different modelsOne mistake named by the MKO is to treat different logistic maps as one model. The standard logistic map f(x)=μx(1−x) with μ=4 has f(1)=0, so 1 is not a fixed point of it; whereas this model with K=1, r=1 has G(1)=1 (N9, N10). The parameter ranges differ too (here 0≤r≤1). The invariance and fixed-point results of this guide belong only to the model specified by the MKO.

A short orbit proves no stability or convergenceThe other mistake named by the MKO. x0 to x3 are 2, 7/2, 175/32 and 58975/8192, increasing and moving closer to 8 over these three steps, but three computed steps prove neither convergence to 8 nor stability of 8, and they are no forecast for a real population (S13). What this guide proves is boundedness (S09) and that updates do not decrease the value (S04).

Where r≤1 is usedThe easiest thing to overlook is that the upper bound needs r≤1: S06 uses (1−r)x≥0 to get r x≤K, which makes K−r x≥0. With r=3 and x=6, K−r x=−10 and G(6)=21/2 lies outside [0,8] (S14). The lower bound needs only r≥0.


- x_n is the value at t=n of the solution of the continuous logistic equation P'=rP(1−P/K) → reject — For K=8, r=1 and P(0)=2, the stated continuous solution gives P(1)=8/(1+3/e). Equality with the discrete x1=7/2 would require e=7/3 by cross-multiplication. An analytic premise is made explicit here: e=Σ_(k≥0)1/k!, as in the exponential-growth guide's series premise. Nonnegative terms give e≥1+1+1/2=5/2, and the exact comparison 5/2>7/3 rules out equality. This is not an inference from an approximate decimal with no error bound, and the continuous solution is not derived here. The MKO states that this model is not an analytic solution of the continuous equation.
- For every r>0, [0,K] is invariant under G → reject — With K=8, r=3, x=6, G(6)=21/2>8 (S14).
- x0 to x3 increase and stay below 8, so the orbit converges to 8 and 8 is stable → reject — A finite orbit cannot prove convergence or stability (MKO assumption a2); that needs a separate argument, which this guide does not give.
- For every 0≤r≤1, 0 and K are the only fixed points → reject — With r=0, G(x)=x and every point is fixed; 'only' needs r>0 (S10).





## Result and limitations

For the model G(x)=x+r x(1−x/K) with K>0 and 0≤r≤1: if 0≤x≤K then x≤G(x)≤K, so an orbit starting in [0,K] stays in [0,K] forever; 0 and K are fixed points, and for r>0 there are no others. For K=8, r=1, x0=2: x1=7/2, x2=175/32, x3=58975/8192. The condition r≤1 cannot be dropped: with r=3 and x=6, G(6)=21/2>8.


- A bounded nondecreasing orbit converges (monotone convergence theorem), but this guide neither cites nor proves that, nor discusses whether the limit is K or its stability; this belongs to the MKO's formal next step.
- N2 is a polynomial-identity grid check with degree ≤2 per variable. The continuous-solution contrast separately declares the exponential-series representation as an analytic premise and uses the exact rational bound e≥5/2>7/3. The original numeric AST does not thereby verify that series representation or the continuous solution formula; those remain analytic premises subject to separate review.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 5ca9487593862c9c09d680b93f87e15ce9161f326f0796bb9f158056f6b57ecf
- original source SHA-256: 352e71a8886bf875d0af919e31e0a2fba9471fb99e640462f4b4b2996e07fd83
- 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-logistic-growth-01.json)