初值問題：逐一審核四個多項式候選

目標與範圍

初值問題：在 ℝ 上 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'。

逐步主鏈

\text{initial-value problem}

y''(x)=6x\ (x\in\mathbb{R}),\ y(0)=1,\ y'(0)=2

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

y_A=x^3+2x+1

y_A'=3x^2+2,\ y_A''=6x

R_{y_A}(x)=y_A''(x)-6x

R_{y_A}(x)=6x-6x=0\ \ \forall x\in\mathbb{R}

y_A(0),\ y_A'(0)

y_A(0)=1,\ y_A'(0)=2

(E),\ (I_1),\ (I_2)\ \text{for}\ y_A

y_A\ \text{solves the IVP on}\ \mathbb{R}

y_B=x^3+1

R_{y_B}\equiv 0,\ y_B(0)=1,\ y_B'(0)=0\neq 2

y_A,\ y_B\ \text{both satisfy}\ (E),\ (I_1)

y_A(1)=4\neq 2=y_B(1)

y_C=x^2+2x+1

y_C(0)=1,\ y_C'(0)=2,\ R_{y_C}(0)=2\neq 0

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

R_{y_D}(x)=y_D''(x)-6x

R_{y_D}(x)=60x^3-180x^2+120x=60x(x-1)(x-2)

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

R_{y_D}(3)

60\cdot 3\cdot 2\cdot 1=360\neq 0\ \Rightarrow\ y_D\ \text{not a solution}

y_A,\ y_B,\ y_C,\ y_D

\text{only}\ y_A\ \text{solves the IVP among the four candidates}

局部子步與引理

(x^3+2x+1)'

3x^2+2

(3x^2+2)'

6x

(3x^5-15x^4+21x^3+2x+1)'

15x^4-60x^3+63x^2+2

(15x^4-60x^3+63x^2+2)'

60x^3-180x^2+126x

逐步反向審查

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