energy_conservation_one_statement
plain-language theorem explainer
The declaration shows that the type EnergyConservationCert is inhabited, confirming total energy remains constant along Newtonian trajectories of the small-strain J-action. A researcher deriving Noether symmetries from variational principles or checking Hamiltonian conservation in classical mechanics would cite this result. The proof is a one-line term that supplies the pre-established energyConservationCert witness.
Claim. There exists a certificate such that for every mass $m > 0$, potential $V:ℝ→ℝ$, and trajectory $γ:ℝ→ℝ$ satisfying differentiability of $V$ and $γ$, differentiability of $γ'$, the factored derivative of total energy, and the standard Euler-Lagrange equation, the mechanical energy $H(γ(t),p(t))$ equals $H(γ(t_1),p(t_1))$ for all times $t_1,t_2$.
background
EnergyConservationCert is the structure whose sole field energy_conserved packages the universal statement of energy conservation for Newtonian trajectories under the small-strain J-action. The structure requires differentiability of $V$ and $γ$ at every point on the trajectory, differentiability of the velocity, a factorization condition on the time derivative of total energy, and satisfaction of the standard EL equation before concluding constancy of $H$ between arbitrary times.
proof idea
The proof is a one-line term wrapper that directly supplies the energyConservationCert definition as the inhabitant of Nonempty EnergyConservationCert. That definition in turn invokes HamiltonianMech.energy_conservation to discharge the energy_conserved clause.
why it matters
This theorem supplies the one-statement summary of energy conservation in the Recognition Science action module, completing the domain certificate that links the J-action to the standard Hamiltonian via Noether's theorem on time-translation symmetry. The module documentation positions it as the wrapper for results already proved in Action.Hamiltonian and references the companion paper RS_Least_Action.tex § Hamiltonian Formulation as a Corollary. No downstream declarations are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.