# 常微分方程：判定階數並核對候選解 y=x² 與 y=x²+x

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

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

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



## 目標與範圍

在區間 I=ℝ 上考慮常微分方程 y″−2y′+y=x²−4x+2。(1) 判定它的階數；(2) 核對 y₁(x)=x² 在整個 ℝ 上是解（殘差恆為零）；(3) 證明 y₂(x)=x²+x 的殘差是 x−2，只在 x=2 為零，所以它不是 ℝ 上的解；(4) 核對初值 y(0)=0、y′(0)=0，並引用二階線性方程的存在唯一定理（含其假設）判定 y₁ 是此初值問題的唯一解；(5) 說明沒有初值時解不唯一。

主要核對限於整係數多項式候選與精確殘差（MKO 假設 a2）；殘差以符號方式化簡，所以結論對區間上每一點成立，而不是只在抽樣點。唯一性不由方程本身推出，而是引用明示假設的定理（citation_verified），本稿不證明該定理。y₃=x²+eˣ 只用來說明「沒有初值時解不唯一」。不處理一般存在性理論或非線性方程的分類；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- func_limit_def
- distributive
- eq_replace
- forall_intro
- quantifier_negation


- G1 — 區間 I=ℝ；未知量 y 是 ℝ 上二次可微的實值函數；方程 E：對每個 x∈I，y″(x)−2y′(x)+y(x)=x²−4x+2。
- G2 — 候選函數：y₁(x)=x²，y₂(x)=x²+x（整係數多項式）；另有 y₃(x)=x²+eˣ，只在 S13、S14 用來說明非唯一性。
- G3 — 初值條件：y(0)=0，y′(0)=0。
- G4 — 殘差：對候選 u，r_u(x)=u″(x)−2u′(x)+u(x)−(x²−4x+2)。u 在 I 上是 E 的解，當且僅當對每個 x∈I 有 r_u(x)=0。


- I=\mathbb{R} — 方程成立的區間
- y',\ y'' — 未知函數的一階與二階導數
- r_u(x) — 候選 u 在 x 的殘差：左邊減右邊
- y_1,\ y_2,\ y_3 — 三個候選函數
- p,\ q,\ g — 標準形 y''+py'+qy=g 的係數與右邊





## 規則與來源


- func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- 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 不定義。
- 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。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_ode_def · cited — 常微分方程是在指定區間上，關聯未知單變數函數 y 與其有限階導數的方程。方程中出現的最高導數階數稱為階數；把候選 y 代入並得零殘差，只核對該候選在指定範圍是否滿足方程。 · mko-ordinary-differential-equation
- mko_ode_check · cited — 候選解核對應重算 y、y′、y″ 等並代入同一方程；只在一點殘差為零通常不足以證整個區間上為解。初值可以篩選候選解，但存在與唯一性仍需連續性、Lipschitz 等額外假設及對應定理。 · mko-ordinary-differential-equation
- deriv_rules · prerequisite — ℝ 上的求導規則：常數的導數為 0；(x)′=1；(u+v)′=u′+v′；(cu)′=cu′（c 為常數）；(eˣ)′=eˣ。
- poly_exp_continuous · prerequisite — 常數函數與多項式函數在 ℝ 上處處連續。
- thm_linear_ivp · cited — 設 p、q、g 在含 x₀ 的開區間 I 上連續。則對任意實數 Y₀、Y₁，初值問題 y″+p(x)y′+q(x)y=g(x)、y(x₀)=Y₀、y′(x₀)=Y₁ 恰有一個解，且該解在整個 I 上存在。 · William F. Trench, Elementary Differential Equations with Boundary Value Problems, Section 5.3, Theorem 5.3.1
- L_deriv_square · lemma — 對每個實數 x，函數 x↦x² 在 x 可微且 (x²)′=2x。





## 逐步主鏈

S01 · definition操作前

y''-2y'+y=x^2-4x+2\ \text{on }I=\mathbb{R}

操作後

F(x,y,y',y'')=y''-2y'+y-(x^2-4x+2)=0

條件：無

規則：mko_ode_def · 依賴：G1, G4

葉節點依據：mko_ode_def + def_intro

依 MKO，常微分方程是在指定區間上關聯未知單變數函數及其導數的方程。把右邊移到左邊，寫成 F(x,y,y′,y″)=0 的形式，區間明示為 I=ℝ。殘差 r_u 正是把候選 u 代入 F 所得的值（G4）。



S02 · implies操作前

F(x,y,y',y'')=0

操作後

\text{order}=2

條件：\text{coefficient of }y''\text{ is }1\neq 0

規則：mko_ode_def · 依賴：S01, mko_ode_def

葉節點依據：mko_ode_def + def_unfold

依 MKO，階數是方程中實際出現的最高導數階數。出現的導數是 y′ 與 y″，y″ 的係數是 1≠0，沒有三階或更高的導數，所以階數是 2。階數不是由左邊有三項決定，也不是由候選 x² 的次數決定。



S03 · implies操作前

y_1(x)=x^2

操作後

y_1'(x)=2x

條件：無

規則：L_deriv_square · 依賴：G2, L_deriv_square

葉節點依據：func_limit_def + distributive

依引理 L_deriv_square（在 S03.1、S03.2 由導數的極限定義證明），y₁′(x)=2x 對每個實數 x 成立。



S04 · implies操作前

y_1'(x)=2x

操作後

y_1''(x)=2

條件：無

規則：deriv_rules · 依賴：S03, deriv_rules

葉節點依據：deriv_rules + mul_one

再求一次導數：(2x)′=2·(x)′=2·1=2（常數倍規則與 (x)′=1）。



S05 · equivalent操作前

y_1''(x)-2y_1'(x)+y_1(x)

操作後

2-2(2x)+x^2

條件：無

規則：eq_replace · 依賴：S03, S04, G2, G4

葉節點依據：eq_replace + mko_ode_check

依 MKO 的核對方法，把重算出的 y₁、y₁′、y₁″ 代入同一個方程的左邊：y₁″=2，y₁′=2x，y₁=x²。



S06 · equivalent操作前

2-2(2x)+x^2

操作後

x^2-4x+2

條件：無

規則：distributive · 依賴：S05

葉節點依據：mul_assoc + add_comm + add_assoc

2(2x)=4x，重新排列各項得 x²−4x+2。這是多項式恆等式（N2），對每個實數 x 成立。



S07 · implies操作前

r_{y_1}(x)=(x^2-4x+2)-(x^2-4x+2)

操作後

\forall x\in\mathbb{R}:\ r_{y_1}(x)=0

條件：無

規則：forall_intro · 依賴：S06, G4

葉節點依據：forall_intro + add_inverse

依 G4，殘差是左邊減右邊；由 S06 左邊等於 x²−4x+2，所以 r_{y₁}(x)=0。這個計算對 x 沒有任何額外假設，x 是任意實數，依全稱推廣 r_{y₁} 在整個 ℝ 上恆為零，所以 y₁ 是 E 在 I=ℝ 上的解。這是符號化簡得到的，不是抽樣點核對。



S08 · implies操作前

y_2(x)=x^2+x

操作後

y_2'(x)=2x+1,\ \ y_2''(x)=2

條件：無

規則：deriv_rules · 依賴：G2, L_deriv_square, deriv_rules

葉節點依據：deriv_rules + L_deriv_square

依和的求導規則、L_deriv_square 與 (x)′=1，y₂′=2x+1；再求一次導數，y₂″=2+0=2。



S09 · equivalent操作前

r_{y_2}(x)=2-2(2x+1)+(x^2+x)-(x^2-4x+2)

操作後

r_{y_2}(x)=x-2

條件：無

規則：distributive · 依賴：S08, G4

葉節點依據：distributive + add_assoc + add_comm + add_inverse

代入並化簡，細節在 S09.1、S09.2：先算左邊得 x²−3x，再減去右邊得 x−2。殘差是一個非零多項式。



S10 · implies操作前

r_{y_2}(x)=x-2

操作後

r_{y_2}(2)=0,\ r_{y_2}(0)=-2\neq 0\ \Rightarrow\ y_2\ \text{not a solution on }\mathbb{R}

條件：無

規則：quantifier_negation · 依賴：S09, G4

葉節點依據：quantifier_negation + numeric_evaluation

在 x=2 殘差為 0，單點核對會誤判 y₂ 為解；但 r_{y₂}(0)=−2≠0。「對所有 x∈ℝ 殘差為零」只要一個反例就被否定，所以 y₂ 不是 ℝ 上的解。更進一步，x−2=0 ⇔ x=2，所以在任何含有 2 以外的點的區間上，y₂ 都不是解。



S11 · implies操作前

y_1(0),\ y_1'(0)

操作後

y_1(0)=0,\ y_1'(0)=0

條件：無

規則：numeric_evaluation · 依賴：G2, G3, S03

葉節點依據：numeric_evaluation + mul_zero

y₁(0)=0²=0，y₁′(0)=2·0=0，所以 y₁ 滿足 G3 的兩個初值條件。初值在這裡起篩選作用。



S12 · theorem_application操作前

y''+p\,y'+q\,y=g,\ p=-2,\ q=1,\ g=x^2-4x+2,\ y(0)=0,\ y'(0)=0

操作後

y_1\ \text{is the unique solution of the IVP on }\mathbb{R}

條件：p,q,g\ \text{continuous on }\mathbb{R}; 0\in\mathbb{R},\ \mathbb{R}\ \text{open}

規則：thm_linear_ivp · 依賴：S07, S11, G1, G3, thm_linear_ivp, poly_exp_continuous

葉節點依據：thm_linear_ivp + poly_exp_continuous

把 E 寫成標準形 y″+p y′+q y=g，p(x)=−2、q(x)=1 是常數函數，g(x)=x²−4x+2 是多項式，三者在開區間 ℝ 上連續，且 x₀=0∈ℝ。引用定理 thm_linear_ivp（Y₀=0、Y₁=0）：初值問題恰有一個解，且在整個 ℝ 上存在。S07 與 S11 說明 y₁ 就是這樣一個解，所以它就是那唯一的解。唯一性來自定理與其連續性假設，而不是來自方程本身。



S13 · implies操作前

y_3(x)=x^2+e^x

操作後

y_3'(x)=2x+e^x,\ \ y_3''(x)=2+e^x

條件：無

規則：deriv_rules · 依賴：G2, deriv_rules, L_deriv_square

葉節點依據：deriv_rules + L_deriv_square

為了說明沒有初值時解不唯一，取 y₃=x²+eˣ。依和的規則、L_deriv_square 與 (eˣ)′=eˣ：y₃′=2x+eˣ，y₃″=2+eˣ。



S14 · implies操作前

r_{y_3}(x)=(2+e^x)-2(2x+e^x)+(x^2+e^x)-(x^2-4x+2)

操作後

r_{y_3}(x)=0\ \forall x,\ \ y_3(0)=1\neq 0

條件：無

規則：distributive · 依賴：S13, G4, G3

葉節點依據：distributive + add_inverse + numeric_evaluation

展開：eˣ 的係數 1−2+1=0，x 的係數 −4+4=0，x² 的係數 1−1=0，常數 2−2=0，所以對每個 x 殘差為 0（N7 把 eˣ 當作獨立符號 E 做恆等式核對，因此對 eˣ 的任何值都成立）。y₃ 也是 E 在 ℝ 上的解，但 y₃(0)=0+1=1≠0，不滿足初值。所以方程本身有不只一個解，初值才把 y₁ 選出來。



S15 · implies操作前

\text{proved facts about }E

操作後

\text{order }2;\ y_1\ \text{solves};\ y_2\ \text{does not};\ y_1\ \text{unique for the IVP};\ E\ \text{alone not unique}

條件：無

規則：and_intro_elim · 依賴：S02, S07, S10, S12, S14

葉節點依據：and_intro_elim

合併結論：E 的階數為 2；y₁=x² 在 ℝ 上是解；y₂=x²+x 不是（殘差 x−2）；在初值 y(0)=0、y′(0)=0 下 y₁ 是唯一解（依引用定理）；沒有初值時 y₃=x²+eˣ 也是解。







## 局部子步與引理

S03.1 · equivalent操作前

(x+h)^2-x^2

操作後

h(2x+h)

條件：無

規則：distributive · 依賴：distributive

葉節點依據：distributive + add_assoc + add_comm + add_inverse

展開 (x+h)²=x²+2xh+h²，減去 x² 得 2xh+h²，再提出 h 得 h(2x+h)。這是對所有實數 x、h 成立的多項式恆等式（N1）。



S03.2 · implies操作前

\frac{(x+h)^2-x^2}{h}=2x+h\ (h\neq 0)

操作後

\lim_{h\to 0}\frac{(x+h)^2-x^2}{h}=2x

條件：h\neq 0

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

葉節點依據：func_limit_def + mul_inverse_nonzero + abs_rules

對 h≠0，可以除以 h，差商等於 2x+h。對任意 ε>0 取 δ=ε：當 0<|h|<δ 時，|(2x+h)−2x|=|h|<ε。依極限定義差商趨於 2x，所以 (x²)′=2x。S03.1 與 S03.2 合起來證得引理 L_deriv_square。



S09.1 · equivalent操作前

2-2(2x+1)+(x^2+x)

操作後

x^2-3x

條件：無

規則：distributive · 依賴：S08

葉節點依據：distributive + add_inverse + add_comm

2(2x+1)=4x+2，所以 2−4x−2+x²+x=x²−3x。



S09.2 · equivalent操作前

(x^2-3x)-(x^2-4x+2)

操作後

x-2

條件：無

規則：distributive · 依賴：S09.1

葉節點依據：neg_mul + distributive + add_inverse

去括號：x²−3x−x²+4x−2，x² 相消，−3x+4x=x，得 x−2。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S02, S07, S10, S12, S14, and_intro_elim — 目標 G：本稿目標的五項判定。足夠條件 H：S02、S07、S10、S12、S14（H⇒G 由合取引入）。H 由給定條件與引用定理正向推出，沒有把 G 當作前提；唯一性依賴的定理標為 citation_verified。
- S14 · premise_audit · S13, G4, distributive, add_inverse — 需要逐項係數相消；這證明了 E 的解不唯一，與 S12 不矛盾，因為 S12 的唯一性是在加上初值之後。
- S13 · premise_audit · deriv_rules, L_deriv_square — 只用到求導規則；y₃ 不是多項式，超出 MKO 題庫的候選類，只作說明用途。
- S12 · premise_audit · thm_linear_ivp, poly_exp_continuous, S07, S11 — 定理需要：方程為線性且 y″ 係數為 1、p、q、g 在含 x₀ 的開區間上連續、給定兩個初值；四項都已核對。定理本身未在本稿證明（citation_verified）。不宣稱非線性方程有同樣結論。
- S11 · premise_audit · S03, numeric_evaluation — 只是在 x=0 求值；滿足初值本身不證明 y₁ 是唯一的解，唯一性由 S12 的定理提供。
- S10 · premise_audit · S09, quantifier_negation, numeric_evaluation — 否定全稱只需一個反例 x=0；r_{y₂}(2)=0 這個事實並不支持 y₂ 是解。
- S09.2 · inverse_equivalence · neg_mul, add_inverse — 負號分配與加法反元素，對所有 x 雙向成立。
- S09.1 · inverse_equivalence · distributive, add_inverse — 分配律與合併同類項，對所有 x 雙向成立。
- S09 · inverse_equivalence · distributive, add_inverse — 每一步都是對所有 x 成立的多項式恆等式（N3），雙向成立。
- S08 · premise_audit · L_deriv_square, deriv_rules — 每個導數都要重新計算，不能沿用 y₁ 的導數；兩者只差在 +x 一項，y₂′ 因而多了 1。
- S07 · premise_audit · S06, G4, forall_intro — 全稱推廣可用，因為 S03 到 S06 對任意 x 成立。結論只關於 y₁ 是一個解，不宣稱它是唯一的解（見 S12 至 S14）。
- S06 · inverse_equivalence · mul_assoc, add_comm — 只用到結合律與交換律，雙向成立。
- S05 · inverse_equivalence · eq_replace, S03, S04 — 等值代換，雙向成立：兩式在每個 x 都表示同一個數。
- S04 · premise_audit · S03, deriv_rules — 只用到求導規則；y₁′ 在整個 ℝ 上可微，所以 y₁″ 處處有定義。
- S03.2 · premise_audit · S03.1, func_limit_def, mul_inverse_nonzero — 除以 h 需要 h≠0；極限定義只看 0<|h|<δ 的 h，所以 h=0 從不需要代入。
- S03.1 · inverse_equivalence · distributive, add_inverse — 展開 h(2x+h) 得 2xh+h²，再加回 x² 即得 (x+h)²；兩式對所有 x、h 相等。
- S03 · premise_audit · L_deriv_square — 依賴該引理；不宣稱反向（導數為 2x 的函數不只 x²，還可差一個常數）。
- S02 · premise_audit · S01, mko_ode_def — 需要確認 y″ 的係數非零；若係數為 0，y″ 並未真正出現，階數會下降。
- S01 · premise_audit · G1, G4, mko_ode_def — 此步只改寫與命名，不推出新事實；移項是等價變形。





## 錯誤控制與反例

一點代入成功不等於區間上的解MKO 指出的誤解之一：y₂=x²+x 在 x=2 代入後殘差為 0，但在 x=0 殘差為 −2。解的定義要求殘差在整個區間上每一點都為零；對多項式候選，最穩妥的做法是像 S07、S09 那樣把殘差化簡成多項式，看它是否為零多項式。

階數看實際出現的最高導數階數不是左邊的項數（3），也不是候選解的次數（x² 的 2 只是巧合）。若某個高階導數的係數為 0，例如 0·y‴+y″=1，則 y‴ 沒有真正出現，該方程是二階。換成候選 x⁵ 也不會改變方程的階數。

存在與唯一需要定理與假設MKO 指出的另一個誤解是由方程與初值直接宣稱必有唯一解。S12 用的定理要求線性、係數在含 x₀ 的開區間上連續。假設不成立時結論可能失敗：非線性方程 y′=3y^(2/3)、y(0)=0 同時有解 y=0 與 y=x³（右邊在 y=0 附近不滿足 Lipschitz 條件）。


- r_{y₂}(2)=0，所以 y₂=x²+x 是此方程在 ℝ 上的解 → reject — r_{y₂}(0)=−2≠0；殘差 x−2 只在 x=2 為零（S10）。
- 左邊有三項，所以這是三階方程 → reject — 階數是實際出現的最高導數階數，這裡是 y″，所以是二階（S02）。
- 任何一階方程加上一個初值都恰有一個解 → reject — y′=3y^(2/3)、y(0)=0 有 y=0 與 y=x³ 兩個解；唯一性需要 Lipschitz 等假設。
- 方程本身就決定了解是 y=x² → reject — y₃=x²+eˣ 也滿足方程（S14）；要初值才把 y₁ 選出來。





## 結論與限制

y″−2y′+y=x²−4x+2 是二階常微分方程。y₁=x² 的殘差在整個 ℝ 上恆為零，所以是解；y₂=x²+x 的殘差是 x−2，只在 x=2 為零，所以不是 ℝ 上的解。y₁ 滿足 y(0)=0、y′(0)=0，依二階線性方程的存在唯一定理（係數連續，citation_verified）它是此初值問題的唯一解；沒有初值時 y₃=x²+eˣ 也是解，所以方程本身不決定唯一解。


- 本輪改以已核對的 Trench《Elementary Differential Equations with Boundary Value Problems》§5.3 定理 5.3.1 支持 thm_linear_ivp。原 Boyce–DiPrima 版次與編號留作來源沿革，未冒稱已查閱；本稿沒有重證該定理。
- 非線性例 y′=3y^(2/3) 只在錯誤控制與負控制中作說明，沒有逐步推導。





## 驗證及來源綁定

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


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

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