線性簡諧振子模型：資格、k/m、多項式候選的殘差與單點能量

目標與範圍

取 m=2、k=8。核對模型資格並算出 k/m；對多項式候選 x_c(t)=1−2t² 算出殘差 R(t)=m x_c''+k x_c，在指定點 t=0、1/2、1 求值，並證明 x_c 不是任何正長度區間上的解；證明方程 2x''+8x=0 沒有非零多項式解；最後算出單一狀態 (x,v)=(1,0) 的能量 E=4，並以能量導數恆等式說明單點能量值為何不證明守恆。

在 MKO 的範圍內工作：m、k 為正有理數；只核模型資格、k/m、多項式候選的指定點殘差與單一狀態能量式（假設 a1）。另證兩個與多項式及導數規則有關的引理：沒有非零多項式解，以及能量導數恆等式。不執行 sin/cos 閉式解、不證守恆定理或穩定性（假設 a2）；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• zero_product
• distributive
• power_laws
• quantifier_negation
• contradiction
• numeric_evaluation

• G1 — 模型（MKO）：正質量 m 與正彈性係數 k（正有理數），位移 x 滿足 m x''+k x=0。本例 m=2、k=8。
• G2 — 多項式候選 x_c(t)=1−2t²（整係數），指定的殘差核對點為 t=0、1/2、1。
• G3 — 狀態能量式 E(x,v)=m v²/2+k x²/2；要求值的單一狀態為 (x,v)=(1,0)。
• G4 — 資格對照用的非例：(m,k)=(0,8) 與 (m,k)=(2,−8)。

• m,\ k — 質量與彈性係數，皆為正有理數
• x(t) — 位移
• x_c(t)=1-2t^2 — 多項式候選
• R(t)=mx_c''(t)+kx_c(t) — 候選的殘差
• E(x,v)=\tfrac{m v^2}{2}+\tfrac{k x^2}{2} — 狀態能量式
• \tfrac{k}{m} — 角頻率平方候選

規則與來源

• 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。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• mko_sho · cited — 線性簡諧振子模型由正質量 m 與正彈性係數 k 組成，位移 x 滿足 m x''+k x=0。比值 k/m 是角頻率平方候選；只有另有三角函數及導數語義時才能建立一般閉式解。 · mko-harmonic-oscillator-model
• mko_deriv_rules · cited — 在相應點可微的實函數有 (f+g)'=f'+g'、(cf)'=cf'、(fg)'=f'g+fg'；若 g 在 x 可微且 f 在 g(x) 可微，(f∘g)'(x)=f'(g(x))g'(x)。本輪 f、g 是全 R 多項式，以常數項起算的升冪係數列表表示。 · mko-derivative-rules
• poly_deriv · prerequisite — 多項式導數：(t^j)'=j t^(j−1)（j≥1），常數的導數為 0，導數對和與常數倍線性。因此次數 d≥1 的多項式的導數次數為 d−1，常數的導數為零多項式。
• poly_roots · prerequisite — 次數 d 的非零多項式至多有 d 個實根；因此在一個正長度區間上處處為零的多項式是零多項式（所有係數為 0）。
• L_no_poly · lemma — 設 m、k 為非零常數。若多項式 x 在某個正長度區間上滿足 m x''+k x=0，則 x 是零多項式。
• L_energy · lemma — 若 x 在某區間上二次可微，令 E(t)=m x'(t)²/2+k x(t)²/2，則 E'(t)=x'(t)·(m x''(t)+k x(t))。

逐步主鏈

\text{linear harmonic oscillator}

mx''+kx=0,\ m>0,\ k>0

(m,k)=(2,8)

m>0\land k>0:\ \text{qualifies};\ (0,8),\ (2,-8)\ \text{do not}

\tfrac{k}{m}

\tfrac{8}{2}=4

x_c(t)=1-2t^2

x_c'(t)=-4t,\ x_c''(t)=-4

R(t)=m x_c''(t)+k x_c(t)

R(t)=-16t^2

t\in\{0,\tfrac{1}{2},1\}

R(0)=0,\ R(\tfrac{1}{2})=-4,\ R(1)=-16

R(t)=-16t^2

x_c\ \text{solves the equation on no interval of positive length}

x\ \text{polynomial},\ 2x''+8x=0\ \text{on an interval}

x=0

\text{nonzero solution}\ x

x\ \text{is not a polynomial}

E(1,0)

\tfrac{2\cdot 0^2}{2}+\tfrac{8\cdot 1^2}{2}=4

E(t)=E(x_c(t),x_c'(t))

E(t)=16t^2+4(1-2t^2)^2=4+16t^4

E(t)=\tfrac{m}{2}x'(t)^2+\tfrac{k}{2}x(t)^2

E'(t)=x'(t)\big(mx''(t)+kx(t)\big)

x_c'(t)R(t)=(-4t)(-16t^2)

64t^3=\tfrac{d}{dt}(4+16t^4)

m=2,\ k=8,\ x_c=1-2t^2,\ (x,v)=(1,0)

\text{qualifies};\ \tfrac{k}{m}=4;\ x_c\ \text{not a solution};\ \text{no nonzero polynomial solution};\ E(1,0)=4

局部子步與引理

2\cdot(-4)+8(1-2t^2)

-8+8-16t^2=-16t^2

x(t)=\sum_{j=0}^{d}a_jt^j,\ a_d\neq 0

[t^d]\,(kx)=k\,a_d\neq 0

x\ \text{of degree}\ d

[t^d]\,(mx'')=0

[t^d]\,(mx''+kx)=0+k\,a_d\neq 0

mx''+kx\neq 0\ \text{on any interval}\ \Rightarrow\ \bot

\big(\tfrac{m}{2}x'^2+\tfrac{k}{2}x^2\big)'

\tfrac{m}{2}\cdot 2x'x''+\tfrac{k}{2}\cdot 2xx'=x'(mx''+kx)

逐步反向審查

• S14 · sufficient_goal_reduction · S02, S03, S07, S08, S10, S13 — 目標 G：五項結論。足夠條件 H：S02、S03、S07、S08、S10、S13 各自成立；H⇒G 由合取。H 都由定義、導數規則與多項式事實正向得出，沒有把 G 當作前提。
• S13 · premise_audit · L_energy, S05, S11 — 例子是對引理的一致性核對，不是引理的證明（證明在 S12.1）；守恆需要的定理明確未用。
• S12.1 · inverse_equivalence · mko_deriv_rules, distributive — 導數唯一，兩邊是同一函數的兩種寫法。
• S12 · premise_audit · L_energy, mko_deriv_rules — 需要 x 二次可微，才能對 x' 再微分。
• S11 · inverse_equivalence · distributive, power_laws — 展開是對所有 t 成立的恆等式（N6 以次數 ≤4 的網格核對）。
• S10 · inverse_equivalence · numeric_evaluation — 精確代入。
• S09 · premise_audit · S08, contrapositive, mko_sho — 逆否與原命題等價；這一步刻意不往存在性推進。
• S08.3 · premise_audit · poly_roots, contradiction, S08.1, S08.2 — 矛盾需要「非零多項式根數有限」這一前置事實，以及區間長度為正（含無窮多點）。
• S08.2 · premise_audit · poly_deriv, case_analysis — 兩種情況涵蓋所有 d≥0。
• S08.1 · premise_audit · zero_product — 需要 k≠0；本模型 k>0 所以成立。
• S08 · premise_audit · L_no_poly, poly_deriv, poly_roots — 引理只用 k≠0、多項式導數的次數規則與根數上界；x=0 確實是解，所以結論是「只有零多項式」。
• S07 · premise_audit · quantifier_negation, square_nonneg, order_basics — 否定全稱只需一個見證點；這裡每個 t≠0 都是見證。
• S06 · inverse_equivalence · numeric_evaluation — 精確代入，可逐一重算。
• S05.1 · inverse_equivalence · distributive, add_inverse — 每一步都是對所有 t 成立的恆等式。
• S05 · inverse_equivalence · distributive, eq_replace — 代換與展開都是等值改寫；N2 以多項式恆等式核對。
• S04 · inverse_equivalence · poly_deriv — 導數唯一確定，兩邊指同一函數。
• S03 · inverse_equivalence · numeric_evaluation, frac_rules — 反向：4·2=8；精確有理數計算。
• S02 · premise_audit · G1, G4, and_intro_elim, de_morgan_logic — 合格需要兩項都成立；不合格只需一項失敗。
• S01 · premise_audit · G1, mko_sho — 此步只陳述模型，不推出新事實。

錯誤控制與反例

沒有三角函數語義就不宣稱 sin/cos 解

MKO 指出的誤解之一是未有三角函數導數支援就直接宣稱一般 sin/cos 解。本稿只用多項式與導數規則：x_c=1−2t² 看似某個餘弦的截斷，但殘差是 −16t²（S05）；而且 L_no_poly 證明沒有非零多項式解（S08）。非零解必須來自另外建立語義的函數，本稿不建立。

單點能量不是守恆定理

MKO 指出的另一誤解。E(1,0)=4 是一個狀態的數。沿候選 x_c，能量從 E(0)=4 變到 E(1)=20（S11）。由 L_energy，E'=x'·R，殘差沿整條曲線為零，足以使 E' 恆為零；再用「零導數函數為常數」定理可得能量恆定（S13）。殘差恆零不是任意候選曲線能量恆定的必要條件：x(t)=1 的速度為零，E(t)=4 恆定但殘差是 8。

單點殘差為零不是解

R(0)=0，但 R(1/2)=−4、R(1)=−16。是否為解要看整個區間上的殘差；有限個點為零也不夠，何況這裡只有一點。

• R(0)=0，所以 x_c=1−2t² 是 2x''+8x=0 的解 → reject — R(1)=−16≠0；R(t)=−16t² 只在 t=0 為零。
• 在 (x,v)=(1,0) 算得 E=4，所以能量沿軌道守恆 → reject — 單點值不涉及時間演化；沿 x_c 有 E(0)=4、E(1)=20。
• (m,k)=(0,8) 也是線性簡諧振子模型 → reject — 模型要求 m>0；m=0 時方程變成 8x=0，不再是二階方程。
• 取次數夠高的多項式，一定能找到 2x''+8x=0 的非零多項式解 → reject — L_no_poly：t^d 係數為 8a_d≠0，任何非零多項式都不是解。
• k/m=4，所以振子的頻率是 4 → reject — k/m 只是角頻率平方候選；把它轉成角頻率或頻率需要本稿未建立的三角函數語義。

結論與限制

m=2、k=8 的模型合格，k/m=4 是角頻率平方候選。多項式候選 x_c=1−2t² 的殘差為 R(t)=−16t²：R(0)=0、R(1/2)=−4、R(1)=−16，所以它不是任何正長度區間上的解；事實上 2x''+8x=0 沒有非零多項式解。單一狀態 (1,0) 的能量是 4；由 E'=x'(m x''+k x)，真正解的殘差恆零足以使 E' 恆零；由此推出區間上能量恆定仍需零導數常數定理，本稿未使用。反向不成立，例如曲線 x(t)=1 有 E(t)=4 恆定但殘差為8。單點能量值不證明守恆。

• 一般閉式解（例如以 cos 2t、sin 2t 表示）、能量守恆定理與穩定性屬於 MKO 的 formal next，需要三角函數導數與「零導數函數為常數」等定理，本稿未做。
• poly_roots（非零多項式根數有限）以前置知識使用，未在本稿證明；N2、N6、N8、N9、N10 是多項式恆等式的網格核對。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: b4e705c85a4a975387cba8996aea06dba3740d4a6e351d15e2887c3eea0e3093
• original source SHA-256: 554e271c524ba8ce10183cce3c7dd0413596c2f0895d68b7bdb617f4bf4ec344
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）