totalEnergy
plain-language theorem explainer
The total energy definition supplies E(t) as the standard Hamiltonian evaluated at trajectory position and its conjugate momentum. Researchers formalizing the J-action reduction to Newtonian mechanics cite this when moving to Hamiltonian form for conservation arguments. It is realized as a direct composition of the Hamiltonian and momentum definitions.
Claim. The total energy of trajectory $γ$ at time $t$ is $E(t) = p(t)^2/(2m) + V(γ(t))$, where the conjugate momentum is $p(t) = m dγ/dt(t)$.
background
The module derives the Hamiltonian formulation from the J-action via its small-strain limit. The standard Lagrangian is $L(q, q̇) = ½ m q̇² - V(q)$. Conjugate momentum is the partial of L with respect to velocity, giving $p = m γ̇$. The Hamiltonian is the Legendre transform $H = p q̇ - L$, which reduces to $p²/(2m) + V(q)$ for this L.
proof idea
One-line wrapper that applies the standard Hamiltonian definition to the position γ(t) and the conjugate momentum at time t.
why it matters
This definition is invoked by the energy conservation theorem and the Noether theorem for J-action, both of which establish constancy of total energy when the Euler-Lagrange equation holds. It fills the Hamiltonian formulation corollary in the companion paper RS_Least_Action.tex. It bridges J-cost potentials to classical conservation in the Newtonian limit of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.