christoffel
plain-language theorem explainer
The declaration defines the Christoffel symbol Γ(x) = -3/(2x) for the one-dimensional Hessian metric g(x) = 1/x³ that arises as the second derivative of the J-cost. Researchers working on variational principles in Recognition Science cite it when writing the geodesic equation for the Hessian-energy action E[γ]. The definition is obtained by direct substitution of g and g' into the standard one-dimensional formula Γ = (1/(2g)) g'.
Claim. For the metric $g(x) = x^{-3}$, the Christoffel symbol is given by the formula $Γ(x) = -3/(2x)$.
background
The Euler–Lagrange module formalizes two action functionals on the cost manifold. The Hessian-energy action is $E[γ] = ∫ ½ g(γ(t)) γ̇(t)² dt$ with metric $g(x) = J''(x) = 1/x³$. In one dimension the geodesic equation of this metric takes the form γ̈ + Γ(γ) γ̇² = 0, where Γ is the Christoffel symbol derived from g. The module imports PathSpace, FunctionalConvexity, Cost and Convexity; upstream structures calibrate the J-functional whose second derivative supplies the metric.
proof idea
The definition is a direct algebraic substitution. With $g(x) = x^{-3}$ one computes $g'(x) = -3x^{-4}$. The one-dimensional formula then yields Γ(x) = (1/2) x³ (-3 x^{-4}) = -3/(2x). No external lemmas are required beyond elementary differentiation and arithmetic.
why it matters
The definition supplies the explicit connection coefficient used by geodesicEquationHolds and geodesic_iff_hessianEnergy_EL. It completes the identification of the Euler–Lagrange equation of the Hessian-energy action with the geodesic equation on the cost manifold, as stated in the paper companion RS_Least_Action.tex. The construction is consistent with the Recognition Science forcing chain that derives dynamics from the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.