# 微分法則：以展開求導核對乘積與鏈式規則

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-derivative-rules/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-derivative-rules-01 · production-20261019-adopted-96



## 目標與範圍

以升冪係數列表 f=[2,0,1]、g=[1,3]（即 f(x)=2+x²、g(x)=1+3x）：先由導數定義證明三次以下多項式的求導公式；再以兩條獨立路徑求 (fg)' 與 (f∘g)'——展開後求導，以及使用乘積、鏈式規則——並確認兩者對每個 x 相同；同時核對和與純量倍的規則，指出 f'g'、漏乘內導數、外導數取錯點、反讀係數等錯誤，最後求 x=1 的值。

只處理 MKO 的多項式切片（輸入至多三次、升冪列表）。和、純量倍、乘積、鏈式規則本身引自 MKO，本稿只對這組 f、g 以多項式恆等式核對它們，並由定義證明三次以下多項式的求導公式；不證明一般可微函數的規則。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- distributive
- power_laws
- abs_rules
- order_basics
- frac_rules
- composition_def
- numeric_evaluation


- G1 — 多項式以升冪係數列表表示：[a0,a1,a2,a3] 表示 a0+a1x+a2x²+a3x³；末端零正規化；全實數論域。
- G2 — f=[2,0,1]，g=[1,3]。
- G3 — 純量 c=−4；求值點 x=1。


- [a_0,a_1,a_2,a_3] — 升冪係數列表 a0+a1x+a2x²+a3x³
- f',\ g' — f、g 的導函數
- fg,\ f\circ g — 乘積與合成 f(g(x))
- R,\ M — 差商的餘項與其界





## 規則與來源


- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- 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。
- 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）。
- composition_def · prerequisite — 合成：對 f:A→B 與 g:B→C，g∘f:A→C 定義為 (g∘f)(a)=g(f(a))。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- 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 成立。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_deriv_rules · cited — 在相應點可微的實函數有 (f+g)'=f'+g'、(cf)'=cf'、(fg)'=f'g+fg'；若 g 在 x 可微且 f 在 g(x) 可微，(f∘g)'(x)=f'(g(x))g'(x)。本輪 f、g 是全 ℝ 多項式，以常數項起算的升冪係數列表表示。 · mko-derivative-rules
- mko_derivative_def · cited — 對 f:ℝ→ℝ，f 在 x 的導數是 lim_(h→0,h≠0)(f(x+h)−f(x))/h，若此兩側有限極限存在。 · mko-derivative
- L_poly_deriv3 · lemma — 對 p(x)=c0+c1x+c2x²+c3x³（實係數）與每個實數 x：p 在 x 可微且 p'(x)=c1+2c2x+3c3x²；即列表 [c0,c1,c2,c3] 的導數列表為 [c1,2c2,3c3]。





## 逐步主鏈

S01 · definition操作前

[a_0,a_1,a_2,a_3]

操作後

a_0+a_1x+a_2x^2+a_3x^3

條件：無

規則：mko_deriv_rules · 依賴：G1

葉節點依據：mko_deriv_rules + def_unfold

依 MKO，列表由常數項起算、升冪排列：第 k 個位置（由 0 起算）是 x^k 的係數。末端補零是同一個多項式。



S02 · equivalent操作前

f=[2,0,1],\ g=[1,3]

操作後

f(x)=2+x^2,\ g(x)=1+3x

條件：無

規則：def_unfold · 依賴：G2, S01

葉節點依據：def_unfold

依升冪讀法，[2,0,1] 是 2+0x+1x²=2+x²，[1,3] 是 1+3x。若誤以降冪讀，[2,0,1] 會變成 2x²+1，[1,3] 會變成 x+3，是不同的多項式。



S03 · implies操作前

p(x)=c_0+c_1x+c_2x^2+c_3x^3

操作後

p'(x)=c_1+2c_2x+3c_3x^2\ (\forall x\in\mathbb{R})

條件：無

規則：L_poly_deriv3 · 依賴：mko_derivative_def

葉節點依據：mko_derivative_def + distributive + abs_rules + order_basics

依引理 L_poly_deriv3，三次以下多項式處處可微，導數列表為 [c1,2c2,3c3]。這是「展開後求導」路徑的依據，由導數定義直接證明（S03.1 至 S03.4），不引用乘積或鏈式規則，所以可獨立核對那些規則。



S04 · implies操作前

f=[2,0,1],\ g=[1,3]

操作後

f'(x)=2x\ ([0,2]),\quad g'(x)=3\ ([3])

條件：無

規則：L_poly_deriv3 · 依賴：S02, S03

葉節點依據：L_poly_deriv3 + numeric_evaluation

依引理：f 的 c1=0、c2=1，f'=[0,2·1]=[0,2]，即 2x；g 的 c1=3，g'=[3]。兩者處處可微，滿足乘積與鏈式規則的可微前提。



S05 · equivalent操作前

f(x)g(x)=(2+x^2)(1+3x)

操作後

2+6x+x^2+3x^3\ \to\ [2,6,1,3]

條件：無

規則：distributive · 依賴：S02, distributive

葉節點依據：distributive + power_laws + mul_comm

展開：2·1+2·3x+x²·1+x²·3x=2+6x+x²+3x³（N3）。乘積升到三次，新的 x³ 項不能截掉。



S06 · implies操作前

[2,6,1,3]

操作後

(fg)'(x)=6+2x+9x^2\ \to\ [6,2,9]

條件：無

規則：L_poly_deriv3 · 依賴：S05, S03

葉節點依據：L_poly_deriv3 + numeric_evaluation

路徑一（展開後求導）：依引理，[c1,2c2,3c3]=[6,2·1,3·3]=[6,2,9]。



S07 · theorem_application操作前

f'(x)g(x)+f(x)g'(x)

操作後

2x(1+3x)+(2+x^2)\cdot 3=6+2x+9x^2=(fg)'(x)

條件：f,g\ \text{differentiable at}\ x

規則：mko_deriv_rules · 依賴：S02, S04, S06, mko_deriv_rules

葉節點依據：mko_deriv_rules + distributive + eq_refl_symm_trans

路徑二（乘積規則）：f'g+fg'=2x+6x²+6+3x²=6+2x+9x²（N4）。與 S06 是同一個多項式，所以兩條路徑對每個實數 x 都一致；這是多項式恆等式，不是有限點抽樣。



S08 · implies操作前

f'(x)g'(x)

操作後

2x\cdot 3=6x;\ x=0:\ 0\neq 6=(fg)'(0)

條件：無

規則：quantifier_negation · 依賴：S04, S06

葉節點依據：quantifier_negation + numeric_evaluation

常見錯誤是把乘積的導數寫成 f'g'=6x。在 x=0 它是 0，而 (fg)'(0)=6（N7），一個點不同就說明 (fg)'≠f'g'。



S09 · equivalent操作前

(f\circ g)(x)=f(1+3x)

操作後

2+(1+3x)^2=3+6x+9x^2\ \to\ [3,6,9]

條件：無

規則：composition_def · 依賴：S02, composition_def

葉節點依據：composition_def + distributive + power_laws

依合成定義 (f∘g)(x)=f(g(x))，把 f 的變數換成 1+3x：2+(1+3x)²=2+1+6x+9x²=3+6x+9x²（N5）。



S10 · implies操作前

[3,6,9]

操作後

(f\circ g)'(x)=6+18x\ \to\ [6,18]

條件：無

規則：L_poly_deriv3 · 依賴：S09, S03

葉節點依據：L_poly_deriv3 + numeric_evaluation

路徑一：依引理，[c1,2c2]=[6,2·9]=[6,18]。



S11 · theorem_application操作前

f'(g(x))\,g'(x)

操作後

2(1+3x)\cdot 3=6+18x=(f\circ g)'(x)

條件：g\ \text{differentiable at}\ x; f\ \text{differentiable at}\ g(x)

規則：mko_deriv_rules · 依賴：S02, S04, S10, mko_deriv_rules

葉節點依據：mko_deriv_rules + distributive + eq_refl_symm_trans

路徑二（鏈式規則）：外導數 f'(u)=2u 在 u=g(x)=1+3x 取值，得 2(1+3x)，再乘內導數 g'(x)=3：6+18x（N6），與 S10 相同，對每個 x 都一致。



S12 · implies操作前

f'(x)g'(x),\ f'(g(x))

操作後

6x,\ 2+6x;\ x=0:\ 0\neq 6,\ 2\neq 6

條件：無

規則：quantifier_negation · 依賴：S04, S10

葉節點依據：quantifier_negation + numeric_evaluation

兩種錯誤：外導數在 x 而非 g(x) 取值，得 f'(x)g'(x)=6x；漏乘內導數，得 f'(g(x))=2+6x。在 x=0，正確值是 6，兩個錯誤分別給 0 與 2（N8、N9）。



S13 · implies操作前

f+g=[3,3,1],\ -4f=[-8,0,-4]

操作後

(f+g)'=[3,2]=[0,2]+[3],\ (-4f)'=[0,-8]=-4\cdot[0,2]

條件：無

規則：L_poly_deriv3 · 依賴：S02, S03, S04, G3, mko_deriv_rules

葉節點依據：L_poly_deriv3 + mko_deriv_rules + numeric_evaluation

f+g=(2+1)+3x+x²=[3,3,1]（N12），依引理導數 [3,2]，即 3+2x，等於 f'+g'=2x+3。−4f=[−8,0,−4]，導數 [0,−8]，即 −8x，等於 −4·f'=−4·2x。和規則與純量規則在此成立；純量 0 會給零多項式 [0]，也要保留，不可刪除。



S14 · equivalent操作前

(fg)'(1),\ (f\circ g)'(1)

操作後

6+2+9=17,\ 6+18=24

條件：無

規則：numeric_evaluation · 依賴：S06, S10, G3

葉節點依據：numeric_evaluation

在 x=1 求值：(fg)'(1)=6+2·1+9·1²=17，(f∘g)'(1)=6+18·1=24（N10、N11）。







## 局部子步與引理

S03.1 · equivalent操作前

(x+h)^2-x^2,\ (x+h)^3-x^3

操作後

h(2x+h),\ h(3x^2+3xh+h^2)

條件：無

規則：distributive · 依賴：distributive, power_laws

葉節點依據：distributive + power_laws + add_inverse

展開 (x+h)²=x²+2xh+h²、(x+h)³=x³+3x²h+3xh²+h³，減去 x²、x³ 後提出 h（N1）。



S03.2 · equivalent操作前

\frac{p(x+h)-p(x)}{h}\ (h\neq 0)

操作後

(c_1+2c_2x+3c_3x^2)+h\,R,\quad R=c_2+c_3(3x+h)

條件：h\neq 0

規則：frac_rules · 依賴：S03.1, frac_rules

葉節點依據：frac_rules + distributive + mul_inverse_nonzero

由 S03.1，p(x+h)−p(x)=c1h+c2h(2x+h)+c3h(3x²+3xh+h²)=h[(c1+2c2x+3c3x²)+h(c2+3c3x+c3h)]（N2 以六個變數的多項式恆等式核對）。h≠0 時除以 h。令 D=c1+2c2x+3c3x²，差商為 D+hR。



S03.3 · implies操作前

0<|h|\le 1

操作後

|R|\le M=|c_2|+|c_3|(3|x|+1)

條件：|h|\le 1

規則：abs_rules · 依賴：S03.2, abs_rules

葉節點依據：abs_rules + order_basics

三角不等式與 |uv|=|u||v|：|R|≤|c2|+|c3||3x+h|≤|c2|+|c3|(3|x|+|h|)≤|c2|+|c3|(3|x|+1)，最後一步用 |h|≤1。M 只依 x 與係數，不依 h。



S03.4 · implies操作前

\varepsilon>0,\ \delta=\min\left(1,\tfrac{\varepsilon}{M+1}\right)

操作後

0<|h|<\delta\Rightarrow|h||R|\le|h|M<\delta(M+1)\le\varepsilon;\ p'(x)=D

條件：M+1>0

規則：mko_derivative_def · 依賴：S03.2, S03.3, mko_derivative_def

葉節點依據：mko_derivative_def + forall_intro + order_basics + abs_rules

M+1>0，δ>0。若 0<|h|<δ，則 |h|<1，S03.3 適用：|(D+hR)−D|=|h||R|≤|h|M≤|h|(M+1)<δ(M+1)≤ε。ε 任意，依導數定義 p'(x)=D=c1+2c2x+3c3x²。S03.1 至 S03.4 合起來證得引理 L_poly_deriv3。







## 逐步反向審查


- S14 · inverse_equivalence · numeric_evaluation — 精確求值。
- S13 · premise_audit · S03, S04, mko_deriv_rules — 兩條路徑對照；不證明一般的和、純量規則。
- S12 · premise_audit · S04, S10, quantifier_negation — 每個錯誤公式各以一點的反例否定。
- S11 · premise_audit · S04, S10, mko_deriv_rules — 前提：g 在 x 可微、f 在 g(x) 可微，S04 給出兩者處處可微。
- S10 · premise_audit · S09, S03 — 不用鏈式規則。
- S09 · inverse_equivalence · composition_def, distributive — 定義代入與展開都是等式，雙向成立。
- S08 · premise_audit · S04, S06, quantifier_negation — 一個反例否定「兩函數相等」。
- S07 · premise_audit · S04, S06, mko_deriv_rules — 規則的前提（f、g 在 x 可微）由 S04 提供；一致性只對這組 f、g 驗證，不證明一般的乘積規則。
- S06 · premise_audit · S05, S03 — 不用乘積規則，只用 S03 的引理。
- S05 · inverse_equivalence · distributive — 恆等式，雙向成立。
- S04 · premise_audit · S02, S03 — 直接代入引理。
- S03.4 · premise_audit · S03.2, S03.3, mko_derivative_def, forall_intro — 用 M+1 而非 M，避免 M=0 時除以 0；嚴格不等來自 |h|<δ。
- S03.3 · premise_audit · abs_rules, order_basics — 只給上界；需要 |h|≤1，這在 S03.4 由 δ≤1 保證。
- S03.2 · inverse_equivalence · frac_rules, distributive — h≠0 時乘除 h 互逆。
- S03.1 · inverse_equivalence · distributive, power_laws — 恆等式，雙向成立。
- S03 · premise_audit · L_poly_deriv3, mko_derivative_def — 引理只涵蓋三次以下；本稿所有求導的多項式都在此範圍內。
- S02 · inverse_equivalence · def_unfold — 由多項式讀回升冪列表得原列表，雙向一致。
- S01 · premise_audit · G1, mko_deriv_rules — 此步只固定讀法。





## 錯誤控制與反例

乘積的導數不是導數的乘積MKO 的誤解之一是乘積導數直接乘兩導數。f'g'=6x，而 (fg)'=6+2x+9x²；x=0 時 0≠6（S08）。正確的是 f'g+fg'（S07），它與展開後求導（S06）一致。

鏈式規則：外導數在 g(x) 取值，再乘內導數另兩個誤解：外導數在 x 取值得 6x，漏乘內導數得 2+6x（S12），都與正確的 6+18x 不同。若內函數是常數，例如 g=[5]，則 f∘g 是常數 f(5)=27，導數 0，鏈式規則也給 f'(5)·0=0，這個零結果要保留。

係數列表是升冪把 [2,0,1] 反讀成 2x²+1 會得到導數 4x 而不是 2x，輸入多項式因而改變，後續公式或數值可能錯；某些測點即使偶然相同，也不能使反讀約定正確。末端補零（[2,0,1,0]）是同一個多項式，不是新題；乘積與合成可能升次，新項不能截掉（S05）。


- (fg)'=f'g'=6x → reject — (fg)'=6+2x+9x²；x=0 時 6≠0。
- (f∘g)'(x)=f'(x)g'(x)=6x → reject — 外導數要在 g(x) 取值；正確為 6+18x。
- (f∘g)'(x)=f'(g(x))=2+6x → reject — 漏乘內導數 g'(x)=3。
- [2,0,1] 表示 2x²+0x+1 → reject — 列表是升冪，[2,0,1]=2+x²。
- f 是二次、g 是一次，所以 (fg)' 至多一次，可以略去 x² 項 → reject — fg 是三次，(fg)'=6+2x+9x² 是二次；不能截掉新項。





## 結論與限制

f=[2,0,1]=2+x²、g=[1,3]=1+3x，f'=2x、g'=3。fg=[2,6,1,3]，(fg)'=[6,2,9]=6+2x+9x²，與 f'g+fg' 對每個 x 相同；f'g'=6x 錯誤。f∘g=[3,6,9]，(f∘g)'=[6,18]=6+18x，與 f'(g(x))g'(x)=2(1+3x)·3 相同；f'(x)g'(x)=6x 與 f'(g(x))=2+6x 都錯誤。(f+g)'=[3,2]、(−4f)'=[0,−8]。在 x=1：(fg)'(1)=17，(f∘g)'(1)=24。


- 和、純量、乘積、鏈式規則引自 MKO，本稿只對這組 f、g 以多項式恆等式核對，不證明一般可微函數的規則；引理 L_poly_deriv3 只涵蓋三次以下多項式，三次輸入的乘積（至多六次）不在本稿求導範圍內。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: d018b0ec61f9ad721df0ccc4872b72a742b428f70ec5a6bc3709008d1983cb9f
- original source SHA-256: 28b99c11ef6db059516f55a9a5cd9265cb5ca4d59d4d271549486abdf6c12833
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-derivative-rules-01.json)