harmonicFlow
plain-language theorem explainer
The harmonicFlow definition supplies the explicit time-evolution map for the classical harmonic oscillator in phase space. Researchers deriving Noether's theorem from cost stationarity in Recognition Science would cite it to check energy conservation by direct computation. The definition is constructed by substituting the standard trigonometric solution formulas with angular frequency sqrt(k/m).
Claim. The flow map sends time $t$ and phase point $(q,p)$ to the point with new position $q' = q cos(ω t) + (p/(m ω)) sin(ω t)$ and new momentum $p' = p cos(ω t) - m ω q sin(ω t)$, where $ω = sqrt(k/m)$, for parameters $m > 0$ and $k > 0$.
background
PhasePoint is the structure with real coordinates q for position and p for momentum. The module QFT.NoetherTheorem develops Noether's theorem from cost stationarity, where a symmetry leaves the J-cost unchanged and the corresponding charge is constant along solutions. The local setting states that time translation symmetry yields energy conservation as the basic example. Upstream results supply the Energy type from RSNativeUnits and ledger factorization structures that calibrate the J-cost.
proof idea
The definition is an explicit algebraic construction. It first computes ω as the positive square root of k/m, then applies the standard closed-form solution of the second-order oscillator equation to the input PhasePoint, producing the rotated (q,p) pair via the sine and cosine terms.
why it matters
This definition is the concrete test case that feeds the theorem harmonic_energy_conserved, which verifies energy is constant along the flow and thereby illustrates the module's core claim that Noether's theorem emerges from ledger balance under symmetry. It directly supports the paper proposition on Noether from ledger structure and the table entry that time translation conserves energy. It touches the open extension of the same mechanism to full quantum field theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.