Action Euler Lagrange Geodesic Iff Hessian Energy El

The geodesic equivalence

In classical mechanics and differential geometry, a geodesic is the straightest possible path between points on a curved surface or in a curved space. On a sphere, geodesics are great circles; in flat space, they are ordinary straight lines. A standard way to find geodesics is to minimize an energy functional, which measures the total kinetic energy of a particle moving along the path. The Euler–Lagrange equation of that energy functional is precisely the geodesic equation, a second-order differential equation that the minimizing path must satisfy.

The Recognition Science framework, a formal system built on a machine-checked library of theorems, applies this standard construction to its own cost manifold. The framework's cost function J(x) = (x + 1/x)/2 - 1 has a second derivative J''(x) = 1/x³, which defines a metric on the positive real numbers. The Hessian-energy action is E[γ] = ∫ ½ g(γ) γ̇² dt, where g(x) = 1/x³. The framework's declaration geodesic_iff_hessianEnergy_EL states that a path γ satisfies the geodesic equation γ̈ + Γ(γ) γ̇² = 0, with Γ(x) = -3/(2x), if and only if it satisfies the Euler–Lagrange equation of this energy functional. This is a definitional equivalence: the two equations name the same mathematical object.

The framework also proves a companion result for a different action, the cost-rate action S[γ] = ∫ J(γ) dt. Its Euler–Lagrange equation reduces to J'(γ) = 0, which forces the path to be constantly at the cost minimum γ = 1. The framework proves that the constant path γ = 1 is also a geodesic of the Hessian metric, since it has zero velocity and zero acceleration. Thus both variational principles agree on the unique ground state: the constant path at the cost minimum. This agreement is the headline equivalence the declaration supports.

What the declaration does not claim is also precise. The equivalence is stated for one-dimensional paths on the positive real line, not for higher-dimensional spaces. The geodesic equation is derived from the Hessian-energy functional, but the framework does not prove that every solution of the geodesic equation is a global minimizer of the energy, only that it satisfies the local Euler–Lagrange condition. The declaration does not assert that the cost-rate action and the Hessian-energy action are the same functional; they are distinct, and the framework's result is that they share the same ground-state solution.

/-- 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

What this page does not claim

The declaration does not prove that every geodesic is a global energy minimizer, only that it satisfies the local Euler–Lagrange equation. The equivalence does not extend to higher-dimensional cost manifolds; it is stated for one-dimensional paths on the positive real line. The cost-rate action and the Hessian-energy action are distinct functionals; the framework shows they share a ground state, not that they are identical.

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: