# 導數：由差商極限求二次式導數並判定尖點無導數 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-derivative/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-derivative-01 · production-20261019-adopted-96 ## 目標與範圍對 f(t)=3t²−2t+5：先對 h≠0 化簡差商 (f(1+h)−f(1))/h=4+3h，再以 ε-δ 證明 f'(1)=4；推導一般公式：差商為 2a2x+a1+a2h、導數為 2a2x+a1；說明有限步 h=1/10 的差商 4.3 不是導數、a2=0 的仿射邊界；最後證明 g(t)=|t−2| 在 t=2 沒有導數（不是 0），而在 t>2 處導數為 1。只處理 MKO 的範圍：全實數論域、次數至多二的多項式（允許 a2=0）與 |t−c| 的尖點。不證明一般微分法則，不處理高次多項式或其他函數。不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - distributive - frac_rules - abs_rules - order_basics - func_limit_def - numeric_evaluation - G1 — 函數 ℝ→ℝ，全實數論域；有限步 h 必須非零。 - G2 — f(t)=3t²−2t+5（a2=3、a1=−2、a0=5），求 x=1 的導數。 - G3 — 比較用：有限步 h=1/10；仿射 e(t)=−2t+5（a2=0）；尖點函數 g(t)=|t−2|。 - Q(h)=\frac{f(x+h)-f(x)}{h} — 步長 h≠0 的差商 - f'(x) — Q(h) 在 h→0（h≠0）的兩側有限極限 - a_2,a_1,a_0 — f(t)=a2t²+a1t+a0 的係數 - g(t)=|t-2| — 在 t=2 有尖點的函數 ## 規則與來源 - 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）。 - abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|v 之一；u0 推出 uwvw。 - func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - add_zero · prerequisite — 加法單位元：u+0=u。 - mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - 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 成立。所有情況必須涵蓋全部可能。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - mko_derivative · cited — 對 f:ℝ→ℝ，f 在 x 的導數是 lim_(h→0,h≠0)(f(x+h)−f(x))/h，若此兩側有限極限存在。f(t)=a2t²+a1t+a0（允許 a2=0）的導數為 2a2x+a1，有限差商為該值加 a2h；|t−c| 在 t>c 為 1、t0 都有 δ>0，使 0<|h|<δ 時 |(A+Bh)−A|<ε；即 h→0 時 A+Bh→A。 ## 逐步主鏈 S01 · definition操作前 f'(x) 操作後 f'(x)=D\iff\forall\varepsilon>0\ \exists\delta>0\ \forall h:\ 0<|h|<\delta\Rightarrow\left|\frac{f(x+h)-f(x)}{h}-D\right|<\varepsilon 條件：h\neq 0 規則：mko_derivative · 依賴：G1, func_limit_def 葉節點依據：mko_derivative + func_limit_def + def_unfold 依 MKO，導數是差商在 h→0（h≠0）的兩側有限極限。差商本身只對 h≠0 有定義；導數是極限，不是某一個有限步的差商。若極限不存在，導數就不存在。 S02 · equivalent操作前 f(1) 操作後 3\cdot 1^2-2\cdot 1+5=6 條件：無規則：numeric_evaluation · 依賴：G2 葉節點依據：numeric_evaluation 中心值 f(1)=3−2+5=6（N3）。這是差商分子中被減去的量。 S03 · equivalent操作前 f(1+h) 操作後 3(1+h)^2-2(1+h)+5=6+4h+3h^2 條件：無規則：distributive · 依賴：G2, distributive 葉節點依據：distributive + power_laws + add_comm + add_assoc (1+h)²=1+2h+h²，所以 3(1+h)²=3+6h+3h²；−2(1+h)=−2−2h；相加 3+6h+3h²−2−2h+5=6+4h+3h²（N1 以多項式恆等式核對）。 S04 · equivalent操作前 f(1+h)-f(1) 操作後 4h+3h^2 條件：無規則：eq_replace · 依賴：S02, S03 葉節點依據：eq_replace + add_inverse + add_zero 代入 S03 與 S02：(6+4h+3h²)−6=4h+3h²。 S05 · equivalent操作前 \frac{4h+3h^2}{h}\ (h\neq 0) 操作後 4+3h 條件：h\neq 0 規則：frac_rules · 依賴：S04, frac_rules 葉節點依據：frac_rules + distributive + mul_inverse_nonzero 分子 4h+3h²=h(4+3h)，對 h≠0 約去 h 得 4+3h。h=0 時差商是 0/0，沒有定義；所以不能把 h=0 直接代入原差商，只能先在 h≠0 處化簡，再看極限。 S06 · implies操作前 \varepsilon>0\ \text{arbitrary},\ \delta=\tfrac{\varepsilon}{3} 操作後 0<|h|<\delta\Rightarrow|(4+3h)-4|=3|h|<\varepsilon;\ f'(1)=4 條件：\varepsilon>0 規則：forall_intro · 依賴：S01, S05 葉節點依據：forall_intro + exists_intro + abs_rules + order_basics 取任意 ε>0，令 δ=ε/3。若 0<|h|<δ，由 S05，|Q(h)−4|=|3h|=3|h|<3δ=ε。ε 任意，依 S01，f'(1)=4。 S07 · equivalent操作前 \frac{f(x+h)-f(x)}{h},\ f(t)=a_2t^2+a_1t+a_0,\ h\neq 0 操作後 2a_2x+a_1+a_2h 條件：h\neq 0 規則：L_diff_quot · 依賴：G2 葉節點依據：distributive + frac_rules + mul_inverse_nonzero 一般化：依引理 L_diff_quot，任何二次以下多項式在任意 x 的差商都是 2a2x+a1+a2h。代入 a2=3、a1=−2、x=1 得 6−2+3h=4+3h，與 S05 一致（N6）。引理在 S07.1、S07.2 證明。 S08 · implies操作前 \lim_{h\to 0,\,h\neq 0}(2a_2x+a_1+a_2h) 操作後 f'(x)=2a_2x+a_1\ \text{for every real}\ x 條件：無規則：L_lin_limit · 依賴：S01, S07 葉節點依據：forall_intro + order_basics + abs_rules 取 A=2a2x+a1、B=a2，依引理 L_lin_limit，差商在 h→0 時趨向 2a2x+a1；依 S01，這就是 f'(x)。x 任意，所以公式對每個實數 x 成立。引理在 S08.1、S08.2 分 B=0 與 B≠0 證明。 S09 · implies操作前 h=\tfrac{1}{10} 操作後 Q(\tfrac{1}{10})=4+\tfrac{3}{10}=\tfrac{43}{10}\neq 4=f'(1) 條件：無規則：numeric_evaluation · 依賴：S05, S06, G3 葉節點依據：numeric_evaluation + frac_rules 有限步 h=1/10 的差商是 4+3/10=43/10（N4，直接由 f(1.1)、f(1) 計算），與導數 4 相差 a2h=3/10。有限差商只是平均變化率；導數是 h→0 的極限。只有當 a2h=0 時兩者才相等（見 S10）。 S10 · implies操作前 e(t)=-2t+5\ (a_2=0) 操作後 \frac{e(x+h)-e(x)}{h}=-2\ (h\neq 0),\ e'(x)=-2 條件：h\neq 0 規則：L_diff_quot · 依賴：S07, S08, G3 葉節點依據：L_diff_quot + L_lin_limit + mul_zero MKO 假設 a2 允許 a2=0（次數至多二，不必是真正的二次式）。由 S07，a2=0、a1=−2 的差商是 −2+0·h=−2，對每個 h≠0 都相同（N11）；由 S08，e'(x)=−2。這裡每個有限差商都等於導數，只因 a2h=0；這不能推廣到 a2≠0 的情形（S09）。常數 a2=a1=0 時導數為 0，也是合法的低階邊界。 S11 · equivalent操作前 g(t)=|t-2|,\ t=2 操作後 \frac{g(2+h)-g(2)}{h}=\frac{|h|-0}{h}=\frac{|h|}{h}\ (h\neq 0) 條件：h\neq 0 規則：eq_replace · 依賴：G3, abs_rules 葉節點依據：eq_replace + abs_rules g(2)=|0|=0，g(2+h)=|h|，所以差商為 |h|/h，對 h≠0 有定義。 S12 · case_split操作前 \frac{|h|}{h} 操作後 1\ (h>0),\quad -1\ (h<0) 條件：h\neq 0 規則：abs_rules · 依賴：S11, abs_rules 葉節點依據：abs_rules + case_analysis + frac_rules h>0 時 |h|=h，差商 h/h=1；h<0 時 |h|=−h，差商 −h/h=−1（N9、N10）。兩個情況涵蓋所有 h≠0。右導數 1、左導數 −1。 S13 · implies操作前 g'(2)=D\ \text{(assumed)},\ \varepsilon=\tfrac12,\ h=\pm\tfrac{\delta}{2} 操作後 |1-D|<\tfrac12,\ |-1-D|<\tfrac12\Rightarrow 2\le|1-D|+|D+1|<1:\ \text{contradiction} 條件：無規則：contradiction · 依賴：S01, S12 葉節點依據：contradiction + exists_elim + abs_rules + order_basics 反證：假設 g'(2)=D 存在。對 ε=1/2 取得 δ>0，令 h=δ/2 與 h=−δ/2，都滿足 0<|h|<δ。由 S12，|1−D|<1/2 且 |−1−D|<1/2。三角不等式：2=|1−(−1)|≤|1−D|+|D−(−1)|<1/2+1/2=1，矛盾。所以 g 在 2 沒有導數。 S14 · implies操作前 t_0>2,\ 0<|h|2 規則：abs_rules · 依賴：G3, S01 葉節點依據：abs_rules + order_basics + frac_rules t0>2 時，若 |h|2，兩個絕對值都等於裡面的式子，分子為 h（N12），差商恰為 1。所以取 δ=t0−2，對任何 ε 誤差都是 0，g'(t0)=1。同理 t0<2 時 g(t)=2−t 在 t0 附近成立，g'(t0)=−1。 S15 · implies操作前 \text{a totalized API returning}\ 0\ \text{at}\ t=2 操作後 g'(2)\ \text{does not exist};\ 0\ \text{is not a limit of}\ Q 條件：無規則：quantifier_negation · 依賴：S12, S13 葉節點依據：quantifier_negation + abs_rules 某些形式庫把導數做成全定義函數，在不可導點填預設值 0。但 0 不是差商的極限：對每個 h≠0，|Q(h)−0|=1，取 ε=1/2 就失敗。所以本條目的答案是「g'(2) 不存在」，不是 0；預設值是函數的記帳慣例，不代表導數存在。 ## 局部子步與引理 S07.1 · equivalent操作前 f(x+h)-f(x) 操作後 a_2(2xh+h^2)+a_1h=h(2a_2x+a_1+a_2h) 條件：無規則：distributive · 依賴：distributive, power_laws 葉節點依據：distributive + power_laws + add_inverse (x+h)²−x²=2xh+h²，a1(x+h)−a1x=a1h，a0 相消；提出公因子 h 得 h(2a2x+a1+a2h)（N2 以五個變數的多項式恆等式核對）。 S07.2 · equivalent操作前 \frac{h(2a_2x+a_1+a_2h)}{h} 操作後 2a_2x+a_1+a_2h 條件：h\neq 0 規則：frac_rules · 依賴：S07.1, frac_rules 葉節點依據：frac_rules + mul_inverse_nonzero h≠0，約去 h。S07.1、S07.2 合起來證得引理 L_diff_quot。 S08.1 · implies操作前 B=0 操作後 |(A+0\cdot h)-A|=0<\varepsilon\ \text{for every}\ h 條件：B=0 規則：mul_zero · 依賴：mul_zero 葉節點依據：mul_zero + add_zero + order_basics B=0 時 A+Bh=A 對每個 h 成立，誤差為 0<ε，任何 δ>0 都可以。 S08.2 · implies操作前 B\neq 0,\ \delta=\tfrac{\varepsilon}{|B|} 操作後 0<|h|<\delta\Rightarrow|Bh|=|B||h|<|B|\delta=\varepsilon 條件：|B|>0 規則：order_basics · 依賴：abs_rules, order_basics 葉節點依據：abs_rules + order_basics + mul_inverse_nonzero B≠0 時 |B|>0，令 δ=ε/|B|>0。若 0<|h|<δ，兩邊乘正數 |B| 得 |B||h|<ε。S08.1、S08.2 合起來證得引理 L_lin_limit。 ## 逐步反向審查 - S15 · premise_audit · S12, S13, quantifier_negation — 直接由 S12 的值與 S13 的不存在得出。 - S14 · premise_audit · abs_rules, S01 — 需要 h 小到不跨過 2；這說明導數不存在只發生在尖點本身。 - S13 · premise_audit · S01, S12, abs_rules, contradiction — 矛盾只否定「兩側極限存在」；兩個單側導數 1 與 −1 仍然存在。 - S12 · premise_audit · abs_rules, case_analysis — 分情況窮盡；h=0 不在考慮之內。 - S11 · inverse_equivalence · eq_replace, abs_rules — 等值代換，雙向成立。 - S10 · premise_audit · S07, S08, L_diff_quot — 直接代入一般公式；不宣稱有限差商一般等於導數。 - S09 · premise_audit · S05, S06, numeric_evaluation — N4、N5 可重算；本步不宣稱任何有限差商等於導數。 - S08.2 · premise_audit · abs_rules, order_basics — 除以 |B| 需要 B≠0，故分情況。 - S08.1 · premise_audit · mul_zero — 只需 ε>0。 - S08 · premise_audit · S01, S07, L_lin_limit — 兩個情況涵蓋所有 a2，包括 a2=0。 - S07.2 · inverse_equivalence · frac_rules, mul_inverse_nonzero — 需要 h≠0；h=0 時兩邊不能比較。 - S07.1 · inverse_equivalence · distributive, power_laws — 恆等式，雙向成立。 - S07 · inverse_equivalence · L_diff_quot — 引理給出 h≠0 時兩式相等，雙向成立。 - S06 · sufficient_goal_reduction · S01, S05, forall_intro — 目標 G：f'(1)=4。足夠條件 H：對任意 ε，δ=ε/3 有效；H⇒G 由定義。H 由 S05 正向證成，未把 G 當作前提，也未代入 h=0。 - S05 · inverse_equivalence · frac_rules, distributive — 反向是乘回 h/h，需要 h≠0；條件由 G1 保證。 - S04 · inverse_equivalence · eq_replace, add_inverse — 等值代換，雙向成立。 - S03 · inverse_equivalence · distributive, power_laws — 對所有 h 成立的恆等式，雙向成立。 - S02 · inverse_equivalence · numeric_evaluation — 精確求值，兩邊同一數。 - S01 · premise_audit · G1, mko_derivative, func_limit_def — 此步只展開定義。 ## 錯誤控制與反例區分有限差商與導數MKO 的誤解之一是把有限差商直接叫導數。h=1/10 的差商是 4.3，導數是 4，相差 a2h=0.3（S09）。仿射 e 的有限差商恰等於導數，只因 a2=0（S10）；這不能升格為一般規則。 h=0 不能代入差商另一個誤解是令 h=0 照算。原差商在 h=0 是 0/0，沒有定義。正確順序是：先在 h≠0 處化簡（S05、S07.2），再求 h→0 的極限（S06、S08）。化簡後的 4+3h 在 h=0 的值 4 恰是極限，這是由 S06 的 ε-δ 論證保證的，不是代入原式得到的。尖點不填 0|t−2| 在 2 的左右差商分別為 −1 與 1，兩側極限不存在（S13）。不能以兩者平均 0 或以全定義 API 的預設 0 冒充導數（S15）。 - (f(1.1)−f(1))/0.1=4.3，所以 f'(1)=4.3 → reject — 這是有限差商；導數是極限 4（S06、S09）。 - 在 (f(1+h)−f(1))/h 中直接令 h=0 求導數 → reject — h=0 時是 0/0，沒有定義；有限步必須非零。 - |t−2| 在 2 的左右導數 −1 與 1 平均為 0，所以 g'(2)=0 → reject — 兩側極限不存在（S13）；|Q(h)−0|=1 對所有 h≠0。 - a2=0 時 f 不是本模型的函數 → reject — MKO 允許 a2=0（次數至多二）；e(t)=−2t+5 的導數為 −2（S10）。 - |t−2| 在任何點都沒有導數 → reject — t>2 時導數為 1，t<2 時為 −1（S14）；只有 t=2 不存在。 ## 結論與限制對 h≠0，f(t)=3t²−2t+5 在 1 的差商為 4+3h，f'(1)=4（δ=ε/3）。一般地，二次以下多項式的差商為 2a2x+a1+a2h，導數為 2a2x+a1；h=1/10 的有限差商 4.3 不是導數，仿射情形 a2=0 才使有限差商等於導數。g(t)=|t−2| 在 2 的右差商為 1、左差商為 −1，所以 g'(2) 不存在（不是 0）；t>2 時 g'=1，t<2 時 g'=−1。 - 本稿只處理次數至多二的多項式與 |t−c|；一般微分法則見 mko-derivative-rules。 ## 驗證及來源綁定 12 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: a75f90a9f71b90af25dc527ee007abb8d54e43fd249e71f3a43474a0803b1085 - original source SHA-256: a75f90a9f71b90af25dc527ee007abb8d54e43fd249e71f3a43474a0803b1085 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-derivative-01.json)