導數：由差商極限求二次式導數並判定尖點無導數

目標與範圍

對 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|<r ⇔ −r<u<r。
• 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。
• 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、t<c 為 −1，t=c 不存在，不填 0。 · mko-derivative
• L_diff_quot · lemma — 對 f(t)=a2t²+a1t+a0、實數 x 與 h≠0：(f(x+h)−f(x))/h=2a2x+a1+a2h。
• L_lin_limit · lemma — 對實數 A、B：每個 ε>0 都有 δ>0，使 0<|h|<δ 時 |(A+Bh)−A|<ε；即 h→0 時 A+Bh→A。

逐步主鏈

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

f(1)

3\cdot 1^2-2\cdot 1+5=6

f(1+h)

3(1+h)^2-2(1+h)+5=6+4h+3h^2

f(1+h)-f(1)

4h+3h^2

\frac{4h+3h^2}{h}\ (h\neq 0)

4+3h

\varepsilon>0\ \text{arbitrary},\ \delta=\tfrac{\varepsilon}{3}

0<|h|<\delta\Rightarrow|(4+3h)-4|=3|h|<\varepsilon;\ f'(1)=4

\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

\lim_{h\to 0,\,h\neq 0}(2a_2x+a_1+a_2h)

f'(x)=2a_2x+a_1\ \text{for every real}\ x

h=\tfrac{1}{10}

Q(\tfrac{1}{10})=4+\tfrac{3}{10}=\tfrac{43}{10}\neq 4=f'(1)

e(t)=-2t+5\ (a_2=0)

\frac{e(x+h)-e(x)}{h}=-2\ (h\neq 0),\ e'(x)=-2

g(t)=|t-2|,\ t=2

\frac{g(2+h)-g(2)}{h}=\frac{|h|-0}{h}=\frac{|h|}{h}\ (h\neq 0)

\frac{|h|}{h}

1\ (h>0),\quad -1\ (h<0)

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}

t_0>2,\ 0<|h|<t_0-2

\frac{g(t_0+h)-g(t_0)}{h}=\frac{(t_0+h-2)-(t_0-2)}{h}=1;\ g'(t_0)=1

\text{a totalized API returning}\ 0\ \text{at}\ t=2

g'(2)\ \text{does not exist};\ 0\ \text{is not a limit of}\ Q

局部子步與引理

f(x+h)-f(x)

a_2(2xh+h^2)+a_1h=h(2a_2x+a_1+a_2h)

\frac{h(2a_2x+a_1+a_2h)}{h}

2a_2x+a_1+a_2h

B=0

|(A+0\cdot h)-A|=0<\varepsilon\ \text{for every}\ h

B\neq 0,\ \delta=\tfrac{\varepsilon}{|B|}

0<|h|<\delta\Rightarrow|Bh|=|B||h|<|B|\delta=\varepsilon

逐步反向審查

• 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、反控制與修訂記錄）