costRateEL_const_one
plain-language theorem explainer
The constant path γ(t) ≡ 1 satisfies the cost-rate Euler-Lagrange equation because J'(1) = 0. Researchers formalizing variational principles in Recognition Science cite this to identify the ground state as the unique minimizer of the integrated J-cost. The proof is a direct one-line evaluation that invokes the explicit derivative lemma at x = 1 and reduces the expression to zero by normalization.
Claim. The constant path γ(t) = 1 satisfies ∀ t, deriv J(γ(t)) = 0, where J is the cost function whose first derivative is given by J'(x) = (1 - x^{-2})/2.
background
The module formalizes Euler-Lagrange equations on the cost manifold for two action functionals. The cost-rate action is S[γ] = ∫ J(γ(t)) dt; because the Lagrangian depends only on position and not velocity, the EL equation collapses to J'(γ(t)) = 0 for all t. The cost function J is the derived cost induced by a multiplicative recognizer, with explicit derivative JcostDeriv(x) = (1 - x^{-2})/2 supplied by the Convexity module. The upstream definition costRateELHolds states precisely that a path satisfies the equation when deriv Jcost (γ t) = 0 holds at every real t.
proof idea
The term proof applies the lemma deriv_Jcost at argument 1 (using the positivity hypothesis one_pos), rewrites the result to the definition JcostDeriv, and finishes with norm_num to obtain the numerical identity 0 = 0.
why it matters
This theorem supplies the cost-rate half of the headline equivalence ground_state_is_unique_critical_point, which asserts that the constant-1 path is both an EL solution for the integrated cost and a geodesic of the Hessian metric. It therefore closes the variational-principle agreement on the ground state inside the Euler-Lagrange module and corresponds to the cost-rate case treated in papers/RS_Least_Action.tex. The result rests on J-uniqueness (T5) and the fact that the minimum of J occurs at the self-similar fixed point 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.