IndisputableMonolith.Action.EulerLagrange
The module derives the Euler-Lagrange equation for the cost-rate action S[γ] = ∫ J(γ(t)) dt, reducing it to J'(q) = 0 because the Lagrangian L(q, q̇) = J(q) carries no velocity dependence. Researchers deriving equations of motion from the Recognition Science variational principle cite these results when moving from the action functional to dynamics. The argument applies the standard EL formula directly to the velocity-independent case after convexity of the action is secured upstream.
claimFor the action functional \(S[\gamma] = \int_a^b J(\gamma(t))\,dt\) with Lagrangian \(L(q,\dot q)=J(q)\), the Euler-Lagrange equation reduces to \(J'(q)=0\).
background
The module sits inside the variational setup of PathSpace, which defines admissible paths as continuous strictly positive functions on closed intervals together with the J-action integral and fixed-endpoint relations. Upstream, Cost.Convexity proves J(x) = ½(x + x⁻¹) - 1 is strictly convex on ℝ₊, while FunctionalConvexity establishes convexity of the full integral functional S[γ] and removes the conditional h_min witness. The local theoretical setting is the principle of least action applied to the d'Alembert cost functional J.
proof idea
The module assembles a chain of lemmas (costRateELHolds, costRateEL_const_one, costRateEL_implies_const_one, costRateEL_iff_const_one) that verify the EL equation for the cost-rate action. Each step applies the standard partial derivative ∂L/∂q = J'(q) and sets the result to zero, using the velocity independence already noted in the module doc-comment. The structure is a sequence of direct algebraic reductions and equivalences rather than deep tactic sequences.
why it matters in Recognition Science
This module supplies the equations of motion obtained from the J-action and is imported by the Hamiltonian module to construct the Legendre transform and Hamilton's equations. It fills the variational step that connects the action functional to dynamics in the Recognition Science framework, resting on the convexity results that support T5 J-uniqueness. The downstream Hamiltonian doc-comment explicitly references the small-strain limit of the same J-action.
scope and limits
- Does not treat Lagrangians with explicit time or velocity dependence.
- Does not derive the geodesic equation without the Hessian metric.
- Does not address variable-endpoint problems.
- Does not prove existence or uniqueness of solutions to the EL equation.
used by (1)
depends on (4)
declarations in this module (12)
-
def
costRateELHolds -
theorem
costRateEL_const_one -
theorem
costRateEL_implies_const_one -
theorem
costRateEL_iff_const_one -
def
hessianMetric -
lemma
hessianMetric_eq -
def
christoffel -
def
geodesicEquationHolds -
theorem
geodesic_iff_hessianEnergy_EL -
theorem
const_one_is_geodesic -
theorem
ground_state_is_unique_critical_point -
def
eulerLagrange_status