hamiltonian_status
plain-language theorem explainer
hamiltonian_status supplies a diagnostic string confirming that the standard Hamiltonian, Hamilton's equations from the Euler-Lagrange equation, and energy conservation along Newtonian trajectories are realized in the Action module with zero sorries and zero axioms. A physicist deriving classical mechanics as the small-strain limit of the J-action would cite this to verify the reduction. It is realized as a one-line string literal that aggregates the status of the three core results.
Claim. The status of the Hamiltonian formulation derived from the J-action is the string reporting that the standard Hamiltonian $H(q,p)=p^2/(2m)+V(q)$, Hamilton's equations from the Euler-Lagrange equation, and energy conservation for trajectories satisfying the standard EL equation hold with zero sorries and zero axioms.
background
The module derives the Hamiltonian formulation from the J-action via the Legendre transform of the standard Lagrangian $L(q, q̇)=½ m q̇² - V(q)$, the small-strain limit of the recognition action. The conjugate momentum is $p = m q̇$, and the Hamiltonian is $H(q,p)=p q̇ - L = p²/(2m) + V(q)$. Hamilton's equations are direct corollaries of the EL equation. This replaces the scaffold-grade Foundation/Hamiltonian.lean with concrete definitions, per the module documentation and the paper companion section on Hamiltonian Formulation as a Corollary.
proof idea
The declaration is a one-line wrapper that returns the fixed string literal aggregating the status of standardHamiltonian, hamilton_equations_from_EL, and energy_conservation with their proof counts.
why it matters
This status declaration marks completion of the classical Hamiltonian sector in the Action module, connecting to the quantum Hamiltonian operator structure. It realizes the paper proposition on Hamiltonian formulation as a corollary to the least-action principle and links the Foundation energy conservation theorem (time-translation invariance implies conserved total Hamiltonian under RRF dynamics) to the concrete Newtonian case with the chain-rule identity dE/dt = q̇ · standardEL = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.