Pith. sign in
module module high

IndisputableMonolith.Action.Hamiltonian

show as:
view Lean formalization →

The Action.Hamiltonian module supplies the standard Hamiltonian H(q,p) = p²/2m + V(q) obtained as the Legendre transform of the quadratic-limit Lagrangian. Researchers bridging the J-cost to Newtonian mechanics cite these definitions for energy and momentum expressions. The module consists of definitions for conjugate momentum and total energy together with theorems that recover Hamilton's equations from the Euler-Lagrange chain.

claimThe standard Hamiltonian is $H(q,p)=p^2/(2m)+V(q)$, where the conjugate momentum satisfies $p=m\dot{q}$ and the underlying Lagrangian is $L(q,\dot{q})=\frac12 m\dot{q}^2-V(q)$.

background

The module belongs to the Action domain. It rests on the cost-rate action $S[\gamma]=\int J(\gamma(t)),dt$ formalized in EulerLagrange, whose integrand depends only on position. QuadraticLimit shows that in the small-strain regime $\gamma=1+\varepsilon$ the cost $J(\gamma)=\frac12(\gamma+\gamma^{-1})-1$ reduces to its quadratic Taylor term $\frac12\varepsilon^2$, converting the J-action into the standard kinetic Lagrangian. The Cost module supplies the base definition of $J$.

proof idea

This is a definition module, no proofs. It introduces standardHamiltonian and conjugateMomentum as direct transcriptions of the Legendre transform, then states hamilton_equations_from_EL and energy_conservation as the interface to the upstream Euler-Lagrange results.

why it matters in Recognition Science

The module is imported by EnergyConservationDomainCert, which certifies energy conservation along Newtonian trajectories from the Lagrangian/EL chain, and by Noether for symmetry results. It supplies the Hamiltonian step that completes the quadratic-limit bridge from the J-action to standard mechanics.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (8)