The unparametrized trajectory space is a smooth manifold

Put $P=\tilde{\mathcal{M}}(p,q)$. If $P=\mathrm{\varnothing }$, its orbit set $\mathcal{M}(p,q)$ is empty and has the empty smooth structure; no dimension is assigned by a negative formula. Assume henceforth that $P$ is nonempty. No point of a trajectory is critical: flow uniqueness would then make it constant, contradicting its distinct endpoint limits. In the transported immersion charts of [F3], the action $t\cdot \gamma =\gamma (\cdot +t)$ is smooth and evaluates to ${\mathrm{\Phi }}_t(\gamma (0))$. Its tangent vector $V$ on the fibre product evaluates to $X(\gamma (0))\mathrm{\ne }0$, so $V$ is nonzero. Hence the dimension of the nonempty smooth manifold $P$ is at least one. By [F1], this dimension is $\lambda (p)-\lambda (q)$; in particular an index difference at most zero forces $P$, and therefore its orbit set, to be empty.

In the nonempty case strict decrease and the endpoint limits imply $f(p)>f(q)$. Set $c=(f(p)+f(q))\mathrm{/}2$, without imposing any global regular-value condition on the ambient function $f$, and put $h=f\circ {\mathrm{ev}}_0:P\to \mathbb{R}$. This map is smooth by [F3]. For every $\gamma \in P$, the flow tangent vector of step 1.1 satisfies $d{h}_{\gamma }(V)=d{f}_{\gamma (0)}(X)<0$, so $h$ is a submersion. For each trajectory, continuity and its two endpoint limits give a finite time $t_0$ with $f(\gamma (t_0))=c$, and strict decrease makes $t_0$ unique. In particular $h^{-1}(c)$ is nonempty. Apply [F4] to $h$, whose scalar target has dimension one: this slice is an embedded codimension-one submanifold of $P$, of dimension $\lambda (p)-\lambda (q)-1\ge 0$.

Translating each trajectory by its unique time $t_0$ from step 2.1 gives exactly one representative in $h^{-1}(c)$. Conversely, two representatives in the same time orbit can both lie in that slice only if their translation is zero. This is the level-representative bijection, using only the continuity and strict-decrease part of [F2]. Put $S=h^{-1}(c)$. The same equation $h(t\cdot \gamma )=c$, now with $\gamma$ varying in a chart of the entire $P$, has nonzero time derivative at every solution. By [F5] its unique hitting time $\tau (\gamma )$ is smooth locally on $P$; uniqueness patches these local functions globally. It satisfies $\tau (s\cdot \gamma )=\tau (\gamma )-s$, so $r(\gamma )=\tau (\gamma )\cdot \gamma$ is a smooth orbit-invariant map $P\to S$ restricting to the identity on $S$. Let $q:P\to P\mathrm{/}\mathbb{R}$ carry the quotient topology [F6]. The induced inverse $\bar{r}:P\mathrm{/}\mathbb{R}\to S$ is continuous: for every open $U\subseteq S$, $q^{-1}({\bar{r}}^{-1}(U))=r^{-1}(U)$ is open, and [F6] applies. Conversely $q{\mathrm{\mid }}_S$ is continuous, and these two maps are inverses. Thus the slice bijection is a homeomorphism for the quotient topology. Transport its smooth structure to $\mathcal{M}(p,q)$; its underlying topology is precisely that quotient topology, and its dimension is the one in step 2.1. Any other $c^{\mathrm{\prime }}$ strictly between the endpoint values gives the same smooth structure: the equation $h(t\cdot \gamma )=c^{\mathrm{\prime }}$ has nonzero derivative in $t$, so [F5] makes the unique hitting time smooth locally on the first slice; uniqueness patches these local times, and the smooth flow action gives mutually inverse smooth change-of-slice maps. Thus the construction and the empty case prove the full statement without Sard's theorem, an ambient regular level, or an added choice hypothesis.