EnergyConservationCert
plain-language theorem explainer
EnergyConservationCert packages the conservation of total energy along Newtonian trajectories of the small-strain J-action together with the first Hamilton equation. A researcher invoking Noether time-translation symmetry in the J-action setting would cite the certificate to treat energy constancy as a domain fact rather than re-deriving it. The structure is witnessed by direct appeal to the energy-conservation theorem and the conjugate-momentum definition already established in the Hamiltonian module.
Claim. The certificate asserts that for mass $m>0$, potential $V$, and trajectory $γ$, whenever $V$, $γ$, and $γ̇$ are differentiable at the relevant points, the time derivative of total energy factors through the Euler-Lagrange operator, and the standard Euler-Lagrange equation holds, then $H(γ(t),p(t))$ is independent of $t$; additionally $γ̇(t)=p(t)/m$ where $p$ is the conjugate momentum $p=mγ̇$.
background
The module supplies a domain certificate for energy conservation derived from the J-action in the small-strain limit. Total energy is defined as $E(t)=H(γ(t),p(t))$ with the standard Hamiltonian $H(q,p)=p^2/(2m)+V(q)$ and conjugate momentum $p=mγ̇$. The Euler-Lagrange operator for the standard Lagrangian $L=½mγ̇²-V(q)$ is $ELγ=mγ̈(t)+V'(γ(t))$, whose vanishing recovers Newton's second law.
proof idea
The structure is introduced as a record with two fields. The energy_conserved field encodes constancy of total energy under the listed differentiability and EL hypotheses. The hamilton_qdot field encodes the velocity equation $γ̇=p/m$. The witness is obtained by applying the energy-conservation theorem from the Hamiltonian module to the first field and the definition of the q-dot equation to the second.
why it matters
The certificate supplies the interface through which the energy-conservation result enters the action domain, directly populating the inhabited-witness theorem energy_conservation_one_statement. It realizes the Hamiltonian formulation as a corollary of the J-action, consistent with the Recognition Science derivation via the functional equation, the eight-tick octave, and Noether symmetry under time translation. It touches the open question of extending the same conservation statements beyond the Newtonian domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.