# 兩點間的平均變化率：資格、端點對調、仿射與二次公式 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-rate-of-change/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-rate-of-change-01 · production-20261019-adopted-96 ## 目標與範圍 （一）已知某指定函數 f 的 f(2)=7、f(−4)=3：判定資格並求平均變化率，化為最簡正分母分數，並說明同時對調兩端點不改變結果。（二）證明 f(x)=mx+b 的平均變化率為 m，並以 ℓ(x)=−3x+7 在 −2 與 4 之間核對。（三）證明 q(x)=a(x−h)²+k（a≠0）的平均變化率為 a(x₀+x₁−2h)，以 q(x)=−2(x−3)²+5 在 1 與 4 之間核對；並以對稱端點、改變第二端點與相同輸入三個情形說明它不是導數，也不能對相同輸入填 0。 在 MKO 範圍內：兩端點是同一指定函數的合法輸入且 x₀≠x₁，整數端點與係數，答案化為最簡正分母分數（a1、a2），二次切片要求 a≠0（a3）。仿射與二次公式以代數恆等式對所有合格端點證明。本稿不定義、不計算導數，只說明平均變化率不是某一點的量；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - frac_rules - distributive - mul_inverse_nonzero - neg_mul - numeric_evaluation - G1 — 定義（MKO）：對同一指定函數 f 的兩個合法輸入 x₀≠x₁，平均變化率 R=(f(x₁)−f(x₀))/(x₁−x₀)。x₀=x₁ 不符合資格，不以 0 或 0/0 代替。代表分式 (b−a)/(d−c) 中 a、b 是輸出 y₀、y₁，c、d 是輸入 x₀、x₁。 - G2 — 直接兩點題：指定函數 f 只給出 f(2)=7、f(−4)=3；取 x₀=2、x₁=−4。 - G3 — ℓ:ℝ→ℝ，ℓ(x)=−3x+7（m=−3、b=7）。 - G4 — q:ℝ→ℝ，q(x)=−2(x−3)²+5（a=−2≠0、h=3、k=5）。 - x_0,x_1 — 兩個輸入端點，x_0\neq x_1 - y_0=f(x_0),\ y_1=f(x_1) — 對應的輸出 - R(f;x_0,x_1)=\frac{y_1-y_0}{x_1-x_0} — 平均變化率 - \ell(x)=-3x+7 — 一次函數例子 - q(x)=-2(x-3)^2+5 — 二次函數例子 ## 規則與來源 - 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）。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。 - neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_rate · cited — 對已知兩個函數值 f(x0)=y0、f(x1)=y1 且 x0≠x1，兩點間平均變化率為 (y1−y0)/(x1−x0)。若 x0=x1，此商不具本條目資格，不以零或 0/0 代替。對 f(x)=mx+b，該商為 m；對 q(x)=a(x−h)²+k，該商為 a(x0+x1−2h)。 · mko-rate-of-change - diff_squares · prerequisite — 平方差：對所有實數 u、v，u²−v²=(u−v)(u+v)（由分配律展開右邊即得）。 - L_swap · lemma — 對 x₀≠x₁：(y₀−y₁)/(x₀−x₁)=(y₁−y₀)/(x₁−x₀)。 - L_linear_rate · lemma — 對 f(x)=mx+b 與 x₀≠x₁：(f(x₁)−f(x₀))/(x₁−x₀)=m。 - L_quad_rate · lemma — 對 q(x)=a(x−h)²+k 與 x₀≠x₁：(q(x₁)−q(x₀))/(x₁−x₀)=a(x₀+x₁−2h)。 ## 逐步主鏈 S01 · definition操作前 f(x_0)=y_0,\ f(x_1)=y_1 操作後 R=\frac{y_1-y_0}{x_1-x_0}\ \ \text{only if}\ x_0\neq x_1 條件：x_0\neq x_1 規則：mko_rate · 依賴：G1, mko_rate 葉節點依據：mko_rate + def_intro 依 MKO 定義平均變化率：輸出差除以輸入差。資格條件有兩個：兩端點是同一指定函數的合法輸入，且 x₀≠x₁，使分母不為零。代表分式 (b−a)/(d−c) 的 a、b 是輸出，c、d 是輸入，不與頂點式的 a、h、k 混用。 S02 · implies操作前 x_0=2,\ x_1=-4 操作後 x_1-x_0=-6\neq0 條件：無 規則：numeric_evaluation · 依賴：S01, G2 葉節點依據：numeric_evaluation 兩端點都是同一個 f 的輸入，且 −4−2=−6≠0，符合資格。分母為負並不違反資格，只需在化簡時把它轉為正分母。 S03 · equivalent操作前 R=\frac{3-7}{-4-2} 操作後 \frac{2}{3} 條件：-6\neq0 規則：frac_rules · 依賴：S02, G2 葉節點依據：frac_rules + numeric_evaluation 只用明示的輸出值 f(2)=7、f(−4)=3（MKO a1）：R=(3−7)/(−4−2)。子步 S03.1、S03.2 先算出 (−4)/(−6)，再化為最簡正分母分數 2/3。 S04 · equivalent操作前 \frac{y_0-y_1}{x_0-x_1}=\frac{7-3}{2-(-4)} 操作後 \frac{4}{6}=\frac{2}{3} 條件：x_0\neq x_1 規則：L_swap · 依賴：S03 葉節點依據：frac_rules + neg_mul 依引理 L_swap，同時對調兩個端點（分子與分母一起換號），商不變：(7−3)/(2−(−4))=4/6=2/3，與 S03 相同。證明在 S04.1。 S05 · equivalent操作前 \frac{(mx_1+b)-(mx_0+b)}{x_1-x_0} 操作後 m 條件：x_0\neq x_1 規則：L_linear_rate · 依賴：S01 葉節點依據：distributive + mul_inverse_nonzero 依引理 L_linear_rate：仿射函數在任意兩個不同輸入之間的平均變化率都是斜率 m。證明在 S05.1、S05.2；m=0 時得 0，對應常數函數。 S06 · implies操作前 \ell(-2)=13,\ \ell(4)=-5 操作後 \frac{-5-13}{4-(-2)}=\frac{-18}{6}=-3=m 條件：4\neq-2 規則：L_linear_rate · 依賴：S05, G3 葉節點依據：mko_rate + numeric_evaluation ℓ(−2)=−3·(−2)+7=13，ℓ(4)=−3·4+7=−5。直接計算 (−5−13)/(4−(−2))=−18/6=−3，與 S05 的 m=−3 一致。 S07 · equivalent操作前 \frac{q(x_1)-q(x_0)}{x_1-x_0} 操作後 a(x_0+x_1-2h) 條件：x_0\neq x_1; a\neq0 規則：L_quad_rate · 依賴：S01 葉節點依據：distributive + diff_squares + mul_inverse_nonzero 依引理 L_quad_rate：二次函數的平均變化率是 a(x₀+x₁−2h)，同時依賴兩個端點。證明在 S07.1 至 S07.3：k 抵消、平方差分解、約去 x₁−x₀。 S08 · implies操作前 q(1)=-3,\ q(4)=3 操作後 \frac{3-(-3)}{4-1}=\frac{6}{3}=2 條件：4\neq1 規則：mko_rate · 依賴：S01, G4 葉節點依據：mko_rate + numeric_evaluation q(1)=−2·(−2)²+5=−3，q(4)=−2·1²+5=3。直接計算 (3−(−3))/(4−1)=6/3=2。 S09 · implies操作前 a(x_0+x_1-2h)\ \text{at}\ a=-2,\ h=3,\ x_0=1,\ x_1=4 操作後 -2(1+4-6)=2 條件：無 規則：L_quad_rate · 依賴：S07, S08 葉節點依據：numeric_evaluation 代入公式：−2·(1+4−6)=−2·(−1)=2，與 S08 的直接計算一致。 S10 · implies操作前 x_0=1,\ x_1=5=2h-1 操作後 R=-2(1+5-6)=0,\ \text{yet}\ q(3)=5\neq-3=q(1) 條件：無 規則：L_quad_rate · 依賴：S07, G4 葉節點依據：numeric_evaluation + quantifier_negation 對稱端點 1 與 5（關於 h=3 對稱）：R=−2·0=0，直接也有 q(5)−q(1)=−3−(−3)=0。但 q 不是常數，例如 q(3)=5≠−3。平均變化率為零只說明兩端點輸出相等，不說明中間的行為。 S11 · implies操作前 x_0=1,\ x_1=2 操作後 R=-2(1+2-6)=6\neq2 條件：無 規則：L_quad_rate · 依賴：S07, S09 葉節點依據：numeric_evaluation + quantifier_negation 保持 x₀=1 而把第二端點改成 2：R=−2·(−3)=6；直接 (q(2)−q(1))/(2−1)=(3−(−3))/1=6。與 x₁=4 時的 2 不同，所以平均變化率不是只屬於 x₀=1 這一點的量；它是兩端點間的有限差商，沒有取任何極限，不能叫作導數。 S12 · implies操作前 x_0=x_1=2 操作後 x_1-x_0=0:\ \text{ineligible, no value assigned} 條件：無 規則：mko_rate · 依賴：S01, G4 葉節點依據：mko_rate + numeric_evaluation 相同輸入 x₀=x₁=2：分母 2−2=0，不符合資格。分子 q(2)−q(2)=0，形式上是 0/0，不是一個數；依 MKO 不以 0 或 0/0 代替，本條目對這組端點不給任何值。 S13 · implies操作前 \text{S02 to S12} 操作後 R=\tfrac23;\ R_{\ell}=m=-3;\ R_q=a(x_0+x_1-2h),\ R_q(1,4)=2;\ x_0=x_1\ \text{ineligible} 條件：無 規則：and_intro_elim · 依賴：S03, S04, S05, S06, S07, S09, S10, S11, S12 葉節點依據：and_intro_elim 整理：直接兩點題的平均變化率為 2/3，對調兩端點不變；仿射函數的平均變化率恆為 m；二次函數為 a(x₀+x₁−2h)，在 1 與 4 之間為 2；對稱端點可得 0 而函數非常數；改變第二端點會改變結果，所以它不是導數；相同輸入不給值。 ## 局部子步與引理 S03.1 · equivalent操作前 \frac{3-7}{-4-2} 操作後 \frac{-4}{-6} 條件：無 規則：numeric_evaluation · 依賴：S02 葉節點依據：numeric_evaluation 分子 3−7=−4，分母 −4−2=−6。 S03.2 · equivalent操作前 \frac{-4}{-6} 操作後 \frac{4}{6}=\frac{2}{3} 條件：無 規則：frac_rules · 依賴：S03.1, frac_rules 葉節點依據：frac_rules + numeric_evaluation 分子分母同乘 −1（非零）得 4/6，分母轉正；再同除 gcd(4,6)=2 得 2/3。gcd(2,3)=1，分母 3>0，是最簡正分母形式。 S04.1 · equivalent操作前 \frac{y_0-y_1}{x_0-x_1} 操作後 \frac{-(y_1-y_0)}{-(x_1-x_0)}=\frac{y_1-y_0}{x_1-x_0} 條件：x_1-x_0\neq0 規則：frac_rules · 依賴：frac_rules, neg_mul 葉節點依據：frac_rules + neg_mul y₀−y₁=−(y₁−y₀)，x₀−x₁=−(x₁−x₀)；再用 a/b=(a·(−1))/(b·(−1))（−1≠0、b≠0）。此步證得引理 L_swap。只換其中一對會使商變號。 S05.1 · equivalent操作前 (mx_1+b)-(mx_0+b) 操作後 m(x_1-x_0) 條件：無 規則：distributive · 依賴：distributive 葉節點依據：distributive + add_inverse + add_comm b 互相抵消，剩 mx₁−mx₀，再以分配律提出 m。 S05.2 · equivalent操作前 \frac{m(x_1-x_0)}{x_1-x_0} 操作後 m 條件：x_1-x_0\neq0 規則：mul_inverse_nonzero · 依賴：S05.1, mul_inverse_nonzero 葉節點依據：mul_inverse_nonzero + mul_assoc + mul_one 因 x₁−x₀≠0，可約去：m(x₁−x₀)·1/(x₁−x₀)=m。若 x₁=x₀，不能約，正是資格條件的作用。S05.1 與 S05.2 合起來證得引理 L_linear_rate。 S07.1 · equivalent操作前 q(x_1)-q(x_0) 操作後 a\bigl[(x_1-h)^2-(x_0-h)^2\bigr] 條件：無 規則：distributive · 依賴：distributive 葉節點依據：distributive + add_inverse + add_comm (a(x₁−h)²+k)−(a(x₀−h)²+k)：k 抵消（k 只平移輸出），再以分配律提出 a。 S07.2 · equivalent操作前 (x_1-h)^2-(x_0-h)^2 操作後 (x_1-x_0)(x_0+x_1-2h) 條件：無 規則：diff_squares · 依賴：S07.1, diff_squares 葉節點依據：diff_squares + distributive + add_inverse 取 u=x₁−h、v=x₀−h：u−v=x₁−x₀，u+v=x₀+x₁−2h，依平方差 u²−v²=(u−v)(u+v)。 S07.3 · equivalent操作前 \frac{a(x_1-x_0)(x_0+x_1-2h)}{x_1-x_0} 操作後 a(x_0+x_1-2h) 條件：x_1-x_0\neq0 規則：mul_inverse_nonzero · 依賴：S07.2, mul_inverse_nonzero 葉節點依據：mul_inverse_nonzero + mul_comm + mul_one 因 x₁−x₀≠0，約去該因子。S07.1 至 S07.3 合起來證得引理 L_quad_rate。這個化簡後的式子仍是兩端點間的差商，不是某一個端點的瞬時變化率。 ## 逐步反向審查 - S13 · sufficient_goal_reduction · S03, S04, S05, S06, S07, S09, S10, S11, S12, and_intro_elim — 目標 G 為 goal 的三部分；足夠條件 H 為各步結論的合取，皆已正向證成，H⇒G 只用合取引入。 - S12 · premise_audit · mko_rate, G1 — 資格條件本身就排除此情形；不宣稱任何極限或導數。 - S11 · premise_audit · S07, S09, numeric_evaluation — 只需兩個不同的值就證明它依賴第二端點；本稿不計算導數本身。 - S10 · premise_audit · S07, numeric_evaluation — 一個反例（q(3)≠q(1)）就足以否定「平均變化率為零 ⇒ 常數」。 - S09 · premise_audit · S07, numeric_evaluation — 公式由 S07 證明；兩種算法一致只是核對。 - S08 · premise_audit · mko_rate, numeric_evaluation — 資格 4≠1 成立；精確計算。 - S07.3 · inverse_equivalence · mul_inverse_nonzero — 約分可逆，前提 x₁−x₀≠0。 - S07.2 · inverse_equivalence · diff_squares, add_inverse — 平方差是恆等式，雙向成立。 - S07.1 · inverse_equivalence · distributive, add_inverse — 恆等式，雙向成立。 - S07 · inverse_equivalence · L_quad_rate — 引理由三個等式子步證成，雙向成立。 - S06 · premise_audit · S05, numeric_evaluation — 一般結論來自 S05；數值只是核對。 - S05.2 · inverse_equivalence · mul_inverse_nonzero — 乘以 (x₁−x₀) 與其倒數互逆，前提 x₁−x₀≠0。 - S05.1 · inverse_equivalence · distributive, add_inverse — 恆等式，雙向成立。 - S05 · inverse_equivalence · L_linear_rate — 引理是等式，雙向成立。 - S04.1 · inverse_equivalence · frac_rules, neg_mul — 兩條規則都是恆等式，前提只有分母非零。 - S04 · inverse_equivalence · L_swap — 引理是等式，雙向成立。 - S03.2 · inverse_equivalence · frac_rules — a/b=(ak)/(bk)（k≠0）雙向成立。 - S03.1 · inverse_equivalence · numeric_evaluation — 整數減法，可逆向核對。 - S03 · inverse_equivalence · frac_rules, numeric_evaluation — 每一步都是同一個有理數的不同寫法，雙向成立。 - S02 · premise_audit · S01, numeric_evaluation — 精確計算輸入差並與 0 比較。 - S01 · premise_audit · G1, mko_rate — 只是定義與資格條件；x₀=x₁ 時不定義任何值。 ## 錯誤控制與反例 相同輸入不能填零MKO 的誤解之一是相同輸入也把差商填 0。x₀=x₁=2 時分母為 0，商是 0/0，不是一個數；本條目規定此時不符合資格、不給值（S12）。 平均變化率不是導數另一個誤解是把平均變化率直接叫導數。從 x₀=1 出發，到 x₁=4 得 2、到 x₁=2 得 6（S11），所以它不是只屬於一點的量；對稱端點 1、5 得 0 而 q 非常數（S10）。它是有限的端點商，沒有取極限。 端點要成對一起對調(q(4)−q(1))/(1−4)=6/(−3)=−2 是錯的：只把分母的次序反過來，分子沒有一起反轉。兩者同時反轉才保持商不變（S04）。 - x₀=x₁=2 時，q 的平均變化率是 0 → reject — 分母為 0，不符合資格；0/0 不是數，不能以 0 代替。 - (q(4)−q(1))/(1−4)=−2 是 1 與 4 之間的平均變化率 → reject — 只反轉了分母；正確為 (q(4)−q(1))/(4−1)=2。 - q 在 1 與 5 之間平均變化率為 0，所以 q 在 [1,5] 上是常數 → reject — q(3)=5≠−3=q(1)。 - 只由 1 到 4 的平均變化率等於 2，未提供任何導數定義或極限證書，就已證明 q 在 x=1 的導數為 2 → reject — 本稿只算出指定兩端點的有限商；改成 x₁=2 時得到 6。這不足以作為某點導數值的證書，因此拒絕上述推論。本稿沒有計算 q′(1)，也不以「兩種程序不同」單獨證明其數值不等；仿射函數的平均變化率與導數值甚至可能相同。 ## 結論與限制 f(2)=7、f(−4)=3 時平均變化率為 (3−7)/(−4−2)=2/3，同時對調兩端點不變。f(x)=mx+b 在任意 x₀≠x₁ 之間的平均變化率為 m（ℓ 的例子為 −3）。q(x)=a(x−h)²+k 的平均變化率為 a(x₀+x₁−2h)；q(x)=−2(x−3)²+5 在 1 與 4 之間為 2，在對稱端點 1 與 5 之間為 0（而 q 非常數），在 1 與 2 之間為 6，所以它依賴兩端點、不是導數。x₀=x₁ 不符合資格，不給值，也不填 0。 - 本稿不定義也不計算導數，只證明平均變化率依賴兩端點；與導數的關係需另行處理。 - G2 的 f 只透過兩個輸出值給出，本稿沒有使用 f 的其他任何資訊。 ## 驗證及來源綁定 21 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 9fc30d6fb2c4750764240925dfd0912b58ac51b42cb81e261c6e4f836b55fb55 - original source SHA-256: c2b90bff75e0c55cc21b498fdb786490c14ae05bee992190158da4a7dd811bad - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-rate-of-change-01.json)