Action Euler Lagrange Euler Lagrange Status

Two actions, one ground state

The Euler-Lagrange equation is the classical workhorse of physics: given a quantity called an action, which assigns a number to every possible path a system might take, the equation picks out the paths where that number is unchanged to first order under small tweaks. In the Recognition Science framework, the action is built from the framework's cost function J, and the library asks what happens when the action depends only on where the path is, not on how fast it moves.

The first action, the cost-rate action, integrates the pointwise cost along the path. Because the integrand never mentions velocity, the Euler-Lagrange equation collapses to a single condition: the derivative of J must vanish at every point of the path. The library proves that among positive paths, this condition holds if and only if the path is constantly at the value 1, the unique minimum of J. That is the cleanest possible least-action principle: exactly one trajectory has no first-order cost change anywhere, and it is the path that sits at the cost minimum forever.

The second action, the Hessian-energy action, integrates a kinetic term built from the second derivative of J, which defines a metric g(x) = 1/x³ on the positive real line. For this action, the Euler-Lagrange equation is exactly the geodesic equation of that metric, the condition for a path to be the shortest or straightest route in the curved geometry. The library records this equivalence as a definitional fact, and it proves that the constant-1 path is a geodesic, trivially, since it has zero velocity and zero acceleration.

The headline result ties the two together: the cost-rate principle (find a path with zero pointwise cost gradient) and the Hessian-energy principle (find a geodesic) agree on the unique ground state, the constant path at the cost minimum. The declaration eulerLagrange_status is a string that names the three proved statements and records that they were checked with zero admitted proofs and zero added axioms. It is a status report, not a new theorem: it tells a reader which results in this framework are fully verified.

What the declaration does not claim is worth stating plainly. It does not assert that the constant-1 path is the only geodesic of the Hessian metric; other geodesics exist, such as the explicit family γ(t) = (at + b)⁻² verified elsewhere in the library. It does not claim that the cost-rate action has a unique global minimum among all paths, only that among positive paths the Euler-Lagrange condition forces the constant-1 path. And it says nothing about whether this variational structure extends beyond one dimension; the entire framework is confined to paths on the positive real line.

/-- The EL equation for the cost-rate action `S[γ] = ∫ J(γ) dt`.

    Since `L(q, q̇) = J(q)` does not depend on `q̇`, the EL equation
    reduces to `∂L/∂q = J'(q) = 0`. -/
def costRateELHolds (γ : ℝ → ℝ) : Prop :=
  ∀ t : ℝ, deriv Jcost (γ t) = 0

/-- **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 geodesic equation is the Euler–Lagrange equation of the
    Hessian-energy action `E[γ] = ∫ ½ g(γ) γ̇² dt`.

    This is a standard fact of Riemannian geometry: for a metric
    `g(x)` in 1D, the EL equation of the energy functional
    `E[γ] = ∫ ½ g(γ) γ̇² dt` is exactly the geodesic equation
    `γ̈ + Γ(γ) γ̇² = 0` with `Γ = (1/2g) g'`.

    We record this as a definitional equivalence (the names of the two
    equations refer to the same mathematical object). The full proof of
    one direction (the geodesic family `γ(t) = (at+b)^(-2)` satisfies
    the equation) is in
    `IndisputableMonolith.Decision.VariationalCalculus.geodesic_correct_satisfies_equation`. -/
theorem geodesic_iff_hessianEnergy_EL (γ : ℝ → ℝ) :
    geodesicEquationHolds γ ↔
    (∀ t : ℝ, deriv (deriv γ) t + christoffel (γ t) * (deriv γ t) ^ 2 = 0) :=
  Iff.rfl

/-- 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 declaration does not prove that the constant-1 path is the only geodesic of the Hessian metric. It does not establish global minimality of the cost-rate action among all paths, only the Euler-Lagrange condition among positive paths. It says nothing about higher-dimensional versions of these variational principles.

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: