# Linear harmonic oscillator: eligibility, k/m, residuals of a polynomial candidate and single-state energy

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-harmonic-oscillator-model/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

Take m=2 and k=8. Check that the parameters satisfy the model's requirements and compute k/m; for the polynomial candidate x_c(t)=1−2t², compute the residual R(t)=m x_c''+k x_c, evaluate it at the specified points t=0, 1/2, 1, and prove that x_c is not a solution on any interval of positive length; prove that the equation 2x''+8x=0 has no nonzero polynomial solution; finally compute the energy E=4 of the single state (x,v)=(1,0), and use the energy-derivative identity to explain why a single energy value proves no conservation.

Works inside the MKO's scope: m and k are positive rationals; only model eligibility, k/m, residuals of a polynomial candidate at specified points and a single-state energy expression are checked (assumption a1). Two lemmas about polynomials and the derivative rules are also proved: there is no nonzero polynomial solution, and the energy-derivative identity. No sin/cos closed-form solution, conservation theorem or stability proof is carried out (assumption a2); the canonical MKO and its English edition are not changed.





## Givens and symbols


- order_basics
- zero_product
- distributive
- power_laws
- quantifier_negation
- contradiction
- numeric_evaluation


- G1 — Model (MKO): positive mass m and positive spring coefficient k (positive rationals), with displacement x satisfying m x''+k x=0. Here m=2 and k=8.
- G2 — Polynomial candidate x_c(t)=1−2t² (integer coefficients), with the specified residual points t=0, 1/2 and 1.
- G3 — State energy expression E(x,v)=m v²/2+k x²/2; the single state to evaluate is (x,v)=(1,0).
- G4 — Non-instances for the eligibility check: (m,k)=(0,8) and (m,k)=(2,−8).


- m,\ k — mass and spring coefficient, positive rationals
- x(t) — displacement
- x_c(t)=1-2t^2 — the polynomial candidate
- R(t)=mx_c''(t)+kx_c(t) — the residual of the candidate
- E(x,v)=\tfrac{m v^2}{2}+\tfrac{k x^2}{2} — the state energy expression
- \tfrac{k}{m} — the angular-frequency-square candidate





## Rules and sources


- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- add_zero · prerequisite — Additive identity: u+0=u.
- square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- mko_sho · cited — A linear harmonic oscillator has positive mass m and positive spring coefficient k, with displacement x satisfying m*x″+k*x=0. The ratio k/m is the angular-frequency-square candidate. A general closed-form solution requires separately established trigonometric-function and derivative semantics. · mko-harmonic-oscillator-model
- mko_deriv_rules · cited — For real functions differentiable at the relevant points, (f+g)′=f′+g′, (cf)′=cf′, and (fg)′=f′g+fg′. If g is differentiable at x and f at g(x), then (f∘g)′(x)=f′(g(x))g′(x). Here f,g are polynomials defined on all of ℝ represented by ascending coefficients starting with the constant term. · mko-derivative-rules
- poly_deriv · prerequisite — Derivatives of polynomials: (t^j)'=j t^(j−1) for j≥1, constants have derivative 0, and differentiation is linear over sums and constant multiples. Hence the derivative of a polynomial of degree d≥1 has degree d−1, and the derivative of a constant is the zero polynomial.
- poly_roots · prerequisite — A nonzero polynomial of degree d has at most d real roots; hence a polynomial that vanishes everywhere on an interval of positive length is the zero polynomial (all coefficients 0).
- L_no_poly · lemma — Let m and k be nonzero constants. If a polynomial x satisfies m x''+k x=0 on some interval of positive length, then x is the zero polynomial.
- L_energy · lemma — If x is twice differentiable on an interval and E(t)=m x'(t)²/2+k x(t)²/2, then E'(t)=x'(t)·(m x''(t)+k x(t)).





## Main derivation

S01 · definitionBefore

\text{linear harmonic oscillator}

After

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

Conditions: m>0; k>0

Rule: mko_sho · Uses: G1, mko_sho

Leaf basis: mko_sho + def_intro

Fix the model as the MKO states it: positive mass m, positive spring coefficient k, and displacement x satisfying m x''+k x=0. The MKO is explicit that k/m is only called the angular-frequency-square candidate, and that a general closed form needs separately established trigonometric and derivative semantics, which this guide does not use.



S02 · impliesBefore

(m,k)=(2,8)

After

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

Conditions: none

Rule: and_intro_elim · Uses: S01, G1, G4

Leaf basis: and_intro_elim + de_morgan_logic + order_basics

Eligibility is the conjunction m>0 and k>0. Both hold for (2,8), so it qualifies. Non-instances: (0,8) has m=0, which is not positive; (2,−8) has k=−8<0. Neither belongs to this model, even though both can be written in the form m x''+k x=0 (with m=0 it is no longer even a second-order equation).



S03 · equivalentBefore

\tfrac{k}{m}

After

\tfrac{8}{2}=4

Conditions: m\neq 0

Rule: numeric_evaluation · Uses: S02, mko_sho

Leaf basis: numeric_evaluation + frac_rules

k/m=8/2=4, and m≠0 allows the division. By the MKO, 4 is called only the angular-frequency-square candidate; reading it as 'angular frequency 2' or as a 'frequency' needs trigonometric semantics, which this guide does not supply.



S04 · equivalentBefore

x_c(t)=1-2t^2

After

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

Conditions: none

Rule: poly_deriv · Uses: G2, poly_deriv

Leaf basis: poly_deriv + numeric_evaluation

(1)'=0 and (−2t²)'=−2·2t=−4t; differentiating again, (−4t)'=−4. Cross-check: x_c(t+h)−x_c(t)=−4t·h−2h² (N10, a polynomial identity); dividing by h and letting h→0 gives −4t.



S05 · equivalentBefore

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

After

R(t)=-16t^2

Conditions: none

Rule: distributive · Uses: S04, G1

Leaf basis: eq_replace + distributive

Substitute m=2, k=8 and the derivatives of S04, then expand and simplify (sub-step S05.1). The residual is the polynomial −16t², with a definite value for every t.



S06 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S05, G2

Leaf basis: numeric_evaluation

Evaluate the residual at the specified points: R(0)=0, R(1/2)=−16·1/4=−4 and R(1)=−16 (N3, N4). Only at t=0 is the residual zero.



S07 · impliesBefore

R(t)=-16t^2

After

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

Conditions: none

Rule: quantifier_negation · Uses: S05, S06, quantifier_negation

Leaf basis: quantifier_negation + square_nonneg + order_basics

For t≠0, t²>0, so R(t)=−16t²<0≠0. Every interval of positive length contains a point t≠0, where the residual is nonzero, so 'R(t)=0 for every t in the interval' fails. R(0)=0 is a single-point fact and cannot make x_c a solution.



S08 · impliesBefore

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

After

x=0

Conditions: m\neq 0; k\neq 0

Rule: L_no_poly · Uses: G1, poly_deriv, poly_roots

Leaf basis: contradiction + poly_deriv + poly_roots + zero_product

Prove Lemma L_no_poly: this equation has no nonzero polynomial solution. This shows that the failure in S07 is not a matter of choosing the wrong coefficients: no polynomial candidate other than zero can be a solution, and nonzero solutions must come from non-polynomial functions, such as trigonometric functions whose semantics must be established separately. Three sub-steps reach a contradiction by comparing leading coefficients.



S09 · impliesBefore

\text{nonzero solution}\ x

After

x\ \text{is not a polynomial}

Conditions: none

Rule: contrapositive · Uses: S03, S08, mko_sho

Leaf basis: contrapositive + mko_sho

The contrapositive of L_no_poly: a nonzero solution is not a polynomial. The MKO says a general closed form needs separately established trigonometric and derivative semantics; this guide establishes neither, so it claims no specific formula for a nonzero solution and does not even claim that one exists.



S10 · equivalentBefore

E(1,0)

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G3, G1

Leaf basis: numeric_evaluation

By the MKO, the energy expression can be used as a single-state quantity: E(1,0)=2·0/2+8·1/2=4 (N5). It is one number for one state and involves no evolution in time.



S11 · equivalentBefore

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

After

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

Conditions: none

Rule: distributive · Uses: S04, G3, G1

Leaf basis: distributive + power_laws + numeric_evaluation

Compute the energy along the candidate x_c: m x_c'²/2=(2/2)(16t²)=16t² and k x_c²/2=4(1−4t²+4t⁴)=4−16t²+16t⁴; the sum is E(t)=4+16t⁴ (N6). So E(0)=4 (the same state (1,0) as in S10), but E(1)=20 (N7): along this non-solution curve the energy is not constant.



S12 · impliesBefore

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

After

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

Conditions: x\ \text{twice differentiable}

Rule: L_energy · Uses: mko_deriv_rules

Leaf basis: mko_deriv_rules

Prove Lemma L_energy: along any twice-differentiable curve, the rate of change of the energy equals the velocity times the residual. An identically zero residual is sufficient for E' to vanish identically; the converse generally fails because the product can also vanish when the velocity is zero. One energy value provides no such interval-wide information.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: L_energy · Uses: S05, S11, S12, S04

Leaf basis: L_energy + poly_deriv + numeric_evaluation

Check the lemma on the candidate: x_c'·R=(−4t)(−16t²)=64t³ (N8), and the derivative of E(t)=4+16t⁴ from S11 is 64t³ (N9 checks this through a difference-quotient identity); they agree. The change in energy comes exactly from the nonzero residual. For a genuine solution the residual is identically zero, so E'(t)=0 at every point; concluding that E is constant would further need the theorem that a function with zero derivative on an interval is constant, which this guide does not use. The single-state value E=4 proves no conservation.



S14 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S02, S03, S07, S08, S10, S13

Leaf basis: and_intro_elim

Summary: (2,8) qualifies (S02) and k/m=4 is the angular-frequency-square candidate (S03); x_c has zero residual only at t=0 and solves the equation on no interval of positive length (S06, S07); there is no nonzero polynomial solution (S08); the single-state energy is E(1,0)=4 (S10), and for a genuine solution the identically zero residual makes E' identically zero (S12, S13), a sufficient direction. A single energy value proves no conservation, and E'≡0 alone does not imply a zero residual.







## Substeps and lemmas

S05.1 · equivalentBefore

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

After

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

Conditions: none

Rule: distributive · Uses: S04, G1, distributive

Leaf basis: distributive + add_inverse + add_zero

2·(−4)=−8; 8(1−2t²)=8−16t² by distributivity; −8+8=0, leaving −16t².



S08.1 · impliesBefore

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

After

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

Conditions: k\neq 0; a_d\neq 0

Rule: zero_product · Uses: poly_deriv, zero_product

Leaf basis: zero_product + distributive

Suppose, for contradiction, that x is not the zero polynomial, with degree d and leading coefficient a_d≠0. The t^d coefficient of k x is k a_d; since k≠0 and a_d≠0, the zero-product property gives k a_d≠0.



S08.2 · impliesBefore

x\ \text{of degree}\ d

After

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

Conditions: none

Rule: poly_deriv · Uses: S08.1, poly_deriv

Leaf basis: poly_deriv + case_analysis

If d≤1, x'' is the zero polynomial and m x''=0; if d≥2, differentiating twice lowers the degree to d−2<d, so m x'' has no t^d term. In both cases the t^d coefficient of m x'' is 0.



S08.3 · impliesBefore

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

After

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

Conditions: none

Rule: contradiction · Uses: S08.1, S08.2, poly_roots

Leaf basis: contradiction + poly_roots + add_assoc

Adding polynomials adds coefficients of equal degree, so the t^d coefficient of m x''+k x is 0+k a_d≠0; it is a nonzero polynomial with at most d roots and cannot vanish everywhere on an interval of positive length. This contradicts 'x solves the equation on that interval', so x is the zero polynomial. S08.1 to S08.3 prove Lemma L_no_poly.



S12.1 · equivalentBefore

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

After

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

Conditions: x\ \text{twice differentiable}

Rule: mko_deriv_rules · Uses: mko_deriv_rules

Leaf basis: mko_deriv_rules + distributive + mul_comm

Differentiate term by term with the sum and constant-multiple rules; by the product rule, (x'·x')'=x''x'+x'x''=2x'x'' and (x·x)'=2xx'. So E'=(m/2)·2x'x''+(k/2)·2xx'=m x'x''+k x x'=x'(m x''+k x) by distributivity. This proves Lemma L_energy.







## Reverse audits


- S14 · sufficient_goal_reduction · S02, S03, S07, S08, S10, S13 — Goal G: the five conclusions. Sufficient condition H: S02, S03, S07, S08, S10 and S13 each hold; H⇒G by conjunction. H is derived forwards from the definitions, the derivative rules and facts about polynomials; G is never used as a premise.
- S13 · premise_audit · L_energy, S05, S11 — The example is a consistency check of the lemma, not its proof (which is S12.1); the theorem conservation would need is explicitly not used.
- S12.1 · inverse_equivalence · mko_deriv_rules, distributive — Derivatives are unique, so both sides are two ways of writing the same function.
- S12 · premise_audit · L_energy, mko_deriv_rules — It needs x twice differentiable so that x' can be differentiated again.
- S11 · inverse_equivalence · distributive, power_laws — The expansion is an identity for all t (N6 checks it on a grid for degree ≤4).
- S10 · inverse_equivalence · numeric_evaluation — Exact substitution.
- S09 · premise_audit · S08, contrapositive, mko_sho — A contrapositive is equivalent to the original; this step deliberately does not move on to existence.
- S08.3 · premise_audit · poly_roots, contradiction, S08.1, S08.2 — The contradiction needs the prerequisite that a nonzero polynomial has finitely many roots, and an interval of positive length (with infinitely many points).
- S08.2 · premise_audit · poly_deriv, case_analysis — The two cases cover every d≥0.
- S08.1 · premise_audit · zero_product — It needs k≠0, which holds since k>0 in this model.
- S08 · premise_audit · L_no_poly, poly_deriv, poly_roots — The lemma uses only k≠0, the degree rule for derivatives of polynomials and the bound on the number of roots; x=0 is indeed a solution, so the conclusion is 'only the zero polynomial'.
- S07 · premise_audit · quantifier_negation, square_nonneg, order_basics — Negating a universal statement needs one witness; here every t≠0 is a witness.
- S06 · inverse_equivalence · numeric_evaluation — Exact substitution, recomputable one by one.
- S05.1 · inverse_equivalence · distributive, add_inverse — Each move is an identity valid for every t.
- S05 · inverse_equivalence · distributive, eq_replace — Substitution and expansion are rewritings of equals; N2 checks the result as a polynomial identity.
- S04 · inverse_equivalence · poly_deriv — Derivatives are uniquely determined, so both sides name the same function.
- S03 · inverse_equivalence · numeric_evaluation, frac_rules — Backward: 4·2=8; an exact rational computation.
- S02 · premise_audit · G1, G4, and_intro_elim, de_morgan_logic — Eligibility requires both conditions; failure of either rules the parameters out.
- S01 · premise_audit · G1, mko_sho — This step only states the model and derives no new fact.





## Error controls and negative controls

No sin/cos claim without trigonometric semanticsOne mistake named by the MKO is to declare the general sin/cos solution without support for trigonometric derivatives. This guide uses only polynomials and the derivative rules: x_c=1−2t² looks like a truncated cosine, but its residual is −16t² (S05), and L_no_poly proves there is no nonzero polynomial solution (S08). Nonzero solutions must come from functions whose semantics are established separately, which this guide does not do.

A single energy value is not a conservation theoremThe other mistake named by the MKO. E(1,0)=4 is a number for one state. Along the candidate x_c the energy changes from E(0)=4 to E(1)=20 (S11). By L_energy, E'=x'·R, so an identically zero residual is sufficient for E'≡0; the theorem that a zero-derivative function is constant then gives constant energy (S13). Zero residual is not necessary for constant energy along an arbitrary candidate curve: x(t)=1 has zero velocity and constant E(t)=4, but residual 8.

Zero residual at one point is not a solutionR(0)=0, but R(1/2)=−4 and R(1)=−16. Whether a candidate is a solution depends on the residual on the whole interval; zero at finitely many points is not enough, let alone at one point as here.


- R(0)=0, so x_c=1−2t² solves 2x''+8x=0 → reject — R(1)=−16≠0; R(t)=−16t² vanishes only at t=0.
- E=4 at (x,v)=(1,0), so energy is conserved along the trajectory → reject — A single value involves no evolution in time; along x_c, E(0)=4 and E(1)=20.
- (m,k)=(0,8) is also a linear harmonic oscillator model → reject — The model requires m>0; with m=0 the equation becomes 8x=0 and is no longer of second order.
- With a polynomial of high enough degree, a nonzero polynomial solution of 2x''+8x=0 can always be found → reject — L_no_poly: the t^d coefficient is 8a_d≠0, so no nonzero polynomial is a solution.
- k/m=4, so the oscillator's frequency is 4 → reject — k/m is only the angular-frequency-square candidate; turning it into an angular frequency or a frequency needs trigonometric semantics not established here.





## Result and limitations

The model with m=2 and k=8 qualifies, and k/m=4 is the angular-frequency-square candidate. The polynomial candidate x_c=1−2t² has residual R(t)=−16t²: R(0)=0, R(1/2)=−4 and R(1)=−16, so it solves the equation on no interval of positive length; in fact 2x''+8x=0 has no nonzero polynomial solution. The single state (1,0) has energy 4; since E'=x'(m x''+k x), an identically zero residual of a genuine solution is sufficient for E'≡0. Concluding constant energy on an interval still requires the zero-derivative theorem, which is not used here. The converse fails: x(t)=1 has constant E(t)=4 but residual 8. A single energy value proves no conservation.


- The general closed-form solution (for example in terms of cos 2t and sin 2t), the energy conservation theorem and stability belong to the MKO's formal next step; they need trigonometric derivatives and theorems such as 'a function with zero derivative is constant', and are not done here.
- poly_roots (a nonzero polynomial has finitely many roots) is used as a prerequisite and not proved here; N2, N6, N8, N9 and N10 are grid checks of polynomial identities.





## Verification and source binding

11 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-harmonic-oscillator-model-01.json)