geodesicEquationHolds
plain-language theorem explainer
The declaration defines the condition that a path γ satisfies the geodesic equation γ̈ + Γ(γ) γ̇² = 0 for the Hessian metric g(x) = 1/x³. Researchers in variational calculus within Recognition Science cite it to link the energy functional to geodesic motion in one dimension. It is introduced as a direct definition that matches the standard form of the Euler-Lagrange equation for the Hessian-energy action.
Claim. A curve γ:ℝ→ℝ obeys the geodesic equation when d²γ/dt²(t) + Γ(γ(t)) (dγ/dt(t))² = 0 holds for every real t, with the Christoffel symbol Γ(x) = -3/(2x) of the metric g(x) = 1/x³.
background
The module formalizes Euler-Lagrange equations for the J-action on the cost manifold. The cost-rate action integrates J(γ(t)) while the Hessian-energy action integrates (1/2) J''(γ(t)) (γ'(t))², yielding the metric g(x) = 1/x³. The Christoffel symbol is defined as christoffel(x) = -3/(2x) from the standard 1D formula Γ = (1/(2g)) g'. This rests on the Recognition Science J-cost and the phi-ladder structure from upstream modules such as PhiForcingDerived.
proof idea
The declaration is a direct definition of the Prop that encodes the geodesic equation using the pre-defined christoffel function. It is applied verbatim in the equivalence geodesic_iff_hessianEnergy_EL and in the proof that the constant path at 1 is a geodesic.
why it matters
It supplies the mathematical object used to prove that the cost-rate and Hessian-energy principles agree on the unique ground state at γ = 1, as recorded in ground_state_is_unique_critical_point and eulerLagrange_status. This completes the identification of the Euler-Lagrange equation with the geodesic equation in the Recognition Science least-action framework, consistent with the eight-tick octave and D=3 emergence from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.