Action Euler Lagrange

The action principle

The Euler–Lagrange equation is the central tool of the calculus of variations. Given a quantity called an action, which is an integral over a path, the equation states the condition for that action to be stationary: a small change in the path produces no first-order change in the integral. In classical mechanics, this condition selects the physical trajectory from all possible ones. The equation takes the form ∂L/∂q − d/dt(∂L/∂q̇) = 0, where L is the Lagrangian, a function of position q and velocity q̇.

In the Recognition Science framework, the action principle applies to a cost manifold, a space of positive real numbers where each point represents a recognition cost. The framework's central cost function J(x) = (x + 1/x)/2 − 1 has a unique minimum at x = 1. The module Action.EulerLagrange formalizes two natural action functionals on this manifold and proves what the Euler–Lagrange equation demands of each.

The first is the cost-rate action S[γ] = ∫ J(γ(t)) dt, which integrates the pointwise cost along a path γ. Because the integrand depends only on γ and not on its derivative γ̇, the Euler–Lagrange equation reduces to J′(γ(t)) = 0. The module proves a clean equivalence: among admissible positive paths, the cost-rate Euler–Lagrange equation holds if and only if the path is constantly at γ(t) = 1. This is the rigidity statement: the only critical point of the cost-rate action is the constant ground state at the cost minimum.

The second functional is the Hessian-energy action E[γ] = ∫ ½ g(γ) γ̇² dt, where g(x) = J″(x) = 1/x³ is the Hessian metric on the cost manifold. This action measures kinetic energy in that metric. Its Euler–Lagrange equation is the geodesic equation γ̈ + Γ(γ) γ̇² = 0, with Christoffel symbol Γ(x) = −3/(2x). The module records this as a definitional equivalence: the geodesic equation and the Hessian-energy Euler–Lagrange equation refer to the same object. It also proves that the constant-1 path is a geodesic, trivially, since it has zero velocity and zero acceleration.

The headline result combines these two facts. The theorem ground_state_is_unique_critical_point states that the constant-1 path satisfies both the cost-rate Euler–Lagrange equation and the geodesic equation. The two variational principles, one seeking a path with zero pointwise cost gradient and the other seeking a geodesic, agree on the unique ground state: the constant path at the cost minimum. The module reports zero axioms and zero sorry, meaning the proofs are complete within the framework's machine-checked library of formal theorems.

What this establishes in plain language is that the action principle, applied to the cost manifold, does not produce a family of possible trajectories. It produces exactly one: the state of minimal cost, held forever. The framework's least-action principle is a statement of stability, not of motion.

/-- **Equivalence: cost-rate EL holds iff the path is constantly at `1`.**

    Among admissible (positive, continuous) paths, the constant ground
    state `γ ≡ 1` is the *unique* solution of the cost-rate EL equation.
    This is the cleanest possible "principle of least action": there is
    exactly one trajectory in the cost manifold that has no first-order
    cost change at every point, and it is the path that stays at the
    cost minimum forever. -/
theorem costRateEL_iff_const_one (γ : ℝ → ℝ) (hpos : ∀ t, 0 < γ t) :
    costRateELHolds γ ↔ ∀ t, γ t = 1 := by
  constructor
  · exact costRateEL_implies_const_one γ hpos
  · intro h t
    have h_eq : γ t = 1 := h t
    -- d/dx J at x = γ t = 1 is J'(1) = 0
    have hd := IndisputableMonolith.Cost.deriv_Jcost (x := γ t) (hpos t)
    rw [hd]
    unfold IndisputableMonolith.Cost.JcostDeriv
    rw [h_eq]
    norm_num

/-- The constant-1 path is a geodesic of the Hessian metric (trivially: zero
    velocity, zero acceleration). -/
theorem const_one_is_geodesic : geodesicEquationHolds (fun _ : ℝ => 1) := by
  intro t
  have h_deriv : deriv (fun _ : ℝ => (1 : ℝ)) = fun _ => 0 := by
    funext s; exact deriv_const s 1
  have h_deriv2 : deriv (deriv (fun _ : ℝ => (1 : ℝ))) t = 0 := by
    rw [h_deriv]; exact deriv_const t 0
  rw [h_deriv2, h_deriv]
  ring

/-- **Headline equivalence (1D, ground state).** Among admissible paths,
    the cost-rate EL has the constant-1 path as its unique solution
    (`costRateEL_iff_const_one`), and the constant-1 path is a geodesic
    of the Hessian metric (`const_one_is_geodesic`).

    Therefore the cost-rate variational principle (find a path with
    zero pointwise cost gradient) and the Hessian-energy variational
    principle (find a geodesic) **agree on the unique ground state**:
    the constant path at the cost minimum. -/
theorem ground_state_is_unique_critical_point :
    costRateELHolds (fun _ : ℝ => 1) ∧ geodesicEquationHolds (fun _ : ℝ => 1) :=
  ⟨costRateEL_const_one, const_one_is_geodesic⟩

What this page does not claim

The module does not prove that the Hessian-energy Euler–Lagrange equation has the constant-1 path as its unique solution among all admissible paths. The module does not establish that the geodesic equation has the explicit family γ(t) = (at + b)^(−2) as its general solution. The framework's action principle does not describe motion in physical space; it describes stability in the cost manifold.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Action/EulerLagrange.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: