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

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

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

derivation-mko-harmonic-oscillator-model-01 · production-20261019-adopted-96



## 目標與範圍

取 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))。





## 逐步主鏈

S01 · definition操作前

\text{linear harmonic oscillator}

操作後

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

條件：m>0; k>0

規則：mko_sho · 依賴：G1, mko_sho

葉節點依據：mko_sho + def_intro

依 MKO 固定模型：正質量 m、正彈性係數 k，位移 x 滿足 m x''+k x=0。MKO 特別限定：k/m 只稱為角頻率平方候選；一般閉式解需要另外建立的三角函數與導數語義，本稿不使用。



S02 · implies操作前

(m,k)=(2,8)

操作後

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

條件：無

規則：and_intro_elim · 依賴：S01, G1, G4

葉節點依據：and_intro_elim + de_morgan_logic + order_basics

模型資格是合取 m>0 且 k>0。(2,8) 兩項都成立，合格。非例：(0,8) 的 m=0 不是正數；(2,−8) 的 k=−8<0。這兩個非例都不屬於本模型，即使它們也能寫成 m x''+k x=0 的形式（m=0 時甚至不再是二階方程）。



S03 · equivalent操作前

\tfrac{k}{m}

操作後

\tfrac{8}{2}=4

條件：m\neq 0

規則：numeric_evaluation · 依賴：S02, mko_sho

葉節點依據：numeric_evaluation + frac_rules

k/m=8/2=4，m≠0 所以可除。依 MKO，4 只稱為角頻率平方候選；把它解讀成「角頻率 2」或「頻率」需要三角函數語義，本稿不做。



S04 · equivalent操作前

x_c(t)=1-2t^2

操作後

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

條件：無

規則：poly_deriv · 依賴：G2, poly_deriv

葉節點依據：poly_deriv + numeric_evaluation

(1)'=0，(−2t²)'=−2·2t=−4t；再微分：(−4t)'=−4。交叉核對：x_c(t+h)−x_c(t)=−4t·h−2h²（N10，多項式恆等式），除以 h 再令 h→0 得 −4t。



S05 · equivalent操作前

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

操作後

R(t)=-16t^2

條件：無

規則：distributive · 依賴：S04, G1

葉節點依據：eq_replace + distributive

代入 m=2、k=8 與 S04 的導數，展開化簡（子步 S05.1）。殘差是 t 的多項式 −16t²，對每個 t 都有確定的值。



S06 · equivalent操作前

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

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S05, G2

葉節點依據：numeric_evaluation

在指定點求殘差：R(0)=0，R(1/2)=−16·1/4=−4，R(1)=−16（N3、N4）。只有 t=0 的殘差為零。



S07 · implies操作前

R(t)=-16t^2

操作後

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

條件：無

規則：quantifier_negation · 依賴：S05, S06, quantifier_negation

葉節點依據：quantifier_negation + square_nonneg + order_basics

t≠0 時 t²>0，所以 R(t)=−16t²<0≠0。任何正長度區間都含有 t≠0 的點，在那裡殘差不為零，所以「區間上每個 t 都有 R(t)=0」不成立。R(0)=0 只是單點事實，不能使 x_c 成為解。



S08 · implies操作前

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

操作後

x=0

條件：m\neq 0; k\neq 0

規則：L_no_poly · 依賴：G1, poly_deriv, poly_roots

葉節點依據：contradiction + poly_deriv + poly_roots + zero_product

證明引理 L_no_poly：本方程沒有非零多項式解。這說明 S07 的失敗不是選錯係數：任何多項式候選（零除外）都不可能是解；非零解只能來自多項式以外的函數，例如另需建立語義的三角函數。分三個子步，以首項係數比較導出矛盾。



S09 · implies操作前

\text{nonzero solution}\ x

操作後

x\ \text{is not a polynomial}

條件：無

規則：contrapositive · 依賴：S03, S08, mko_sho

葉節點依據：contrapositive + mko_sho

L_no_poly 的逆否：非零解不是多項式。MKO 指出一般閉式解需要另外建立的三角函數及導數語義；本稿沒有建立它們，所以不宣稱任何具體的非零解公式，也不宣稱非零解存在。



S10 · equivalent操作前

E(1,0)

操作後

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

條件：無

規則：numeric_evaluation · 依賴：G3, G1

葉節點依據：numeric_evaluation

依 MKO，能量式可作為單一狀態的量值：E(1,0)=2·0/2+8·1/2=4（N5）。這是一個狀態的一個數，不涉及任何時間演化。



S11 · equivalent操作前

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

操作後

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

條件：無

規則：distributive · 依賴：S04, G3, G1

葉節點依據：distributive + power_laws + numeric_evaluation

沿候選 x_c 計算能量：m x_c'²/2=(2/2)(16t²)=16t²，k x_c²/2=4(1−4t²+4t⁴)=4−16t²+16t⁴；相加得 E(t)=4+16t⁴（N6）。所以 E(0)=4（與 S10 相同的狀態 (1,0)），但 E(1)=20（N7）：沿這條非解的曲線，能量不是常數。



S12 · implies操作前

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\ \text{twice differentiable}

規則：L_energy · 依賴：mko_deriv_rules

葉節點依據：mko_deriv_rules

證明引理 L_energy：能量沿任一二次可微曲線的變化率，等於速度乘以方程的殘差。殘差沿整條曲線恆為零，足以推出 E' 恆為零；反向一般不成立，因為乘積也可能因速度為零而為零。單點能量值本身不提供這些全區間資訊。



S13 · implies操作前

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

操作後

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

條件：無

規則：L_energy · 依賴：S05, S11, S12, S04

葉節點依據：L_energy + poly_deriv + numeric_evaluation

對候選驗證引理：x_c'·R=(−4t)(−16t²)=64t³（N8），而 S11 的 E(t)=4+16t⁴ 的導數是 64t³（N9 以差商恆等式核對），兩者一致。能量變化正來自非零殘差。對真正的解，殘差恆為零，所以 E'(t)=0 在每一點成立；要由此推出 E 為常數，還需要「導數恆為零的函數在區間上為常數」的定理，本稿沒有使用。單一狀態的 E=4 不證明任何守恆。



S14 · implies操作前

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

條件：無

規則：and_intro_elim · 依賴：S02, S03, S07, S08, S10, S13

葉節點依據：and_intro_elim

彙整：(2,8) 合格（S02），k/m=4 是角頻率平方候選（S03）；x_c 只在 t=0 殘差為零，不是任何正長度區間上的解（S06、S07）；沒有非零多項式解（S08）；單一狀態能量 E(1,0)=4（S10），對真正的解，殘差恆零使 E' 恆零（S12、S13），這是充分方向；單點能量值不證守恆，也不由 E' 恆零反推殘差恆零。







## 局部子步與引理

S05.1 · equivalent操作前

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

操作後

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

條件：無

規則：distributive · 依賴：S04, G1, distributive

葉節點依據：distributive + add_inverse + add_zero

2·(−4)=−8；8(1−2t²)=8−16t²（分配律）；−8+8=0，剩下 −16t²。



S08.1 · implies操作前

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

操作後

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

條件：k\neq 0; a_d\neq 0

規則：zero_product · 依賴：poly_deriv, zero_product

葉節點依據：zero_product + distributive

反設 x 不是零多項式，次數為 d、首項係數 a_d≠0。k x 的 t^d 係數是 k a_d；因 k≠0、a_d≠0，由零乘積性質 k a_d≠0。



S08.2 · implies操作前

x\ \text{of degree}\ d

操作後

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

條件：無

規則：poly_deriv · 依賴：S08.1, poly_deriv

葉節點依據：poly_deriv + case_analysis

若 d≤1，x''是零多項式，m x''=0；若 d≥2，兩次微分使次數降為 d−2<d，所以 m x'' 沒有 t^d 項。兩種情況下 m x'' 的 t^d 係數都是 0。



S08.3 · implies操作前

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

操作後

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

條件：無

規則：contradiction · 依賴：S08.1, S08.2, poly_roots

葉節點依據：contradiction + poly_roots + add_assoc

多項式相加時同次係數相加，所以 m x''+k x 的 t^d 係數是 0+k a_d≠0，它是非零多項式，至多有 d 個根，不可能在正長度區間上處處為零。這與「x 在該區間上是解」矛盾，所以 x 是零多項式。S08.1 至 S08.3 證得引理 L_no_poly。



S12.1 · equivalent操作前

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

條件：x\ \text{twice differentiable}

規則：mko_deriv_rules · 依賴：mko_deriv_rules

葉節點依據：mko_deriv_rules + distributive + mul_comm

依和與常數倍規則逐項微分；由乘積規則，(x'·x')'=x''x'+x'x''=2x'x''，(x·x)'=2xx'。所以 E'=(m/2)·2x'x''+(k/2)·2xx'=m x'x''+k x x'=x'(m x''+k x)（分配律）。這證得引理 L_energy。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-harmonic-oscillator-model-01.json)