costRateELHolds
plain-language theorem explainer
This definition encodes the stationarity condition for the cost-rate action functional S[γ] = ∫ J(γ(t)) dt on paths γ : ℝ → ℝ. Researchers formalizing variational principles in Recognition Science cite it when proving that only the constant ground state minimizes the action. The definition directly transcribes the reduced Euler-Lagrange equation obtained when the Lagrangian depends solely on configuration, requiring the derivative of J to vanish at every point along the path.
Claim. A path γ : ℝ → ℝ satisfies the cost-rate Euler-Lagrange equation when dJ(γ(t))/dt = 0 for every real t, where J denotes the cost function induced by the multiplicative recognizer.
background
The cost-rate action is the time integral of the pointwise cost J(γ(t)). Because the Lagrangian L(q, q̇) = J(q) is independent of velocity, the Euler-Lagrange equation reduces exactly to ∂L/∂q = J'(γ(t)) = 0. The module places this alongside the Hessian-energy action E[γ] = ∫ (1/2) J''(γ(t)) γ̇(t)² dt whose geodesics obey a second-order equation in the metric g(x) = J''(x) = 1/x³.
proof idea
This is a one-line definition that directly states the pointwise derivative condition on the cost function. It serves as the interface used by sibling theorems to verify that the constant path at 1 satisfies the equation and to prove uniqueness under positivity.
why it matters
The definition anchors the cost-rate variational principle in the Recognition Science framework. It is invoked by costRateEL_const_one, costRateEL_iff_const_one, and ground_state_is_unique_critical_point, which together show that the constant path at unity is the unique critical point and agrees with the geodesic condition of the Hessian metric. It implements the Euler-Lagrange reduction described in the paper companion RS_Least_Action.tex and connects to T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.