lemma proved term proof

`hessianMetric_eq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 142@[simp] lemma hessianMetric_eq {x : ℝ} (_hx : 0 < x) :
 143    hessianMetric x = 1 / x ^ 3 := by

proof body

Term-mode proof.

 144  unfold hessianMetric
 145  rw [zpow_neg, zpow_ofNat, one_div]
 146
 147/-- The Christoffel symbol of the Hessian metric `g(x) = 1/x³`.
 148
 149    For a 1D metric, `Γ = (1/2g) (dg/dx) = (1/2) · x³ · (-3 x⁻⁴) = -3/(2x)`. -/

depends on (6)

Lean names referenced from this declaration's body.

hessianMetric in IndisputableMonolith.Action.EulerLagrange decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use