# 初值問題：逐一審核四個多項式候選 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-initial-value-problem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-initial-value-problem-01 · production-20261019-adopted-96 ## 目標與範圍 初值問題：在 ℝ 上 y''(x)=6x，且 y(0)=1、y'(0)=2。逐一審核四個整係數多項式候選 y_A=x³+2x+1、y_B=x³+1、y_C=x²+2x+1、y_D=3x⁵−15x⁴+21x³+2x+1：分開核對方程殘差與兩個初值，判定哪一個是此初值問題的解，並說明只核初值、只核一個初值、或只在有限網格上核殘差為何都不夠。 在 MKO 的範圍內工作：整係數多項式候選、明示初值與指定的有限殘差網格（假設 a1）。候選 y_A 的殘差以多項式導數規則符號化算出，因此在整個 ℝ 上為零；y_D 示範有限網格核對的限度。本稿不宣稱解唯一、不求一般解、不討論最大解區間（假設 a2）；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - distributive - eq_replace - numeric_evaluation - and_intro_elim - quantifier_negation - forall_elim - G1 — 初值問題：未知函數 y:ℝ→ℝ 滿足二階常微分方程 y''(x)=6x（對每個 x∈ℝ），以及初始資料 y(0)=1、y'(0)=2（x0=0、y0=1、v0=2）。 - G2 — 候選（ℝ 上的整係數多項式）：y_A=x³+2x+1，y_B=x³+1，y_C=x²+2x+1，y_D=3x⁵−15x⁴+21x³+2x+1。 - G3 — 殘差定義為 R_y(x)=y''(x)−6x；為候選 y_D 指定的有限殘差網格是 {0,1,2}。 - y_A,\ y_B,\ y_C,\ y_D — 四個多項式候選 - R_y(x)=y''(x)-6x — 候選 y 的方程殘差 - (E) — 方程責任：對所有 x∈ℝ，R_y(x)=0 - (I_1),\ (I_2) — 初值責任：y(0)=1、y'(0)=2 - \{0,1,2\} — 為 y_D 指定的有限殘差網格 ## 規則與來源 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - mko_ivp · cited — 初值問題由常微分方程及同一未知函數在指定點的初始資料組成。一階問題常給 y(x0)=y0；二階問題通常需 y(x0)=y0 與 y'(x0)=v0。候選解必須同時滿足方程與初值。 · mko-initial-value-problem - mko_ode_residual · cited — 常微分方程是在指定區間上，關聯未知單變數函數 y 與其有限階導數的方程。方程中出現的最高導數階數稱為階數；把候選 y 代入並得零殘差，只核對該候選在指定範圍是否滿足方程。 · mko-ordinary-differential-equation - poly_deriv · prerequisite — 多項式導數：多項式在 ℝ 上處處可微；(x^k)'=k x^(k−1)（k≥1），常數的導數為 0，且 (f+g)'=f'+g'、(cf)'=cf'。 ## 逐步主鏈 S01 · definition操作前 \text{initial-value problem} 操作後 y''(x)=6x\ (x\in\mathbb{R}),\ y(0)=1,\ y'(0)=2 條件：無 規則：mko_ivp · 依賴：G1, mko_ivp 葉節點依據：mko_ivp + def_intro 依 MKO，初值問題由方程與同一未知函數在指定點的初始資料組成。這裡方程是二階的（最高導數 y''），所以初始資料給兩個：y(0)=1 與 y'(0)=2。兩者都是對同一個函數 y、在同一點 x0=0 的要求。 S02 · equivalent操作前 y\ \text{solves the IVP} 操作後 (E)\ \forall x\in\mathbb{R}:\ R_y(x)=0\ \land\ (I_1)\ y(0)=1\ \land\ (I_2)\ y'(0)=2 條件：無 規則：def_unfold · 依賴：S01, G3, mko_ode_residual 葉節點依據：def_unfold + and_intro_elim 展開「是初值問題的解」：候選必須同時負起三個責任：方程責任 (E)，即殘差 R_y(x)=y''(x)−6x 在整個 ℝ 上為零；以及兩個初值責任 (I1)、(I2)。三者是合取，任何一項失敗，候選就不是此初值問題的解。 S03 · equivalent操作前 y_A=x^3+2x+1 操作後 y_A'=3x^2+2,\ y_A''=6x 條件：無 規則：poly_deriv · 依賴：G2, poly_deriv 葉節點依據：poly_deriv 用多項式導數規則逐項求 y_A 的一階與二階導數，分兩個子步。 S04 · equivalent操作前 R_{y_A}(x)=y_A''(x)-6x 操作後 R_{y_A}(x)=6x-6x=0\ \ \forall x\in\mathbb{R} 條件：無 規則：eq_replace · 依賴：S03, S02 葉節點依據：eq_replace + add_inverse + forall_intro 代入 y_A''=6x：R_{y_A}(x)=6x−6x=0。這是對每個實數 x 都成立的代數恆等式，不是在若干點上取樣的結果，所以方程責任 (E) 在整個 ℝ 上成立。 S05 · equivalent操作前 y_A(0),\ y_A'(0) 操作後 y_A(0)=1,\ y_A'(0)=2 條件：無 規則：numeric_evaluation · 依賴：G2, S03 葉節點依據：numeric_evaluation + forall_elim 代入 x=0：y_A(0)=0+0+1=1，y_A'(0)=3·0+2=2。兩個初值責任 (I1)、(I2) 都成立。注意 y_A'(0) 要用導數 y_A'，不是 y_A 本身。 S06 · implies操作前 (E),\ (I_1),\ (I_2)\ \text{for}\ y_A 操作後 y_A\ \text{solves the IVP on}\ \mathbb{R} 條件：無 規則：and_intro_elim · 依賴：S02, S04, S05 葉節點依據：and_intro_elim + def_unfold 三個責任都已證明（S04、S05），依 S02，y_A 是此初值問題在 ℝ 上的解。這同時說明此問題至少有一個解；本稿不宣稱解唯一。 S07 · implies操作前 y_B=x^3+1 操作後 R_{y_B}\equiv 0,\ y_B(0)=1,\ y_B'(0)=0\neq 2 條件：無 規則：poly_deriv · 依賴：G2, poly_deriv, S02 葉節點依據：poly_deriv + de_morgan_logic + numeric_evaluation y_B'=3x²，y_B''=6x，所以 R_{y_B}(x)=6x−6x=0 對所有 x 成立，(E) 成立；y_B(0)=1，(I1) 成立；但 y_B'(0)=3·0=0≠2，(I2) 失敗。依 S02，y_B 滿足方程，卻不是此初值問題的解。 S08 · implies操作前 y_A,\ y_B\ \text{both satisfy}\ (E),\ (I_1) 操作後 y_A(1)=4\neq 2=y_B(1) 條件：無 規則：numeric_evaluation · 依賴：S04, S05, S07 葉節點依據：numeric_evaluation + exists_intro y_A 與 y_B 都滿足方程與 y(0)=1，但 y_A(1)=1+2+1=4，y_B(1)=1+1=2，兩者是不同的函數。所以只給 y(0)=1 不足以挑出一個解；第二個初值 y'(0)=2 才把 y_B 排除。這就是 MKO 說二階問題通常需要 y(x0) 與 y'(x0) 兩個資料的原因。 S09 · implies操作前 y_C=x^2+2x+1 操作後 y_C(0)=1,\ y_C'(0)=2,\ R_{y_C}(0)=2\neq 0 條件：無 規則：quantifier_negation · 依賴：G2, poly_deriv, S02 葉節點依據：quantifier_negation + poly_deriv + numeric_evaluation y_C'=2x+2，y_C''=2。初值：y_C(0)=1、y_C'(0)=2，兩個都成立。但 R_{y_C}(x)=2−6x，在 x=0 得 R_{y_C}(0)=2≠0。要否定「對所有 x，R(x)=0」，找到一個 x 使 R(x)≠0 就夠了；所以 (E) 失敗，y_C 不是解。只核初值的人會誤收 y_C。 S10 · equivalent操作前 y_D=3x^5-15x^4+21x^3+2x+1 操作後 y_D'=15x^4-60x^3+63x^2+2,\ y_D''=60x^3-180x^2+126x 條件：無 規則：poly_deriv · 依賴：G2, poly_deriv 葉節點依據：poly_deriv + numeric_evaluation 逐項求 y_D 的一階與二階導數，分兩個子步；係數的乘法在 N2 至 N7 精確核對。 S11 · equivalent操作前 R_{y_D}(x)=y_D''(x)-6x 操作後 R_{y_D}(x)=60x^3-180x^2+120x=60x(x-1)(x-2) 條件：無 規則：distributive · 依賴：S10, G3 葉節點依據：distributive + add_assoc + numeric_evaluation R_{y_D}(x)=60x³−180x²+126x−6x=60x³−180x²+120x。提出公因式：60x(x²−3x+2)，而 x²−3x+2=(x−1)(x−2)。所以 R_{y_D}(x)=60x(x−1)(x−2)；N9 以多項式恆等式核對。 S12 · implies操作前 x\in\{0,1,2\} 操作後 R_{y_D}(0)=R_{y_D}(1)=R_{y_D}(2)=0,\ y_D(0)=1,\ y_D'(0)=2 條件：無 規則：zero_product · 依賴：S11, G2, G3, S10 葉節點依據：zero_product + numeric_evaluation 在指定網格上，60x(x−1)(x−2) 的某個因子為零，所以三點的殘差都是 0（N10）。初值：y_D(0)=1（只剩常數項），y_D'(0)=2（只剩常數項 2）。y_D 通過了這份有限網格加初值的審核。 S13 · implies操作前 R_{y_D}(3) 操作後 60\cdot 3\cdot 2\cdot 1=360\neq 0\ \Rightarrow\ y_D\ \text{not a solution} 條件：無 規則：quantifier_negation · 依賴：S11, S12, S02 葉節點依據：quantifier_negation + numeric_evaluation 在網格外取 x=3：R_{y_D}(3)=60·3·2·1=360≠0。所以「對所有 x，R(x)=0」不成立，(E) 失敗，y_D 不是此初值問題的解，雖然它通過了 S12 的有限審核。這正是 MKO 的提醒：有限點上殘差為零不是整個區間上的恆等證明。 S14 · implies操作前 y_A,\ y_B,\ y_C,\ y_D 操作後 \text{only}\ y_A\ \text{solves the IVP among the four candidates} 條件：無 規則：case_analysis · 依賴：S06, S07, S09, S13 葉節點依據：case_analysis + and_intro_elim 四個候選逐一判定：y_A 三個責任都成立（S06）；y_B 失敗於 y'(0)（S07）；y_C 失敗於方程（S09）；y_D 只通過有限網格，失敗於 x=3 的方程（S13）。結論只涵蓋這四個候選：y_A 是解，其餘不是。 ## 局部子步與引理 S03.1 · equivalent操作前 (x^3+2x+1)' 操作後 3x^2+2 條件：無 規則：poly_deriv · 依賴：G2, poly_deriv 葉節點依據：poly_deriv + numeric_evaluation 和的導數是導數的和：(x³)'=3x²，(2x)'=2·(x)'=2，(1)'=0，所以 y_A'=3x²+2。交叉核對：y_A(x+h)−y_A(x)=h(3x²+2)+3xh²+h³（N1，多項式恆等式），除以 h 再令 h→0 得 3x²+2。 S03.2 · equivalent操作前 (3x^2+2)' 操作後 6x 條件：無 規則：poly_deriv · 依賴：S03.1, poly_deriv 葉節點依據：poly_deriv 再求一次導數：(3x²)'=3·2x=6x，(2)'=0，所以 y_A''=6x。 S10.1 · equivalent操作前 (3x^5-15x^4+21x^3+2x+1)' 操作後 15x^4-60x^3+63x^2+2 條件：無 規則：poly_deriv · 依賴：G2, poly_deriv 葉節點依據：poly_deriv + numeric_evaluation (3x⁵)'=5·3x⁴=15x⁴，(−15x⁴)'=−4·15x³=−60x³，(21x³)'=3·21x²=63x²，(2x)'=2，(1)'=0。 S10.2 · equivalent操作前 (15x^4-60x^3+63x^2+2)' 操作後 60x^3-180x^2+126x 條件：無 規則：poly_deriv · 依賴：S10.1, poly_deriv 葉節點依據：poly_deriv + numeric_evaluation (15x⁴)'=4·15x³=60x³，(−60x³)'=−3·60x²=−180x²，(63x²)'=2·63x=126x，(2)'=0。 ## 逐步反向審查 - S14 · sufficient_goal_reduction · S06, S07, S09, S13 — 目標 G：四個候選的判定。足夠條件 H：S06、S07、S09、S13 四個各別判定，這四種情況涵蓋全部候選；H⇒G 由分情況論證。H 由導數規則與精確代入正向得出，沒有把 G 當作前提。 - S13 · premise_audit · S11, quantifier_negation, S02 — 一個見證點 x=3 就足以否定全稱命題（N11）。 - S12 · premise_audit · S11, zero_product, numeric_evaluation — 這些都是在有限個點上的事實；不宣稱反向，即不由這三點推出 (E) 在 ℝ 上成立（S13 證明它不成立）。 - S11 · inverse_equivalence · distributive, numeric_evaluation — 反向展開 60x(x−1)(x−2) 回到 60x³−180x²+120x；兩者是同一多項式（N9 在 0 到 3 的網格上核對三次多項式恆等式）。 - S10.2 · inverse_equivalence · poly_deriv — 同 S10.1；係數乘法見 N5、N6、N7。 - S10.1 · inverse_equivalence · poly_deriv — 逐項套用規則；係數乘法見 N2、N3、N4。 - S10 · inverse_equivalence · poly_deriv — 導數唯一，兩邊指同一函數。 - S09 · premise_audit · quantifier_negation, poly_deriv, S02 — ¬∀x P(x) ⇔ ∃x ¬P(x)；見證 x=0 已明示並精確核對（N8）。 - S08 · premise_audit · S04, S05, S07, numeric_evaluation — 一個具體的反例（兩個不同的函數）就足以說明一個初值不夠；不宣稱兩個初值必定足以保證唯一，那需要另外的論證。 - S07 · premise_audit · poly_deriv, S02, numeric_evaluation — 否定一個合取只需一項失敗，這裡是 (I2)；不宣稱 y_B 在其他意義下不好，它確實是方程的解。 - S06 · premise_audit · S02, S04, S05, and_intro_elim — 合取需要三項全部成立；不宣稱反向的唯一性：找到一個解並不排除其他解。 - S05 · inverse_equivalence · numeric_evaluation — 精確代入，兩邊同值。 - S04 · inverse_equivalence · eq_replace, add_inverse — 以相等的式子代換，並用 u−u=0；對每個 x 兩邊同值。 - S03.2 · inverse_equivalence · poly_deriv — 同 S03.1，直接套用規則。 - S03.1 · inverse_equivalence · poly_deriv — 每一項都直接套用規則，所得函數唯一。 - S03 · inverse_equivalence · poly_deriv — 導數是唯一確定的函數，所以等式兩邊指同一個函數；N1 以差商恆等式交叉核對一階導數。 - S02 · inverse_equivalence · def_unfold, and_intro_elim — 這是定義的展開，兩向成立：三項都成立就是解，是解就三項都成立。 - S01 · premise_audit · G1, mko_ivp — 此步只寫出問題，不推出新事實；寫下初值本身並不保證有解或唯一解（MKO 第一段）。 ## 錯誤控制與反例 只核初值不核方程MKO 指出的第一個誤解。y_C 滿足 y(0)=1 與 y'(0)=2，但 y_C''=2，殘差 2−6x 在 x=0 就是 2（S09）。方程責任與初值責任要分開核對，任何一項失敗就不是候選解。 有限網格的零殘差不證明全區間解MKO 指出的第二個誤解。y_D 的殘差 60x(x−1)(x−2) 在網格 {0,1,2} 上全為零，初值也相符，但 R(3)=360（S12、S13）。有限採樣只能否定（找到非零點），不能單獨證明恆等於零；y_A 的殘差是以代數恆等式 6x−6x=0 證明對所有 x 為零。 二階問題需要兩個初值y_A 與 y_B 都滿足 y''=6x 與 y(0)=1，卻是不同的函數（S08）。只核 y(0) 會把 y_B 誤當成解；y'(0)=2 是必要的第二個資料。核 y'(0) 時要代入導數 y'，不是 y 本身。 - y_C(0)=1 且 y_C'(0)=2，所以 y_C 是此初值問題的解 → reject — R_{y_C}(x)=2−6x，R_{y_C}(0)=2≠0，方程不成立。 - y_D 在 0、1、2 的殘差都是 0 且初值相符，所以 y_D 是解 → reject — R_{y_D}(3)=60·3·2·1=360≠0。 - y_B 滿足 y''=6x 與 y(0)=1，所以是此初值問題的解 → reject — y_B'(0)=0≠2，第二個初值不成立。 - 找到一個滿足方程與初值的候選，就證明了解唯一 → reject — 存在一個解不推出沒有其他解；只給 y(0)=1 時 y_A 與 y_B 就是兩個不同的解。唯一性需要另外的論證，本稿沒有給。 ## 結論與限制 在四個候選中，只有 y_A=x³+2x+1 是初值問題 y''=6x、y(0)=1、y'(0)=2 在 ℝ 上的解：它的殘差恆為零，且兩個初值都成立。y_B=x³+1 滿足方程與 y(0)=1 但 y_B'(0)=0；y_C=x²+2x+1 滿足兩個初值但 R(0)=2；y_D 在網格 {0,1,2} 上殘差為零且初值相符，但 R(3)=360。本稿不宣稱解唯一。 - 本稿不證明此初值問題的解唯一。一條可能的路線是：兩解之差 w 滿足 w''=0、w(0)=0、w'(0)=0，再用「導數恆為零的函數在區間上為常數」（均值定理的推論）；這需要引用該定理，本稿未做。 - N1 與 N9 是多項式恆等式的網格核對（對每個變數的次數上限已給定），N10 只是三個點的有限核對；本稿的結論不依賴它們，它們是交叉核對。 ## 驗證及來源綁定 14 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 9ab9d67dde3d67d0467dfdb56a74490ed9fc771c9c18aba72aa959ee7d220859 - original source SHA-256: 9ab9d67dde3d67d0467dfdb56a74490ed9fc771c9c18aba72aa959ee7d220859 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-initial-value-problem-01.json)