偏導數：由差商極限推出二次多項式的偏導公式，並計算一點的梯度

目標與範圍

對係數依 [1,x,y,x²,xy,y²] 排列的二次多項式 f，從差商極限的定義證明 ∂f/∂x=c_1+2c_3x+c_4y、∂f/∂y=c_2+c_4x+2c_5y。再對 c=(1,−2,3,1,2,−1) 算出 (1,2) 的偏導與梯度 (4,1)，並說明單一非零 h 的差商（5 或 41/10）與同時移動兩個座標（極限 5）都不是 x 偏導。

只處理 G1 的二變數二次多項式切片（MKO 假設 a1），偏導以差商極限精確推導。不以偏導存在推出一般函數的連續或全微分（a2）；錯誤控制中的非多項式例子只作對照。不改動 canonical MKO 或其英文 edition。

已知條件與符號

• func_limit_def
• abs_rules
• order_basics
• distributive
• power_laws

• G1 — f(x,y)=c_0+c_1x+c_2y+c_3x²+c_4xy+c_5y²，係數為整數，次序固定為 [1,x,y,x²,xy,y²]，f 在 ℝ² 上處處有定義（MKO 假設 a1、a2）。
• G2 — 實例：c=(1,−2,3,1,2,−1)，即 f(x,y)=1−2x+3y+x²+2xy−y²，點 (1,2)。

• c=(c_0,c_1,c_2,c_3,c_4,c_5) — 依 [1,x,y,x²,xy,y²] 次序的係數
• f(x,y) — 二次多項式
• h — 非零增量
• q_x(h) — x 方向差商 (f(x+h,y)−f(x,y))/h
• f_x,\ f_y — x 偏導與 y 偏導
• \nabla f=(f_x,f_y) — 梯度：偏導的有序收集

規則與來源

• func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。
• 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。
• 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。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• 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）。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_partial_def · cited — 二變數函數 f 在點 (x,y) 的 x 偏導，以 y 固定並令 h≠0 趨近 0 的差商極限定義；y 偏導類似。本輪對二次多項式做精確符號微分，不用單一有限差分代替極限。 · mko-partial-derivative
• mko_mvf_def · cited — 二變數實多項式 f:ℝ²→ℝ 的明示切片，係數依 [1,x,y,x²,xy,y²] 固定次序。 · mko-multivariable-real-function
• L_numerator_x · lemma — 對所有實數 x、y、h：f(x+h,y)−f(x,y)=h(c_1+2c_3x+c_4y)+c_3h²。
• L_affine_limit · lemma — 對實常數 A、B，函數 h↦A+Bh 在 h≠0 上有 lim_{h→0}(A+Bh)=A。

逐步主鏈

f_x(x,y)

\lim_{h\to0,\ h\neq0}\frac{f(x+h,y)-f(x,y)}{h}

c=(c_0,c_1,c_2,c_3,c_4,c_5)

f(x,y)=c_0+c_1x+c_2y+c_3x^2+c_4xy+c_5y^2

f(x+h,y)-f(x,y)

h(c_1+2c_3x+c_4y)+c_3h^2

\frac{h(c_1+2c_3x+c_4y)+c_3h^2}{h}

q_x(h)=(c_1+2c_3x+c_4y)+c_3h\quad(h\neq0)

\lim_{h\to0}\big(A+Bh\big)

A

f_x(x,y)=\lim_{h\to0}q_x(h)

f_x(x,y)=c_1+2c_3x+c_4y

\frac{f(x,y+h)-f(x,y)}{h}=(c_2+c_4x+2c_5y)+c_5h

f_y(x,y)=c_2+c_4x+2c_5y

c=(1,-2,3,1,2,-1)

f_x=-2+2x+2y,\quad f_y=3+2x-2y

(x,y)=(1,2)

f_x(1,2)=4,\ \ f_y(1,2)=1,\ \ \nabla f(1,2)=(4,1)

\frac{f(1+h,2)-f(1,2)}{h}

\frac{4h+h^2}{h}=4+h\ \xrightarrow{h\to0}\ 4

q_x(h)=4+h

q_x(1)=5,\ \ q_x(\tfrac1{10})=\tfrac{41}{10},\ \ q_x(h)\neq4\ \text{for every}\ h\neq0

\frac{f(1+h,2+h)-f(1,2)}{h}

\frac{5h+2h^2}{h}=5+2h\ \xrightarrow{h\to0}\ 5\neq4=f_x(1,2)

\text{S06 to S12}

f_x=c_1+2c_3x+c_4y,\ f_y=c_2+c_4x+2c_5y;\ \nabla f(1,2)=(4,1)

局部子步與引理

c_0,\ c_1x,\ c_2y,\ c_3x^2,\ c_4xy,\ c_5y^2\ \text{at}\ (x+h,y)\ \text{minus at}\ (x,y)

0,\ c_1h,\ 0,\ c_3(2xh+h^2),\ c_4hy,\ 0

c_1h+c_3(2xh+h^2)+c_4hy

h(c_1+2c_3x+c_4y)+c_3h^2

\varepsilon>0

\delta=\frac{\varepsilon}{|B|+1}>0

0<|h|<\delta

|(A+Bh)-A|=|B||h|\le|B|\delta=\frac{|B|}{|B|+1}\varepsilon<\varepsilon

逐步反向審查

• S13 · premise_audit · S06, S07, S09 — 只合取已證結論；不宣稱 f 全微分或連續（雖然多項式事實上如此，本稿不證）。
• S12 · premise_audit · L_affine_limit, numeric_evaluation — 只說明這個極限不是 f_x；「方向導數等於 f_x+f_y」只是本例的數值觀察，本稿不證明一般公式。
• S11 · premise_audit · S10, order_basics — 4+h=4 ⇔ h=0，而 h=0 被排除；這個結論只針對本實例。
• S10 · premise_audit · L_affine_limit, numeric_evaluation — 與 S06 的公式互相核對；只對這個實例。
• S09 · inverse_equivalence · numeric_evaluation — 精確整數求值。
• S08 · inverse_equivalence · eq_replace — 等量代換，雙向成立。
• S07 · premise_audit · L_affine_limit, distributive, mul_inverse_nonzero — 與 S03 到 S06 相同的四步，只是 x、y 的角色互換；N2 獨立驗證分子恆等式。
• S06 · premise_audit · S04, S05, S01 — 兩個函數在 h≠0 上相同，極限就相同；h=0 的值不參與。
• S05.2 · premise_audit · abs_rules, order_basics, forall_intro — 用到 |uv|=|u||v|、乘非負數保序、乘正數保持嚴格不等；只宣稱上界。
• S05.1 · premise_audit · abs_rules, order_basics — 正數除以正數為正；δ 只依賴 ε 與 B。
• S05 · premise_audit · L_affine_limit, func_limit_def — 0 是 ℝ∖{0} 的極限點，所以函數極限有意義。
• S04 · inverse_equivalence · mul_inverse_nonzero, frac_rules — 乘 1/h 與乘 h 互逆，前提 h≠0。
• S03.2 · inverse_equivalence · distributive, mul_comm — 提出公因子與展開互逆。
• S03.1 · inverse_equivalence · distributive, power_laws, add_inverse — 每一項都是恆等展開；只有含 x 的項留下，這正是「固定 y」的效果。
• S03 · inverse_equivalence · L_numerator_x, distributive — 這是代數恆等式，對所有 x、y、h 成立，雙向皆可。
• S02 · premise_audit · mko_mvf_def — 係數次序是輸入契約，錯置可能改變多項式與偏導；但不是每個置換都一定改變結果，例如交換相等係數不變。本題 c_1=−2、c_2=3 不相等，交換後確會改變所列偏導。
• S01 · premise_audit · mko_partial_def — 只展開定義；h=0 被排除，因為差商在 h=0 沒有定義。

錯誤控制與反例

不要同時移動兩個座標

MKO 指出的誤解之一是同時改變兩個座標。S12 中 (f(1+h,2+h)−f(1,2))/h→5，而 x 偏導是 4。x 偏導的定義要求 y 固定，只有第一個座標加 h。

一個 h 的差商不是偏導

MKO 的另一個誤解是以一個非零 h 的差商聲稱偏導存在。本例 q_x(h)=4+h，對每個非零 h 都不是 4（h=1 給 5，h=1/10 給 41/10）。即使某種有限差分碰巧給出正確數字（例如中心差分 (q_x(1)+q_x(−1))/2=(5+3)/2=4），那也只是二次多項式的特性，不是存在性的證明：對 u(x,y)=|x| 在 (0,0)，中心差分 (|h|−|−h|)/(2h)=0 對每個 h≠0 成立，但 x 偏導不存在（右差商為 1、左差商為 −1）。

偏導存在不推出連續

MKO 假設 a2 提醒偏導存在不用來推出一般函數連續。例：g(x,y)=xy/(x²+y²)（(x,y)≠(0,0)）、g(0,0)=0。g(x,0)=0 與 g(0,y)=0 對所有 x、y 成立，所以兩個偏導在原點存在且為 0；但沿 y=x，g(t,t)=1/2 對所有 t≠0 成立，不趨近 g(0,0)=0，所以 g 在原點不連續。

• q_x(1)=5，所以 f_x(1,2)=5 → reject — 偏導是 h→0 的極限：q_x(h)=4+h→4（S10、S11）。
• (f(1+h,2+h)−f(1,2))/h→5，所以 x 偏導是 5 → reject — 這同時移動了 y；固定 y=2 的極限是 4（S12）。
• 函數在一點的兩個偏導都存在，所以它在該點連續 → reject — g(x,y)=xy/(x²+y²)、g(0,0)=0 在原點兩偏導皆為 0，但 g(t,t)=1/2（錯誤控制 3）。
• 中心差分 (q(h)+q(−h))/2 對某個 h 給出一個數，就證明了偏導存在且等於它 → reject — u(x,y)=|x| 在 (0,0) 的中心差分恆為 0，但 x 偏導不存在（錯誤控制 2）。

結論與限制

對 f=c_0+c_1x+c_2y+c_3x²+c_4xy+c_5y²，差商在 h≠0 時為仿射式，故 f_x=c_1+2c_3x+c_4y、f_y=c_2+c_4x+2c_5y。對 c=(1,−2,3,1,2,−1)：f_x=−2+2x+2y、f_y=3+2x−2y，在 (1,2) 得梯度 (4,1)。q_x(h)=4+h 對任何非零 h 都不等於 4；同時移動兩座標的極限為 5。

• 錯誤控制 2、3 的非多項式例子以文字論證，沒有拆成編號步驟；本稿主結論不依賴它們。
• 梯度的幾何意義、全微分與高階偏導（MKO 的 formal next）不在範圍內。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: cec61d27ae749c4333888ce08539fdb4a14ce72bd62e3e9d85ee86ac92f9eab1
• original source SHA-256: 277ef1a5d5807fe90f5ab864bef246dbbc0d025aaa5183b9a9d7f44340c942e7
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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