Level slices of connecting gradient trajectories

A negative-gradient trajectory joining distinct limiting points crosses every intermediate value of the defining function exactly once. Thus an intermediate level provides a canonical time origin for each parametrized connecting trajectory, a useful slice when forming Morse trajectory spaces modulo time translation.

The argument needs differentiability along the orbit and continuity of the defining function at the limiting endpoints. It does not require global regularity of the gradient: a hypothetical plateau would force a stationary interval, and hence a periodic orbit, which is impossible for a nonconstant negative-gradient trajectory.

The level-slice construction follows the trajectory-space viewpoint of Audin--Damian, Morse Theory and Floer Homology, Chapter 2.

theorem Flow.IsNegativeGradient.orbit_strictAnti_of_nonconstant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {x : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hnonconst : ∃ (t : ℝ), φ.toFun t x ≠ x) : StrictAnti fun (t : ℝ) => f (φ.toFun t x)

On a nonconstant negative-gradient orbit, the defining function strictly decreases with time.

theorem Flow.IsNegativeGradient.orbit_strictAnti_of_mem_unstableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q x : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hpq : p ≠ q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : StrictAnti fun (t : ℝ) => f (φ.toFun t x)

On a connecting orbit with distinct endpoints, the defining function strictly decreases with time. In particular no two times on that orbit have the same value.

theorem Flow.IsNegativeGradient.existsUnique_time_value_of_mem_unstableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q x : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hfp : ContinuousAt f p) (hfq : ContinuousAt f q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) {c : ℝ} (hc : f q < c ∧ c < f p) : ∃! t : ℝ, f (φ.toFun t x) = c

A connecting negative-gradient trajectory crosses each value strictly between its limiting endpoint values at exactly one time. The unique time gives a canonical representative of its time-translation orbit on that level.