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

目標與範圍

在區間 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。

逐步主鏈

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

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

\text{order}=2

y_1(x)=x^2

y_1'(x)=2x

y_1'(x)=2x

y_1''(x)=2

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

2-2(2x)+x^2

2-2(2x)+x^2

x^2-4x+2

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

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

y_2(x)=x^2+x

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

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

r_{y_2}(x)=x-2

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}

y_1(0),\ y_1'(0)

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

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}

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

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

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

\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}

局部子步與引理

(x+h)^2-x^2

h(2x+h)

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

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

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

x^2-3x

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

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