const_one_is_geodesic
plain-language theorem explainer
The constant path γ(t) ≡ 1 satisfies the geodesic equation of the Hessian metric g(x) = 1/x³ on the cost manifold. Researchers formalizing variational principles in Recognition Science cite this to equate the cost-rate minimum with a geodesic of the induced energy functional. The tactic proof computes the first and second derivatives of the constant function as zero, substitutes into the geodesic equation, and simplifies algebraically.
Claim. The constant path $γ(t) ≡ 1$ satisfies $ÿ(t) + Γ(γ(t)) ẏ(t)² = 0$ for all $t ∈ ℝ$, where $Γ(x) = -3/(2x)$ is the Christoffel symbol of the metric $g(x) = J''(x) = 1/x³$.
background
The Euler–Lagrange module treats two functionals on the cost manifold. The cost-rate action integrates the J-cost pointwise, reducing its EL equation to J'(γ(t)) = 0 whose unique solution is the constant ground state at the J minimum. The Hessian-energy action integrates ½ J''(γ) ẏ², yielding the geodesic equation of the metric g(x) = 1/x³ whose Christoffel symbol is Γ(x) = -3/(2x).
proof idea
Tactic-mode proof. Introduce t, prove the first derivative of the constant-1 function is identically zero via deriv_const, deduce the second derivative is likewise zero, rewrite the geodesic equation with these facts, and finish with ring.
why it matters
Feeds directly into ground_state_is_unique_critical_point, which packages the cost-rate EL holding for the constant path together with this geodesic verification. The module doc-comment states that the two variational principles therefore agree on the unique ground state. This step closes the 1D equivalence between cost-rate and Hessian-energy formulations inside the Recognition least-action setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.