ground_state_is_unique_critical_point
plain-language theorem explainer
The constant path at value 1 satisfies both the cost-rate Euler-Lagrange condition that the derivative of the J-cost vanishes pointwise and the geodesic equation in the Hessian metric g(x) = J''(x). Researchers on variational principles within Recognition Science cite this to show the two action functionals agree exactly on the ground state. The proof is a one-line term that conjoins the separate verifications for each equation.
Claim. The constant path $γ(t) ≡ 1$ satisfies $∀ t, (d/dt) J(γ(t)) = 0$ and the geodesic equation $∀ t, γ̈(t) + Γ(γ(t)) γ̇(t)^2 = 0$, where Γ is the Christoffel symbol of the Hessian metric $g(x) = J''(x)$.
background
The module derives Euler-Lagrange equations for two functionals on the cost manifold. The cost-rate action is $S[γ] = ∫ J(γ(t)) dt$, whose EL equation reduces to $J'(γ(t)) = 0$ because the Lagrangian is independent of velocity. The Hessian-energy action is $E[γ] = ∫ ½ J''(γ(t)) γ̇(t)^2 dt$, whose EL equation is the geodesic equation in the metric $g(x) = J''(x) = x^{-3}$ with Christoffel symbol Γ(x) = -3/(2x). costRateELHolds γ is the predicate ∀ t, deriv Jcost (γ t) = 0. geodesicEquationHolds γ is the predicate ∀ t, deriv (deriv γ) t + christoffel (γ t) * (deriv γ t)^2 = 0. The constant path at 1 is the ground state because J'(1) = 0.
proof idea
The proof is the term ⟨costRateEL_const_one, const_one_is_geodesic⟩. It directly assembles two upstream results: costRateEL_const_one verifies that J'(1) = 0 so the constant path meets the cost-rate EL, while const_one_is_geodesic confirms the geodesic equation by explicit computation that both first and second derivatives vanish.
why it matters
This theorem records the headline equivalence that the cost-rate variational principle and the Hessian-energy variational principle coincide on the unique ground state. It is referenced by the downstream definition eulerLagrange_status to summarize the agreement. The result fills the 1D ground-state case in the Euler-Lagrange derivation of the companion paper and confirms that the J-cost minimum is also a geodesic of the induced metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.