theorem proved term proof

`ground_state_is_unique_critical_point`

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

formal statement (Lean)

 199theorem ground_state_is_unique_critical_point :
 200    costRateELHolds (fun _ : ℝ => 1) ∧ geodesicEquationHolds (fun _ : ℝ => 1) :=

Term-mode proof.

 201  ⟨costRateEL_const_one, const_one_is_geodesic⟩
 202
 203/-! ## Status report -/
 204

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.