Connecting orbits and intermediate level sets

For a negative-gradient flow, every orbit connecting two distinct limiting points meets an intermediate level exactly once. Consequently the quotient map from connecting points to their time-translation orbits restricts to a bijection on that level. This identifies the underlying points of an unparametrized Morse trajectory space with a level slice, before any smooth structure or compactification is constructed.

The use of an intermediate level as a slice follows Audin--Damian, Morse Theory and Floer Homology, Chapter 2.

theorem Flow.IsNegativeGradient.bijOn_quotient_mk_unstableSet_inter_stableSet_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ x ∈ φ.unstableSet p ∩ φ.stableSet q, ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hfp : ContinuousAt f p) (hfq : ContinuousAt f q) {c : ℝ} (hc : f q < c ∧ c < f p) : Set.BijOn (fun (x : E) => Quotient.mk'' x) (φ.unstableSet p ∩ φ.stableSet q ∩ {x : E | f x = c}) {a : Quotient (AddAction.orbitRel ℝ E) | ∃ x ∈ φ.unstableSet p ∩ φ.stableSet q, Quotient.mk'' x = a}

The quotient map is bijective from an intermediate level of the connecting set onto the orbit classes containing connecting points.