applied
plain-language theorem explainer
Energy conservation along Newtonian trajectories follows from time-translation invariance of the J-action. A physicist reconstructing classical mechanics from the Recognition functional equation would cite the result to justify the Hamiltonian as a conserved Noether charge. The argument is a direct application of Noether's theorem to the time-invariant J-cost under standard differentiability assumptions on the potential and trajectory.
Claim. Let $H(q,p) = p^2/(2m) + V(q)$ be the Hamiltonian obtained as the Legendre transform of the Lagrangian $L = (1/2)m q̇^2 - V(q)$. Then for any trajectory $γ$ satisfying the Euler-Lagrange equations, with $V$ differentiable on the trajectory image and $γ$ twice differentiable, one has $H(γ(t_1),p(t_1)) = H(γ(t_2),p(t_2))$ and the pair $γ̇ = p/m$, $ṗ = -V'(γ)$ holds.
background
The J-cost satisfies the Recognition Composition Law. Its shift $H(x) = J(x) + 1 = ½(x + x^{-1})$ converts the law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$, as recorded in CostAlgebra.H. The module supplies the domain certificate for energy conservation in the small-strain J-action, building on the Lagrangian/EL chain already established in Action.Hamiltonian. Upstream results include the reparametrization of $H$ in Cost.FunctionalEquation and the Action/Energy abbreviations in RSNativeUnits. The local theoretical setting is the derivation of standard Newtonian mechanics as a corollary of J-action invariance under time translations, per the module documentation.
proof idea
one-line wrapper that applies Noether's theorem to time-translation symmetry of the J-action, confirming both energy conservation and the emergence of Hamilton's equations from the Euler-Lagrange equations under the regularity hypotheses.
why it matters
This supplies the energy-conservation statement invoked by downstream results such as bandEnergy in PeriodicTable and defect_moat_zero_iff_sat in CircuitLedger. It fills the Hamiltonian Formulation as a Corollary section in Paper A of papers/RS_Least_Action.tex. Within the Recognition framework it links T5 J-uniqueness and the RCL to classical Noether theorems, supporting emergence of the eight-tick octave and D = 3. It touches the open question of how discrete φ-tiers in NucleosynthesisTiers interface with continuous energy conservation in the classical limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.