hessianMetric
plain-language theorem explainer
hessianMetric defines the Hessian metric g(x) := x^{-3} on the positive reals as the second derivative of the J-cost. Researchers deriving the geodesic equation for the Hessian-energy action E[γ] cite it when reducing the Euler-Lagrange equation to Christoffel form. The definition is a direct noncomputable power expression with no lemmas applied inside it.
Claim. The Hessian metric on the positive ray is the function $g(x) = x^{-3}$, which equals the second derivative of the J-cost function.
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 the constant ground state at 1. The Hessian-energy action integrates half the product of J''(γ(t)) and γ̇(t)², so the metric g(x) = J''(x) supplies the kinetic term. The module states that g(x) evaluates to 1/x³ and induces the geodesic equation with Christoffel symbol Γ(x) = -3/(2x). Upstream, Jcost is taken from the Cost module and satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
The definition is a direct noncomputable abbreviation that sets hessianMetric x to the integer power x^(-3). No lemmas are invoked inside the definition body. The immediate downstream lemma hessianMetric_eq rewrites the power to the fractional form 1/x³ under the hypothesis 0 < x.
why it matters
This definition supplies the metric tensor for the Hessian-energy action whose EL equation is the geodesic equation. It is used by hessianMetric_eq and then by christoffel and geodesicEquationHolds. The construction appears in the paper companion RS_Least_Action.tex in the section on the Euler-Lagrange equation as the geodesic equation, linking J-uniqueness to the spatial dimension D = 3 via the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.