costRateEL_implies_const_one
plain-language theorem explainer
Any positive path satisfying the cost-rate Euler-Lagrange condition must be constantly equal to one. Researchers formalizing variational principles in Recognition Science cite this rigidity result to identify the unique critical point of the integrated J-cost. The proof substitutes the explicit derivative of Jcost, reduces the zero condition to an algebraic equation via linarith, and solves for equality to one using positivity and power inversion.
Claim. Let $γ:ℝ→ℝ$ satisfy $0<γ(t)$ for all $t$. If $J'(γ(t))=0$ for all $t$, then $γ(t)=1$ for all $t$.
background
The cost-rate action is $S[γ]=∫J(γ(t))dt$. Because the Lagrangian depends only on position, the Euler-Lagrange equation reduces to the pointwise condition $J'(γ(t))=0$. The definition costRateELHolds encodes exactly this requirement. The upstream lemma deriv_Jcost states that deriv Jcost x equals JcostDeriv x for positive x, where JcostDeriv x is defined as (1-x^{-2})/2.
proof idea
Fix arbitrary t. The EL hypothesis supplies deriv Jcost (γ t)=0. Apply deriv_Jcost (using positivity) to replace it by JcostDeriv (γ t). Unfold to obtain (1-(γ t)^{-2})/2=0. Linear arithmetic yields (γ t)^{-2}=1. Invert via zpow_neg and field_simp, cast the exponent, factor the difference of squares, and discard the extraneous root γ t=-1 by positivity, leaving γ t=1.
why it matters
This supplies the forward direction of costRateEL_iff_const_one, which asserts the full equivalence between the EL condition and constancy at one. It realizes the uniqueness half of the principle of least action for the cost-rate functional, as stated in the module documentation. In the Recognition framework it confirms that the only trajectory with vanishing first variation is the J-fixed point at the ground state, consistent with T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.