hessianMetric_eq
plain-language theorem explainer
The lemma establishes that the Hessian metric induced by the second derivative of the J-cost equals one over x cubed for positive real x. Researchers deriving the geodesic equation for the Hessian-energy action on the cost manifold would cite this identity to obtain the explicit Christoffel symbol. The proof is a direct term-mode reduction that unfolds the metric definition and rewrites the negative integer power.
Claim. For every real number $x > 0$, the Hessian metric $g(x) := J''(x)$ satisfies $g(x) = 1/x^3$.
background
The module formalizes Euler-Lagrange equations for two action functionals on the cost manifold. The cost-rate action integrates the pointwise J-cost, while the Hessian-energy action integrates half J'' times squared velocity and induces the Riemannian metric g(x) = J''(x). Upstream, hessianMetric is defined as the noncomputable map sending x to x raised to the negative third integer power, with the explicit form g(x) = 1/x^3 stated in its doc-comment as the natural metric induced by the second derivative of Jcost.
proof idea
The proof is a term-mode reduction. It unfolds the definition of hessianMetric and rewrites using the rules for negative integer powers, natural-number powers, and division to reach the explicit reciprocal form.
why it matters
This identity supplies the concrete metric for the Hessian-energy action whose Euler-Lagrange equation is the geodesic equation of the cost manifold. It supports sibling derivations of the Christoffel symbol and geodesic flow. In the Recognition framework it realizes the explicit kinetic term in the least-action principle, consistent with the eight-tick octave and the phi-ladder structure of J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.