182 intro t 183 have h_deriv : deriv (fun _ : ℝ => (1 : ℝ)) = fun _ => 0 := by 184 funext s; exact deriv_const s 1 185 have h_deriv2 : deriv (deriv (fun _ : ℝ => (1 : ℝ))) t = 0 := by 186 rw [h_deriv]; exact deriv_const t 0 187 rw [h_deriv2, h_deriv] 188 ring 189 190/-- **Headline equivalence (1D, ground state).** Among admissible paths, 191 the cost-rate EL has the constant-1 path as its unique solution 192 (`costRateEL_iff_const_one`), and the constant-1 path is a geodesic 193 of the Hessian metric (`const_one_is_geodesic`). 194 195 Therefore the cost-rate variational principle (find a path with 196 zero pointwise cost gradient) and the Hessian-energy variational 197 principle (find a geodesic) **agree on the unique ground state**: 198 the constant path at the cost minimum. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.