harmonic_energy_conserved
plain-language theorem explainer
The declaration establishes invariance of the classical harmonic-oscillator energy under its own time-evolution map. A physicist checking the Recognition Science derivation of Noether's theorem from cost stationarity would cite the result as the explicit time-translation case. The argument unfolds the flow, introduces the natural frequency, records the unit-circle identity, and reduces the transformed energy expression to the original via field simplification and ring normalization.
Claim. Let $m>0$, $k>0$. Let $E(q,p)=p^2/(2m)+k q^2/2$ be the harmonic energy and let $ϕ_t(q,p)$ be the phase-space flow with frequency $ω=√(k/m)$. Then $E(ϕ_t(q,p))=E(q,p)$ for every real $t$.
background
The module derives Noether's theorem from stationarity of the J-cost functional. Time translation is listed among the symmetries that must produce a conserved charge; the harmonic oscillator supplies the simplest dynamical test of that mechanism. Upstream material supplies the RS-native units in which energy, momentum and time are simply real numbers, together with auxiliary structures for nuclear densities and constants that are not invoked here.
proof idea
The proof unfolds the definitions of energy and flow, sets ω=√(k/m), proves positivity and the square relation, and records cos²+sin²=1. It then states an auxiliary claim for arbitrary c,s on the unit circle and proves the claim by rewriting k=mω², applying field_simp and ring_nf, substituting s²=1-c², and finishing with ring. The goal follows by instantiating the auxiliary claim at the cosine and sine of ωt.
why it matters
The result supplies the concrete energy-conservation instance required by the module summary that time translation yields energy conservation. It illustrates the Recognition Science claim that cost stationarity under a continuous symmetry produces a conserved quantity. The declaration belongs to the program of obtaining the full Noether correspondence from ledger balance; an open question is whether the same algebraic reduction extends to arbitrary potentials without further scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.