Action Euler Lagrange Cost Rate El Const One

The constant ground state

In the calculus of variations, the Euler-Lagrange equation is the condition a path must satisfy to be a stationary point of an action functional, the integral that assigns a number to each path. For an action of the form S[γ] = ∫ J(γ(t)) dt, where the integrand depends only on the position γ(t) and not on the velocity γ'(t), the equation simplifies drastically: it reduces to J'(γ(t)) = 0. The cost function J(x) = (x + 1/x)/2 - 1 has derivative J'(x) = (1 - x⁻²)/2, which vanishes only at x = 1. So the Euler-Lagrange equation says the path must sit at the point 1 at every instant.

The declaration costRateEL_const_one is the machine-checked proof that the constant path γ(t) = 1 satisfies this equation. The proof is a one-line computation: at x = 1, the derivative is (1 - 1)/2 = 0. The companion theorem costRateEL_iff_const_one goes further and proves the converse: among positive paths, the only solution is the constant path at 1. This is a rigidity statement. It says the variational principle has exactly one critical point in the positive domain, and that point is the ground state, the configuration where the cost is minimized.

In Recognition Science, this result carries a specific interpretation. The framework models reality as a ledger, a discrete record of recognition events, and the cost function J measures the price of each recognition. The theorem says that the least-action principle for the cost-rate action has a unique trajectory: the path that stays at the cost minimum forever. There is no other positive path with zero first-order cost change at every point. This is the cleanest possible form of a least-action principle: exactly one trajectory, and it is the trivial one.

The declaration does not claim that this constant path is dynamically interesting, nor that it describes any observed motion. It is a statement about a variational problem on a one-dimensional cost manifold, not a physical law. The theorem also does not address the Hessian-energy action E[γ] = ∫ ½ J''(γ(t)) γ'(t)² dt, whose Euler-Lagrange equation is the geodesic equation of the metric g(x) = 1/x³. That separate result, recorded in the same module, shows the constant path is trivially a geodesic (zero velocity, zero acceleration), but the geodesic family with nontrivial motion, γ(t) = (at + b)⁻², is a different object. The cost-rate result concerns only the potential-like action, not the kinetic-like one.

What the declaration establishes, in short, is a uniqueness theorem for a specific variational problem. It proves that the cost-rate action has exactly one critical point among positive paths, and that point is the constant path at the cost minimum. The value of the result is not in the motion it describes, which is none, but in the rigidity it demonstrates: the variational principle does not admit a family of solutions, only a single ground state.

/-- **Cost-rate EL theorem.** The constant path `γ ≡ 1` satisfies the
    cost-rate Euler–Lagrange equation, since `J'(1) = 0`. -/
theorem costRateEL_const_one : costRateELHolds (fun _ => 1) := by
  intro t
  -- J'(x) = (1 - x⁻²)/2 (from Cost.Convexity.JcostDeriv)
  -- At x = 1: J'(1) = (1 - 1)/2 = 0
  have h := IndisputableMonolith.Cost.deriv_Jcost (x := 1) one_pos
  rw [h]
  unfold IndisputableMonolith.Cost.JcostDeriv
  norm_num

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

What this page does not claim

The declaration does not claim the constant path describes any observed physical motion. It does not address the Hessian-energy action or its nontrivial geodesic solutions. It does not claim the cost-rate variational principle is the only action principle in the framework.

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: