離散 logistic 增量模型：[0,K] 的不變性、固定點與一條短軌道

目標與範圍

對模型 G(x)=x+r x(1−x/K)（K>0、0≤r≤1），證明：若 0≤x≤K，則 0≤G(x)≤K，因此從 [0,K] 出發的整條軌道都留在 [0,K]；0 與 K 是固定點，且 r>0 時它們是僅有的固定點。再以 K=8、r=1、x0=2 精確算出 x1、x2、x3，並以 r=3 的例子說明條件 r≤1 不可省。

在 MKO 的範圍內工作：K、r 固定，初值在 [0,K]，全部計算採精確有理數（假設 a1）。證明一步不變性與固定點，並只展開三步短軌道；不由有限結果宣稱穩定、收斂或真實族群適配（假設 a2）。不討論標準 logistic map 的動力學或連續 logistic 方程的解；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• distributive
• frac_rules
• zero_product
• nat_induction
• eq_congruence
• numeric_evaluation

• G1 — 模型（MKO）：固定 K>0 與 0≤r≤1，G(x)=x+r x(1−x/K)，x_(n+1)=G(x_n)，初值 x0∈[0,K]，所有計算為精確有理數。
• G2 — 例子：K=8、r=1、x0=2。
• G3 — 對照（不滿足 r≤1）：K=8、r=3、x=6。

• K — 容量，K>0
• r — 增量比率，0≤r≤1
• G(x)=x+rx(1-\tfrac{x}{K}) — 一步更新映射
• x_n — 第 n 步狀態，x_{n+1}=G(x_n)
• [0,K] — 被證明為不變的區間

規則與來源

• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• mko_logistic · cited — 本條目的離散 logistic 增量模型固定 K>0 與 0≤r≤1，以 x_(n+1)=x_n+r x_n(1−x_n/K) 更新。若 0≤x_n≤K，則下一步仍在 [0,K]；0 與 K 是固定點。這是指定離散模型，不是連續 logistic 方程的解析解。 · mko-discrete-logistic-growth
• L_gap · lemma — 對所有實數 x 與 K>0：K·(K−G(x))=(K−x)(K−r x)。
• L_nonneg_prod · lemma — 若 u≥0 且 v≥0，則 uv≥0。

逐步主鏈

\text{discrete logistic increment model}

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

G(x)-x

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

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

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

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

G(x)\ge x\ge 0

K\cdot(K-G(x))

(K-x)(K-rx)

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

rx\le x\le K

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

G(x)\le K

0\le x\le K

0\le G(x)\le K

x_0\in[0,K]

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

G(x)=x

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

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

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

x_1=\tfrac{7}{2}

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

x_2=\tfrac{175}{32}

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

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

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

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

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

局部子步與引理

u\ge 0,\ v\ge 0

uv\ge 0

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

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

逐步反向審查

• S15 · sufficient_goal_reduction · S08, S09, S10, S14 — 目標 G：不變性與固定點定理及其假設的必要性。足夠條件 H：S08、S09、S10 與反例 S14；H⇒G 由合取。H 由代數與歸納正向證成，沒有把 G 當作前提；S13 只是例子。
• S14 · premise_audit · G3, L_gap, numeric_evaluation — 一個反例足以說明假設不可刪；不宣稱 r>1 時每個 x 都會離開區間（例如 x=0、x=K 仍固定）。
• S13 · premise_audit · numeric_evaluation, S09, S04 — 計算精確可重算；與定理一致不構成對定理的證明，定理的證明是 S03 到 S09。
• S12 · inverse_equivalence · numeric_evaluation, frac_rules — 精確分數乘法，兩邊同值。
• S11 · inverse_equivalence · numeric_evaluation, frac_rules — 精確有理數計算，兩邊同值。
• S10 · inverse_equivalence · zero_product, mul_inverse_nonzero — 乘以與除以 K≠0 互為反運算；零乘積性質是雙向的。r>0 的條件只在「僅有」這部分使用。
• S09 · premise_audit · S08, nat_induction, G1 — 歸納需要基底與步驟兩者；這只說明軌道有界，不說明它收斂或穩定。
• S08 · premise_audit · S04, S07 — 需要兩個方向的界；只證其中一個不能得到區間不變。
• S07 · premise_audit · S05, S06, L_nonneg_prod, order_basics — 需要 K>0 才能除以 K 而不改變不等號方向；兩個因子的非負性分別來自 x≤K 與 S06。
• S06 · premise_audit · L_nonneg_prod, order_basics, G1 — 需要 r≤1 與 x≥0；r>1 時 r x 可能超過 K（S14 的例子 r x=18>8）。
• S05.1 · inverse_equivalence · distributive, frac_rules — 兩邊展開成同一多項式（N2 在每變數次數 ≤2 的網格上核對），雙向成立；K/K=1 需要 K≠0。
• S05 · inverse_equivalence · L_gap — 恆等式兩邊是同一個多項式表示式，雙向成立；證明在 S05.1，N2 以多項式恆等式核對。
• S04 · premise_audit · S03, order_basics — 用加法保序與傳遞性；不宣稱 G(x)>x（例如 x=0 或 x=K 時相等）。
• S03.1 · premise_audit · order_basics, mul_zero, case_analysis — 只用乘以正數保序與乘以零；不宣稱 uv≥0 推回 u、v 都非負（兩負數之積也非負）。
• S03 · premise_audit · L_nonneg_prod, order_basics, G1 — 需要 x≤K（使 K−x≥0）、x≥0、r≥0 與 K>0；不宣稱反向。x>K 且 r>0 時，K−x<0，所以增量為負；r=0 時增量為0。
• S02 · inverse_equivalence · frac_rules, distributive — 同分母合併與拆分互為反運算，前提 K≠0（由 K>0）；N1 以本例數字交叉核對。
• S01 · premise_audit · G1, mko_logistic — 此步只陳述模型與參數條件，不推出新事實。

錯誤控制與反例

不同的 logistic 形式是不同的模型

MKO 指出的誤解之一是把不同形式的 logistic map 混為一談。標準 logistic map f(x)=μx(1−x) 在 μ=4 時 f(1)=0，所以 1 不是它的固定點；而本模型取 K=1、r=1 時 G(1)=1（N9、N10）。參數範圍也不同（本模型 0≤r≤1）。本稿的不變性與固定點結論只屬於 MKO 指定的模型。

短軌道不證穩定或收斂

MKO 指出的另一誤解。x0 到 x3 為 2、7/2、175/32、58975/8192，遞增且接近 8，但三步計算不證明收斂到 8 或 8 的穩定性，更不是對真實族群的預測（S13）。本稿證明的只有有界性（S09）與單調不減（S04）。

r≤1 用在哪一步

最容易忽略的是上界需要 r≤1：S06 由 (1−r)x≥0 得 r x≤K，才使 K−r x≥0。r=3、x=6 時 K−r x=−10，G(6)=21/2 超出 [0,8]（S14）。下界則只需要 r≥0。

• x_n 就是連續 logistic 方程 P'=rP(1−P/K) 的解在 t=n 的值 → reject — K=8、r=1、P(0)=2 時，所列連續解在 t=1 給 P(1)=8/(1+3/e)。若它等於離散的 x1=7/2，交叉相乘便需 e=7/3。此處另明示分析前提 e=Σ_(k≥0)1/k!（同離散指數成長稿的級數前提）；因各項非負，e≥1+1+1/2=5/2，而精確比較 5/2>7/3 排除該等式。這不是由 e 的無誤差界近似值推出，也不在此推導連續解。MKO 明言本模型不是連續方程的解析解。
• 對任何 r>0，[0,K] 都在 G 下不變 → reject — K=8、r=3、x=6 時 G(6)=21/2>8（S14）。
• x0 到 x3 遞增且小於 8，所以軌道收斂到 8 且 8 是穩定的 → reject — 有限軌道不能證明收斂或穩定（MKO 假設 a2）；這需要另外的論證，本稿沒有給。
• 對所有 0≤r≤1，0 與 K 是僅有的固定點 → reject — r=0 時 G(x)=x，每個點都是固定點；「僅有」需要 r>0（S10）。

結論與限制

對 K>0、0≤r≤1 的模型 G(x)=x+r x(1−x/K)：若 0≤x≤K，則 x≤G(x)≤K，因此從 [0,K] 出發的軌道永遠留在 [0,K]；0 與 K 是固定點，r>0 時沒有其他固定點。K=8、r=1、x0=2 時 x1=7/2、x2=175/32、x3=58975/8192。條件 r≤1 不可省：r=3、x=6 時 G(6)=21/2>8。

• 有界且單調不減的軌道會收斂（單調收斂定理），但本稿不引用也不證明這一點，也不討論極限是否為 K 或其穩定性；這屬於 MKO 的 formal next。
• N2 是每變數次數 ≤2 的多項式恆等式網格核對。連續解的負例比較另明示 e 的級數表示為分析前提，並用 e≥5/2>7/3 的精確有理數界；這不等於原有數值 AST 已驗證指數級數或連續解公式，兩項仍屬分析前提與另行審閱範圍。

驗證及來源綁定

12 個本稿宣告算術檢查；只支持所列算式。

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 5ca9487593862c9c09d680b93f87e15ce9161f326f0796bb9f158056f6b57ecf
• original source SHA-256: 352e71a8886bf875d0af919e31e0a2fba9471fb99e640462f4b4b2996e07fd83
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）