Action Euler Lagrange Const One Is Geodesic

The constant path as geodesic

In classical mechanics, the Euler–Lagrange equation selects the path a system actually takes from the infinite set of possible paths. It turns the question of motion into a calculus problem: find the curve that makes a certain quantity, the action, stationary. The Recognition Science framework applies this same machinery to its own ledger, a discrete record of recognition events, by defining two natural action functionals on its cost manifold.

The first, the cost-rate action, integrates the pointwise cost along a path. Because the cost function depends only on position and not on velocity, its Euler–Lagrange equation reduces to a simple condition: the derivative of the cost must vanish at every point. The framework's machine-checked library of formal theorems proves that, among positive paths, the only solution is the constant path at the cost minimum, where the cost equals 1. This is the rigidity statement: the unique critical point of the cost-rate action is the ground state.

The second action, the Hessian-energy action, integrates the kinetic energy in a metric derived from the second derivative of the cost. The Euler–Lagrange equation of this energy functional is exactly the geodesic equation of that metric, a standard fact of Riemannian geometry. The theorem const_one_is_geodesic establishes the bridge between the two principles: the constant path at the cost minimum is a geodesic of this metric. It satisfies the geodesic equation trivially, because its velocity and acceleration are both zero.

The headline result combines these two facts. 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 is the unique solution to the first and a geodesic of the second. This is the cleanest possible form of a least-action principle: there is exactly one trajectory in the cost manifold with no first-order cost change at any point, and it is the path that stays at the cost minimum forever.

What this theorem does not claim is equally important. It does not assert that the constant path is the only geodesic of the Hessian metric; the explicit family γ(t) = (at+b)^(-2) also satisfies the geodesic equation. It does not establish that the cost-rate action has a global minimum, only that its critical points are constants. And it does not make any claim about the physical interpretation of the cost manifold itself, which remains a modeling choice within the framework.

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

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

/-- **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 constant path is the only geodesic of the Hessian metric. The cost-rate action attains a global minimum. The cost manifold itself has a physical interpretation beyond being a modeling choice.

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: