conjugateMomentum
plain-language theorem explainer
Conjugate momentum is defined as p(t) equals m times the time derivative of trajectory gamma at t. Researchers deriving Hamiltonian mechanics from the J-action in Recognition Science cite this as the direct link from the small-strain Lagrangian to phase space variables. The definition is a one-line expression implementing the Legendre transform for the quadratic kinetic term.
Claim. The conjugate momentum is given by $p(t) = m$ times the derivative of trajectory $gamma$ at time $t$, for mass parameter $m$ and differentiable path $gamma : mathbb{R} to mathbb{R}$.
background
The module derives Hamiltonian mechanics from the J-action by taking its small-strain limit, where the Lagrangian becomes the standard form $L(q, dot{q}) = frac{1}{2} m dot{q}^2 - V(q)$. The conjugate momentum is introduced via the Legendre transform to obtain the Hamiltonian $H(q, p) = p^2/(2m) + V(q)$. This replaces an earlier scaffold version with concrete definitions and a conservation theorem, as noted in the module's companion paper section on Hamiltonian formulation as a corollary of least action.
proof idea
This is a one-line definition that directly encodes the partial derivative of the Lagrangian with respect to velocity, $p = partial L / partial dot{q} = m dot{q}$. It applies the standard expression for conjugate momentum in the quadratic kinetic limit without further lemmas.
why it matters
The definition supplies the phase-space coordinate used by totalEnergy, hamilton_equations_from_EL, and energy_conservation in the same module, as well as EnergyConservationCert. It completes the step from Euler-Lagrange to Hamilton's equations for the J-action, realizing the Hamiltonian formulation as a direct corollary. This connects to the Recognition Science least-action principle and the shift from Lagrangian to phase-space dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.