Action Euler Lagrange Cost Rate El Iff Const One

The unique ground state

The cost-rate action is a way to measure the total cost of a path through the cost manifold: it adds up the pointwise cost J(γ(t)) over time. Because the integrand depends only on the position γ(t) and not on velocity, the Euler–Lagrange equation simplifies dramatically. It reduces to the condition that the derivative of J vanishes at every point of the path, J'(γ(t)) = 0.

The declaration costRateEL_iff_const_one proves the equivalence: among admissible paths that stay positive, the cost-rate Euler–Lagrange equation holds if and only if the path is constantly at 1. In other words, the only critical point of the cost-rate action is the constant path at the cost minimum. This is a rigidity statement: no other positive path has zero first-order cost change at every point. The proof is a direct consequence of the fact that J'(1) = 0 and the derivative of J vanishes only at x = 1.

This result is the cleanest possible form of a least-action principle within the framework. It says there is exactly one trajectory in the cost manifold with no first-order cost variation at any instant, and that trajectory is the one that stays at the cost minimum forever. The constant-1 path is also a geodesic of the Hessian metric g(x) = J''(x) = 1/x³, which makes the cost-rate variational principle and the Hessian-energy variational principle agree on the unique ground state.

In Recognition Science, this theorem is a formal foundation: it shows that the framework's notion of a ground state is not a convention but a forced consequence of the variational structure. The machine-checked library records this as a proved theorem with no unproved assumptions. The declaration is part of a larger chain that derives physical constants and dimensionality from the cost function, but this particular result concerns only the variational principle itself.

What the declaration does not claim is equally important. It does not claim that the cost-rate action has a unique global minimum over all paths; it only identifies the critical points. It does not address paths that are not positive, and it does not apply to the Hessian-energy action, which has its own separate geodesic equation. The theorem is about the cost-rate action alone, and it is a statement about critical points, not about the action's value.

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

def eulerLagrange_status : String :=
  "Action.EulerLagrange: costRateEL_iff_const_one, geodesicEquationHolds, ground_state_is_unique_critical_point (0 sorry, 0 axiom)"

What this page does not claim

The cost-rate action has a unique global minimum over all paths, not just a unique critical point. The Hessian-energy action has the same Euler–Lagrange equation as the cost-rate action. The theorem applies to paths that are not strictly positive.

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: