Action Euler Lagrange Cost Rate El Implies Const One

The cost-rate theorem

The calculus of variations asks which path through a space makes a given integral smallest. The classical Euler–Lagrange equation is the standard tool: it turns that question into a differential equation the optimal path must satisfy. For the simplest possible integral, one that adds up a function of position alone, the equation collapses to a single condition: the derivative of that function must vanish at every point of the path.

In Recognition Science, the cost function, the price the framework assigns to each recognition event, has a unique forced form. Its derivative is zero only at the value 1, the point of lowest cost. The machine-checked theorem costRateEL_implies_const_one combines these two facts. It states: if a path stays positive and satisfies the Euler–Lagrange equation for the cost-rate action, then the path equals 1 at every moment. The only stationary path is the constant path at the cost minimum.

The theorem is a rigidity statement. Among all positive paths, the cost-rate action has exactly one critical point, and that point is the ground state. The framework's library proves the stronger equivalence: a positive path satisfies the cost-rate Euler–Lagrange equation if and only if it is constantly 1. This is the cleanest possible least-action principle: one trajectory, the one that never leaves the minimum.

The theorem does not claim that every minimizing path must be constant. The action integral has no boundary conditions, and any path that stays at 1 minimizes it, but the theorem concerns critical points, not global minima. It also does not cover the Hessian-energy action, a separate functional whose Euler–Lagrange equation is the geodesic equation of the metric g(x) = 1/x³. That equation has nonconstant solutions, such as the family γ(t) = (at + b)⁻². The cost-rate theorem applies only to its own action, not to the geodesic one.

What the theorem changes is the picture of the cost manifold: the point of lowest cost is not just a number but an attractor for the variational principle. Any path that feels no first-order cost change must sit there forever. The framework's library records this result with zero unresolved proofs and zero extra axioms.

/-- **Converse: paths satisfying the cost-rate EL with positivity are
    constantly at `1`.**

    This is the rigidity statement: the only critical points of the
    cost-rate action among admissible paths are constants at the cost
    minimum. -/
theorem costRateEL_implies_const_one (γ : ℝ → ℝ) (hpos : ∀ t, 0 < γ t)
    (hEL : costRateELHolds γ) : ∀ t, γ t = 1 := by
  intro t
  -- J'(x) = (1 - x⁻²)/2 = 0 ↔ x⁻² = 1 ↔ x² = 1 ↔ (since x > 0) x = 1.
  have hd := hEL t
  have hpost : 0 < γ t := hpos t
  have hd' := IndisputableMonolith.Cost.deriv_Jcost hpost
  rw [hd'] at hd
  unfold IndisputableMonolith.Cost.JcostDeriv at hd
  -- (1 - (γ t)⁻²)/2 = 0 → (γ t)⁻² = 1
  have h1 : 1 - (γ t) ^ (-2 : ℤ) = 0 := by linarith
  have h2 : (γ t) ^ (-2 : ℤ) = 1 := by linarith
  -- (γ t)⁻² = 1 → γ t = 1 (since γ t > 0)
  have hne : γ t ≠ 0 := ne_of_gt hpost
  have h3 : (γ t) ^ (2 : ℤ) = 1 := by
    have hinv : (γ t) ^ (-2 : ℤ) = ((γ t) ^ (2 : ℤ))⁻¹ := by
      rw [zpow_neg]
    rw [hinv] at h2
    have hpow_pos : 0 < (γ t) ^ (2 : ℤ) := by positivity
    have hpow_ne : (γ t) ^ (2 : ℤ) ≠ 0 := ne_of_gt hpow_pos
    field_simp at h2
    exact h2.symm
  have h4 : (γ t) ^ 2 = 1 := by
    have : (γ t) ^ (2 : ℤ) = (γ t) ^ (2 : ℕ) := by norm_cast
    rw [this] at h3
    exact_mod_cast h3
  -- γ t > 0 and (γ t)² = 1 → γ t = 1
  -- (γ t - 1)(γ t + 1) = γ t² - 1 = 0 → γ t = 1 (since γ t > 0)
  have h6 : (γ t - 1) * (γ t + 1) = 0 := by
    have : (γ t - 1) * (γ t + 1) = (γ t) ^ 2 - 1 := by ring
    rw [this, h4]; ring
  have hsum_pos : 0 < γ t + 1 := by linarith
  have hsum_ne : γ t + 1 ≠ 0 := ne_of_gt hsum_pos
  have h7 : γ t - 1 = 0 := by
    rcases mul_eq_zero.mp h6 with h | h
    · exact h
    · exact absurd h hsum_ne
  linarith

/-- **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 for the Hessian metric.

    A path `γ` satisfies `γ̈ + Γ(γ) γ̇² = 0`, where `Γ` is the
    Christoffel symbol of `g(x) = 1/x³`. -/
def geodesicEquationHolds (γ : ℝ → ℝ) : Prop :=
  ∀ t : ℝ, deriv (deriv γ) t + christoffel (γ t) * (deriv γ t) ^ 2 = 0

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 theorem does not claim that every minimizing path is constant; it concerns critical points, not global minima. The theorem does not cover the Hessian-energy action, whose geodesic equation has nonconstant solutions. The theorem does not derive the form of the cost function itself; it assumes the forced cost J and studies its variational consequences.

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: