# 偏微分方程：常係數二階算子的主部分類與二次多項式候選的符號殘差

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

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

derivation-mko-partial-differential-equation-01 · production-20261019-adopted-96



## 目標與範圍

在 ℝ² 上給定線性常係數算子 L(u)=u_xx+2u_xy−3u_yy+u_x 與右端 g(x,y)=2x+y−2。先依明示的主部約定 a u_xx+b u_xy+c u_yy 與判別式 b²−4ac 對 L 分類；再對三個二次多項式候選 u_A=x²+xy+y²、u_B=x²+2xy、u_C=x²+xy+y²+y 精確計算符號殘差 R=L(u)−g，判定哪些候選在全 ℝ² 上滿足 L(u)=g，並說明 u_B 的點殘差在整條直線 y=−8 上為零，為何仍不構成解。

停在 MKO 的切片內：二變數二次多項式候選、線性常係數算子、多項式的符號偏導數、點殘差、主部分類與多項式恆等式。主部約定固定為 a u_xx+b u_xy+c u_yy（混合項係數記為 b，而非 2b）。不討論一般解、邊界或初始條件、存在唯一性、弱解或適定性；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- numeric_evaluation
- distributive
- eq_replace
- poly_partial
- quantifier_negation


- G1 — 算子與方程：對 ℝ² 上的二次可微函數 u，L(u)=u_xx+2u_xy−3u_yy+u_x，其中 u_xy 表示先對 x、再對 y 求偏導；右端 g(x,y)=2x+y−2；所問的方程是在全 ℝ² 上 L(u)=g。
- G2 — 主部約定（MKO 要求明示）：二階主部寫成 a u_xx+b u_xy+c u_yy，b 是 u_xy 的完整係數；判別式 D=b²−4ac。
- G3 — 三個二次多項式候選：u_A=x²+xy+y²、u_B=x²+2xy、u_C=x²+xy+y²+y。


- u_x,\ u_y — u 對 x、對 y 的一階偏導數
- u_{xx},\ u_{xy},\ u_{yy} — 二階偏導數；u_{xy} 表示先對 x 再對 y 微分
- L — 本稿的線性常係數算子
- a,\ b,\ c — 主部 a u_{xx}+b u_{xy}+c u_{yy} 的係數
- D=b^2-4ac — 本約定下的判別式
- A,\ B,\ C — 另一約定 A u_{xx}+2B u_{xy}+C u_{yy} 的係數
- R_u=L(u)-g — 候選 u 的符號殘差多項式





## 規則與來源


- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- 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。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_pde · cited — 本輪固定二變數二次多項式候選 u 與線性常係數算子，精確計算一階或二階殘差。二階主部採 a u_xx+b u_xy+c u_yy，判別式為 b²−4ac；這個約定必須明示。點殘差為零只證該點；只有符號殘差多項式全零，才證指定多項式在全域滿足該算子方程。 · mko-partial-differential-equation
- poly_partial · prerequisite — 多項式的偏導數：二變數多項式有各階偏導數；∂/∂x 逐項且線性地作用，把 y 視為常數，∂/∂x(x^m y^k)=m x^(m−1) y^k（m≥1），m=0 時為 0；∂/∂y 對稱地作用。多項式的混合偏導與求導次序無關：u_xy=u_yx。
- pde_class · prerequisite — 常係數二階線性算子的分類（標準定義）：若主部 a u_xx+b u_xy+c u_yy 的係數不全為 0，則 b²−4ac>0 稱雙曲型，b²−4ac=0 稱拋物型，b²−4ac<0 稱橢圓型。分類只看主部，與低階項及右端無關。
- poly_coeff_zero · prerequisite — 係數全為 0 的多項式在 ℝ² 的每一點取值都是 0；因此兩個係數逐一相同的多項式在每一點取值相同。
- L_conv · lemma — 若同一個主部也寫成 A u_xx+2B u_xy+C u_yy（即 a=A、b=2B、c=C），則 b²−4ac=4(B²−AC)；因 4>0，兩個判別式同號。





## 逐步主鏈

S01 · definition操作前

L(u)=u_{xx}+2u_{xy}-3u_{yy}+u_x

操作後

a=1,\ b=2,\ c=-3;\ \text{lower-order part } u_x;\ g=2x+y-2

條件：無

規則：mko_pde · 依賴：G1, G2

葉節點依據：mko_pde + def_unfold

依 G2 的約定，主部是 L 的二階部分 a u_xx+b u_xy+c u_yy。逐項對照：u_xx 的係數 a=1，u_xy 的完整係數 b=2（不除以 2），u_yy 的係數 c=−3。u_x 是一階（低階）項，不進入分類；g 是右端。先把約定寫明，是 MKO 的明確要求，因為同一個算子在另一種寫法下混合項係數會被讀成 1。



S02 · equivalent操作前

D=b^2-4ac

操作後

D=2^2-4\cdot 1\cdot(-3)=16

條件：無

規則：numeric_evaluation · 依賴：S01

葉節點依據：numeric_evaluation + neg_mul

代入 a=1、b=2、c=−3：b²=4；4ac=4·1·(−3)=−12（負數乘正數為負）；所以 D=4−(−12)=4+12=16。減去一個負數等於加上它的相反數。



S03 · implies操作前

D=16

操作後

L\ \text{is hyperbolic}

條件：(a,b,c)\neq(0,0,0); D>0

規則：pde_class · 依賴：S01, S02, pde_class

葉節點依據：pde_class + order_basics

分類定義要求主部係數不全為 0：a=1≠0，成立。D=16>0，所以依定義 L 是雙曲型。低階項 u_x 與右端 g 不影響分類。



S04 · implies操作前

A u_{xx}+2B u_{xy}+C u_{yy}=u_{xx}+2u_{xy}-3u_{yy}

操作後

A=1,\ B=1,\ C=-3,\ B^2-AC=4=\tfrac{16}{4}

條件：b=2B

規則：L_conv · 依賴：S01, S02, L_conv

葉節點依據：L_conv + numeric_evaluation

在另一種約定下，混合項係數寫成 2B，所以 2B=2，B=1；A=1、C=−3。此時 B²−AC=1−(1)(−3)=4。依引理 L_conv，b²−4ac=4(B²−AC)，即 16=4·4，兩約定給出同號、同類型。前提是每個公式配它自己的係數；若把 b=2 放進 B²−AC 得 4+3=7，或把 B=1 放進 b²−4ac 得 1+12=13，兩者都不是任何一種約定下的判別式。



S05 · implies操作前

u_A=x^2+xy+y^2

操作後

(u_A)_x=2x+y,\ (u_A)_y=x+2y

條件：無

規則：poly_partial · 依賴：G3, poly_partial

葉節點依據：poly_partial

逐項求偏導。對 x：∂x(x²)=2x，∂x(xy)=y（y 視為常數），∂x(y²)=0，所以 (u_A)_x=2x+y。對 y：∂y(x²)=0，∂y(xy)=x，∂y(y²)=2y，所以 (u_A)_y=x+2y。



S06 · implies操作前

(u_A)_x=2x+y,\ (u_A)_y=x+2y

操作後

(u_A)_{xx}=2,\ (u_A)_{xy}=1,\ (u_A)_{yy}=2

條件：無

規則：poly_partial · 依賴：S05, poly_partial

葉節點依據：poly_partial

再求一次：(u_A)_xx=∂x(2x+y)=2；(u_A)_xy=∂y(2x+y)=1（依 G1，先對 x 再對 y）；(u_A)_yy=∂y(x+2y)=2。交叉核對：(u_A)_yx=∂x(x+2y)=1，與 (u_A)_xy 相同，符合多項式混合偏導與次序無關。



S07 · equivalent操作前

L(u_A)=(u_A)_{xx}+2(u_A)_{xy}-3(u_A)_{yy}+(u_A)_x

操作後

L(u_A)=2x+y-2

條件：無

規則：eq_replace · 依賴：G1, S05, S06

葉節點依據：eq_replace + distributive + numeric_evaluation

把 S06 與 S05 的結果代入 G1 的算子：L(u_A)=2+2·1−3·2+(2x+y)。常數部分 2+2−6=−2（S07.1），所以 L(u_A)=2x+y−2。這是符號計算，結果對每一點 (x,y) 都成立，不是在個別點取樣。



S08 · equivalent操作前

R_{u_A}=L(u_A)-g

操作後

R_{u_A}=(2-2)x+(1-1)y+(-2+2)=0

條件：無

規則：distributive · 依賴：S07, G1

葉節點依據：distributive + add_inverse + add_comm

R_{u_A}=(2x+y−2)−(2x+y−2)。依分配律合併同類項：x 的係數 2−2=0，y 的係數 1−1=0，常數 −2−(−2)=0。三個係數全為 0，所以符號殘差是零多項式；這是 MKO a2 所說能證全域的那種證據。



S09 · implies操作前

R_{u_A}\equiv 0

操作後

\forall (x,y)\in\mathbb{R}^2:\ L(u_A)(x,y)=g(x,y)

條件：無

規則：poly_coeff_zero · 依賴：S08, poly_coeff_zero, forall_intro

葉節點依據：poly_coeff_zero + forall_intro

係數全為 0 的多項式在每一點取值 0。取任意 (x,y)∈ℝ²：R_{u_A}(x,y)=0，即 L(u_A)(x,y)−g(x,y)=0，L(u_A)(x,y)=g(x,y)。推導對 (x,y) 沒有任何額外假設，依 ∀ 引入，u_A 在全 ℝ² 上滿足 L(u)=g。



S10 · implies操作前

u_B=x^2+2xy

操作後

(u_B)_x=2x+2y,\ (u_B)_y=2x,\ (u_B)_{xx}=2,\ (u_B)_{xy}=2,\ (u_B)_{yy}=0

條件：無

規則：poly_partial · 依賴：G3, poly_partial

葉節點依據：poly_partial

一階：∂x(x²)=2x、∂x(2xy)=2y，所以 (u_B)_x=2x+2y；∂y(x²)=0、∂y(2xy)=2x，所以 (u_B)_y=2x。二階：(u_B)_xx=∂x(2x+2y)=2，(u_B)_xy=∂y(2x+2y)=2，(u_B)_yy=∂y(2x)=0。交叉核對 (u_B)_yx=∂x(2x)=2。



S11 · equivalent操作前

R_{u_B}=L(u_B)-g

操作後

R_{u_B}=(2+4-0+2x+2y)-(2x+y-2)=y+8

條件：無

規則：eq_replace · 依賴：G1, S10

葉節點依據：eq_replace + distributive + numeric_evaluation

代入：L(u_B)=2+2·2−3·0+(2x+2y)=2x+2y+6。減去 g：x 的係數 2−2=0，y 的係數 2−1=1，常數 6−(−2)=8。所以 R_{u_B}=y+8。y 的係數是 1≠0，這不是零多項式。



S12 · implies操作前

R_{u_B}(x,-8)

操作後

R_{u_B}(x,-8)=-8+8=0\ \text{for every } x\in\mathbb{R}

條件：無

規則：eq_replace · 依賴：S11

葉節點依據：eq_replace + numeric_evaluation

以 y=−8 代入 R_{u_B}=y+8，得 0，與 x 無關。所以 u_B 的點殘差在整條直線 y=−8 的無限多個點上都為零，例如 (0,−8)、(5,−8)。這正是容易被誤讀成「u_B 是解」的情形。



S13 · implies操作前

R_{u_B}(0,0)

操作後

R_{u_B}(0,0)=8\neq 0,\ \text{so}\ \neg\,\forall (x,y):\ L(u_B)(x,y)=g(x,y)

條件：無

規則：quantifier_negation · 依賴：S11, quantifier_negation

葉節點依據：quantifier_negation + exists_intro + numeric_evaluation

在 (0,0)：R_{u_B}(0,0)=0+8=8≠0；也就是 L(u_B)(0,0)=6，而 g(0,0)=−2。全稱命題「對所有 (x,y)，L(u_B)=g」的否定等價於「存在一點使其不成立」，(0,0) 就是這樣的點。所以 u_B 不是 L(u)=g 在 ℝ² 上的解，儘管 S12 的點殘差在整條直線上為零。



S14 · implies操作前

u_C=x^2+xy+y^2+y

操作後

R_{u_C}\equiv 0,\quad u_C-u_A=y\not\equiv 0

條件：無

規則：poly_partial · 依賴：G1, G3, poly_partial, S09

葉節點依據：poly_partial + eq_replace + poly_coeff_zero

(u_C)_x=2x+y，(u_C)_y=x+2y+1；二階偏導 (u_C)_xx=2、(u_C)_xy=1、(u_C)_yy=2，與 u_A 相同。所以 L(u_C)=2+2−6+(2x+y)=2x+y−2，R_{u_C} 是零多項式，u_C 也在全 ℝ² 上滿足 L(u)=g（理由同 S09）。但 u_C−u_A=y 不是零多項式，所以 u_C≠u_A。方程 L(u)=g 本身（不加任何邊界或初始條件）至少有兩個相異的多項式解：一個候選通過，並不給出一般解或唯一性。



S15 · implies操作前

\text{results of S03, S09, S13, S14}

操作後

L\ \text{hyperbolic};\ u_A,u_C\ \text{solve } L(u)=g\ \text{on}\ \mathbb{R}^2;\ u_B\ \text{does not}

條件：無

規則：and_intro_elim · 依賴：S03, S09, S13, S14

葉節點依據：and_intro_elim

把各部分結論合在一起：分類（S03）、u_A 與 u_C 的全域符號證書（S09、S14）、u_B 的單點否證（S13）。每一項結論各有自己的證據，彼此不互相替代：分類不說解，點殘差不說全域，候選通過不說唯一。







## 局部子步與引理

S04.1 · equivalent操作前

(2B)^2-4AC

操作後

4(B^2-AC)

條件：無

規則：distributive · 依賴：power_laws, distributive

葉節點依據：power_laws + distributive + mul_comm + order_basics

由指數律 (2B)²=2²B²=4B²；再由分配律 4B²−4AC=4(B²−AC)。以 a=A、b=2B、c=C 代入，得 b²−4ac=4(B²−AC)。因 4>0，乘以 4 不改變正、零、負，所以兩個判別式同號。這證明了引理 L_conv（N3 是同一恆等式在網格上的多項式核對）。



S07.1 · equivalent操作前

2+2\cdot 1-3\cdot 2

操作後

-2

條件：無

規則：numeric_evaluation · 依賴：numeric_evaluation

葉節點依據：numeric_evaluation

2+2=4，3·2=6，4−6=−2。







## 逐步反向審查


- S15 · premise_audit · S03, S09, S13, S14, and_intro_elim — 只是合取已證的結論。不宣稱一般解、存在唯一性或適定性，這些不在本切片內（MKO a2、para2）。
- S14 · premise_audit · G3, poly_partial, poly_coeff_zero, S09 — 需要 u_C 的符號殘差為零與 u_C−u_A 不為零多項式。只宣稱沒有附加條件時解不唯一；不宣稱加上邊界或初始條件後的任何情況。
- S13 · premise_audit · S11, quantifier_negation — 否證只需一個精確的點；需要的是 S11 的殘差公式與量詞否定。這不說 u_B 在任何點都不滿足方程（S12 顯示它在 y=−8 上滿足）。
- S12 · premise_audit · S11, eq_replace — 只是在直線 y=−8 上求值。結論只關於這些點，不推出 R_{u_B} 是零多項式；S13 顯示它不是。
- S11 · inverse_equivalence · S10, eq_replace, distributive — 代換與合併同類項都是等值改寫，可逆向還原；兩式是同一個多項式。
- S10 · premise_audit · G3, poly_partial — 與 S05、S06 相同，只用多項式求導規則；不宣稱反向。
- S09 · premise_audit · S08, poly_coeff_zero, forall_intro — 需要殘差是零多項式（S08），而不是在某些點為零。只宣稱 u_A 是這個方程在 ℝ² 上的一個解；不宣稱它是唯一解或一般解。
- S08 · inverse_equivalence · S07, distributive, add_inverse — 合併同類項是多項式的等值改寫，可以逆向拆開；兩式是同一個多項式。
- S07.1 · inverse_equivalence · numeric_evaluation — 反向：−2+6=4=2+2·1，兩邊是同一個整數。
- S07 · inverse_equivalence · S05, S06, eq_replace — 等值代換可雙向進行：把 2x+y−2 拆回 2+2·1−3·2+(2x+y)，每一項又等於對應的偏導數。
- S06 · premise_audit · S05, poly_partial — 需要 S05 的一階偏導與求導規則；二階偏導都是常數，因為 u_A 是二次多項式。不宣稱反向。
- S05 · premise_audit · G3, poly_partial — 只用多項式的逐項求導規則。不反向宣稱：由偏導數回推原函數只能定到另一變數的函數，所以此步不是等價。
- S04.1 · inverse_equivalence · power_laws, distributive — 反向展開 4(B²−AC)=4B²−4AC=(2B)²−4AC；兩式是同一個多項式，對所有 A、B、C 成立，沒有附加條件。
- S04 · premise_audit · S01, S02, L_conv — 結論依賴 b=2B 這個一致的讀法。只宣稱兩個正確公式同號，不宣稱任何恰好同號的混用公式都可接受；錯誤控制給出混用導致符號改變的例子。
- S03 · premise_audit · S01, S02, pde_class — 需要主部非零與 D 的符號。分類只是主部的性質；本步不宣稱 L(u)=g 在任何邊界或初始條件下有解或解唯一。
- S02 · inverse_equivalence · S01, numeric_evaluation, neg_mul — 反向重算：16−4=12=−4ac，與 4ac=−12 一致；兩邊是同一個數，等式雙向成立。
- S01 · premise_audit · G1, G2, mko_pde — 此步只依約定讀出係數，不推出新事實。讀法依賴 G2：若改用 A u_xx+2B u_xy+C u_yy，混合項係數是 B=1，判別式公式也要跟著換（見 S04）。





## 錯誤控制與反例

點殘差為零不等於解MKO 指出的常見誤解是由取樣點殘差為零宣稱全域解。u_B 的殘差在整條直線 y=−8 上為零，甚至是無限多個點，但殘差多項式 y+8 不是零多項式，(0,0) 處等於 8。只有符號殘差的每個係數都為 0（S08），才證明在全 ℝ² 上成立。

混用 b 與 2B 的判別式MKO 的另一個誤解是混用 2b u_xy 與 b u_xy 的判別式。例：算子 u_xx+2u_xy+2u_yy。依 G2，a=1、b=2、c=2，D=4−8=−4<0，橢圓型；依 A u_xx+2B u_xy+C u_yy，B=1，B²−AC=1−2=−1<0，同樣橢圓型。若把混合項係數 2 直接當成 B 代入 B²−AC，得 4−2=2>0，會錯判為雙曲型。所以必須先寫明約定，再用該約定自己的公式。

分類與候選通過都不給唯一性S03 的雙曲型只描述主部；S09 只說 u_A 是一個解。S14 找到第二個解 u_C=u_A+y，說明沒有邊界或初始條件時解不唯一。存在唯一性與適定性需要另外的定理與條件，本稿不處理。


- u_B 在 (0,−8) 與 (5,−8) 的殘差都是 0，所以 u_B 在 ℝ² 上滿足 L(u)=g → reject — R_{u_B}=y+8 不是零多項式；R_{u_B}(0,0)=8≠0。
- u_xx+2u_xy+2u_yy 的混合項係數是 2，代入 B²−AC 得 2>0，所以它是雙曲型 → reject — 在 2B 約定下 B=1，B²−AC=−1；在 b 約定下 D=4−8=−4；兩者都是橢圓型。
- u_A 滿足 L(u)=g，所以 u_A 是此方程的唯一解 → reject — u_C=u_A+y 也滿足，且 u_C≠u_A。
- L 是雙曲型，所以 L(u)=g 對任何邊界資料都有唯一解 → reject — 分類只看主部；本稿沒有證明任何存在唯一或適定性結果，MKO a2 也排除這類宣稱。





## 結論與限制

在約定 a u_xx+b u_xy+c u_yy、D=b²−4ac 下，L 的係數為 a=1、b=2、c=−3，D=16>0，L 是雙曲型（改用 A u_xx+2B u_xy+C u_yy 時 B=1、B²−AC=4，同號）。u_A=x²+xy+y² 與 u_C=x²+xy+y²+y 的符號殘差都是零多項式，所以都在全 ℝ² 上滿足 L(u)=g；u_B=x²+2xy 的殘差是 y+8，雖然在整條直線 y=−8 上為零，但在 (0,0) 等於 8，所以 u_B 不是解。


- poly_partial、pde_class 與 poly_coeff_zero 是本稿的前提（標準定義與多項式事實），不在本稿中從更基本的定義推出。
- 本稿不處理一般解、邊界或初始條件、存在唯一性與適定性（MKO 的 formal next）。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: d7f1dca1ded3622b8bc0d17369236ab7e35c0df919f547af5b7b66b3c462a9b0
- original source SHA-256: d7f1dca1ded3622b8bc0d17369236ab7e35c0df919f547af5b7b66b3c462a9b0
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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