geodesic_iff_hessianEnergy_EL
plain-language theorem explainer
Researchers working on the variational formulation of Recognition Science cite this equivalence to identify critical paths of the Hessian-energy action with geodesics of the induced metric g(x) = x^{-3}. The statement equates the predicate that a path γ obeys γ̈ + Γ(γ) γ̇² = 0 to the explicit Euler-Lagrange form derived from E[γ] = ∫ ½ g(γ) γ̇² dt. The proof is the one-line term Iff.rfl because the two sides coincide by definition of the geodesic predicate.
Claim. For a path γ : ℝ → ℝ, γ satisfies the geodesic equation ∀ t, d²γ/dt²(t) + Γ(γ(t)) (dγ/dt(t))² = 0 with Christoffel symbol Γ(x) = -3/(2x) of the metric g(x) = x^{-3} if and only if the same equation holds, which is the Euler-Lagrange equation of the energy functional E[γ] = ∫ ½ g(γ(t)) (dγ/dt(t))² dt.
background
The module distinguishes two action functionals on paths in the cost manifold. The cost-rate action integrates the pointwise J-cost, reducing its EL equation to the constant ground state γ ≡ 1. The Hessian-energy action integrates ½ J''(γ(t)) γ̇(t)² dt where J''(x) = 1/x³, yielding the metric g(x) = x^{-3} whose Christoffel symbol is defined as Γ(x) = -3/(2x) in the sibling declaration christoffel. The predicate geodesicEquationHolds γ is the universal quantification of γ̈ + Γ(γ) γ̇² = 0 at every t, as introduced in the upstream definition of that predicate.
proof idea
The proof is the one-line term Iff.rfl. This suffices because the right-hand side of the biconditional is literally the body of the definition of geodesicEquationHolds γ, which expands directly to the displayed forall expression involving deriv and christoffel.
why it matters
This declaration records the standard identification of the geodesic equation with the EL equation of the Hessian-energy action, as described in the paper companion RS_Least_Action.tex section on the Euler-Lagrange equation as the geodesic equation. It bridges the energy functional to the geometry of the cost manifold, supporting the uniqueness of the ground state and the connection between cost-rate and energy formulations in the Recognition Science framework. No downstream uses appear in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.