costRateEL_iff_const_one
plain-language theorem explainer
The equivalence shows that the cost-rate Euler-Lagrange condition holds for a positive path precisely when the path is constantly 1. Analysts of variational principles in Recognition Science cite this uniqueness result to locate the ground-state trajectory. The proof splits into the rigidity implication from the EL condition and the direct verification that the derivative vanishes at 1.
Claim. Let $γ : ℝ → ℝ$ be positive. The condition that the derivative of the cost function $J$ vanishes at $γ(t)$ for every $t$ holds if and only if $γ(t) = 1$ for all $t$, where $J'(x) = (1 - x^{-2})/2$.
background
The cost-rate action is the integral of the pointwise cost $J(γ(t))$ over time. Because the Lagrangian depends only on position, the Euler-Lagrange equation reduces to the pointwise stationarity requirement that the derivative of $J$ vanishes along the path. This stationarity predicate is the content of the upstream definition that encodes $∀ t, (d/dx)J(γ(t)) = 0$ and is quoted as reducing to $J'(q) = 0$ since the Lagrangian carries no velocity dependence.
proof idea
The proof builds the biconditional via constructor. One direction applies the upstream implication theorem that the Euler-Lagrange condition plus positivity forces constancy at 1. The converse assumes the constant value 1, invokes the derivative lemma that equates the derivative of $J$ to its explicit form, substitutes the argument 1 into that form, and reduces the resulting arithmetic expression to zero.
why it matters
This equivalence pins down the unique solution of the cost-rate variational principle and supplies the key step for the headline statement that the cost-rate and Hessian-energy principles coincide on the constant-1 ground state. It implements the principle of least action by exhibiting the constant path at the $J$ minimum as the sole trajectory with vanishing first variation. The result aligns with $J$-uniqueness in the forcing chain and appears in the companion paper section on the Euler-Lagrange equation as the geodesic equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.