harmonicEnergy
plain-language theorem explainer
The harmonicEnergy definition supplies the classical energy functional for the harmonic oscillator in phase space. Researchers working on Noether theorems in Recognition Science would cite it when verifying conservation laws from cost stationarity. The definition is a direct transcription of the standard Hamiltonian expression using the PhasePoint structure.
Claim. For mass $m$ and spring constant $k$, the energy at phase point $(q,p)$ is $H(q,p) = p^2/(2m) + k q^2/2$.
background
The QFT-006 module derives Noether's theorem from cost stationarity in Recognition Science, where symmetries that leave the J-cost unchanged produce conserved charges. PhasePoint is the structure carrying position $q$ and momentum $p$. The upstream PhasePoint definition supplies the carrier for this energy expression, which the module uses to illustrate time-translation symmetry conserving energy.
proof idea
One-line definition that assembles the kinetic term $p^2/(2m)$ and potential term $k q^2/2$ directly from the fields of the PhasePoint argument.
why it matters
This definition feeds the downstream theorem harmonic_energy_conserved, which verifies energy conservation along the harmonic flow as an explicit check that Noether's theorem holds in the Recognition Science setting. It illustrates the general mechanism where cost stationarity under time translation yields the conserved Noether charge, aligning with the module's target of deriving conservation from ledger balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.