PhasePoint
PhasePoint packages a classical phase-space point as the ordered pair of real numbers (q, p) for position and momentum. Researchers deriving Noether's theorem from cost-stationarity in Recognition Science reference it when constructing explicit harmonic-oscillator models of conserved energy. The declaration is a bare structure with two fields and no computational or proof content.
claimA phase-space point is a pair $(q, p) ∈ ℝ × ℝ$ where $q$ is the position coordinate and $p$ is the conjugate momentum.
background
The module develops Noether's theorem from the stationarity of the Recognition Science cost functional. Upstream, the shifted cost H is defined by H(x) = J(x) + 1 = ½(x + x⁻¹), converting the Recognition Composition Law into the algebraic identity H(xy) + H(x/y) = 2 H(x) H(y). PhasePoint supplies the elementary carrier for the position-momentum data that appears in the harmonic-oscillator illustrations of conserved quantities.
proof idea
The declaration is a direct structure definition that introduces the two fields q and p with no further computation or proof.
why it matters in Recognition Science
PhasePoint supplies the concrete data type for the harmonic-oscillator examples that illustrate the general Noether correspondence between symmetries and conserved charges. It is used by harmonicEnergy to compute the classical energy p²/2m + k q²/2 and by harmonicFlow to exhibit the explicit time evolution that leaves this energy invariant. The construction sits inside the program of deriving Noether's theorem from cost stationarity, where time-translation symmetry yields energy conservation.
scope and limits
- Does not impose any metric or symplectic structure on the (q, p) plane.
- Does not encode the underlying J-cost or ledger balance.
- Does not generalize to higher-dimensional or field-theoretic phase spaces.
formal statement (Lean)
179structure PhasePoint where
180 q : ℝ -- position
181 p : ℝ -- momentum
182
183/-- Harmonic oscillator energy: H = p²/2m + kq²/2 -/