Horizontal orbits under local first integrals have empty interior

Use the local first integrals in the Statement. Write $\omega ={\sum }_{j=1}^{n+1}{\omega }_{j}d{x}_j$ in the fixed Euclidean coordinates and set $w=({\omega }_1,\dots ,{\omega }_{n+1})$ and $Z_j=e_j-({\omega }_j\mathrm{/}\mathrm{\mid }w{\mathrm{\mid }}^2)w$. These globally defined $C^2$ vector fields are horizontal and span $\ker \omega$ at each point, since their matrix is the orthogonal projection onto that kernel. On every neighborhood supplied by the hypothesis, $dS=\mu \omega$ has nonzero derivative, and each $Z_j$-flow preserves $S$ as long as its trajectory remains there, by [F3]. Its derivative therefore preserves horizontal tangent vectors there: differentiating $S({\varphi }_j^t(x))=S(x)$ gives $d{S}_{{\varphi }_j^t(x)}D{\varphi }_j^t(x)v=d{S}_{x}v=0$ for horizontal $v$. The compact image of any finite flow trajectory has a finite subcover by such neighborhoods; a sufficiently fine finite subdivision of its compact time interval puts each subtrajectory in one of them. This follows directly from compactness: otherwise shrinking subintervals failing the subdivision would have a limiting time whose neighborhood contains them. Composing the local derivative identities obtains preservation over the full duration. Local flow uniqueness makes these continuations consistent, and [F2] gives $C^2$ dependence on durations and initial points wherever the finite composition is defined.

Fix $q\in U$ and a neighborhood $W$ with $dS=\mu \omega$ as in the hypothesis. Since $d{S}_q=\mu (q){\omega }_q\mathrm{\ne }0$, apply [L1] to $x\mapsto S(x)-S(q)$ with ambient dimension $n+1$ and target dimension $1$; after choosing the solved coordinate, its zero set is a local $C^1$ graph plaque $P$ through $q$, parameterized by its $n$ free coordinates. Let $\pi$ be projection to those free coordinates. Choose $n$ of the fields $Z_j$ that form a basis of $\ker {\omega }_q=\ker d{S}_q$, and for $s=(s_1,\dots ,s_n)$ near $0$ let $E(s)$ be the endpoint at $q$ of the successive local flows of these fields for durations $s_1,\dots ,s_n$. Shrink the open duration domain $D\subseteq {\mathbb{R}}^n$ so all flow segments stay in $W$. Step 1.1 shows that each flow preserves $S$, so $E(D)\subseteq P$; moreover $DE(0)$ has the chosen basis as its columns. The differential $D(\pi \circ E)(0)$ is therefore an invertible $n\times n$ matrix, because $D{\pi }_q$ is an isomorphism from the tangent space of the graph plaque to its free-coordinate space. Choose an open neighborhood $Y\subseteq {\mathbb{R}}^n$ of $y_0=\pi (q)$ and shrink $D$ so that the target-augmented map $H:D\times Y\to {\mathbb{R}}^n$, $H(s,y):=\pi (E(s))-y$, is defined. It satisfies $H(0,y_0)=0$ and its solved block $D_{s}H(0,y_0)=D(\pi \circ E)(0)$ is invertible. Apply [L1] with ambient dimension $2n$ and target dimension $n<2n$, permuting inputs to $(y,s)$ so $y$ is free and $s$ is solved. For every $y$ near $y_0$ this gives $s(y)$ with $\pi (E(s(y)))=y$; uniqueness of the graph plaque then says the endpoints $E(s(y))$ fill a relative neighborhood of $q$ in $P$. Each is reachable by a finite word of horizontal flows inside $W$. Conversely, a horizontal path preserves the local $S$ on each short subarc in a first-integral neighborhood by [F3]. Thus near each parameter value its image lies in the relative plaque neighborhood just shown to be reachable by such a finite word. The finite-word orbits are equivalence classes by flow reversal and concatenation, so their preimages along the path are relatively open in its interval domain. By [F4], connectedness of that interval forces one class. Hence every point horizontally reachable from $q$ lies in its finite-word orbit; the reverse inclusion follows because every word is a horizontal concatenation.

For a fixed finite word $\alpha$ of length $m\ge 1$, write $F_{\alpha }:O_{\alpha }\subseteq {\mathbb{R}}^m\to U$ for its endpoint map from $q$, on the open set of admissible duration tuples. Each duration derivative is a field vector transported by the later flows and is horizontal by step 1.1. Near any $s\in O_{\alpha }$, continuity puts the endpoint image in a neighborhood with the first integral $S$ from the hypothesis; hence $D(S\circ F_{\alpha })=0$. On a small convex parameter ball, [F3] makes $S\circ F_{\alpha }$ constant. Coordinatewise density in [F5] supplies a closed box with rational endpoints containing $s$ in its interior and contained in that ball. Its image under $F_{\alpha }$ is compact by [F6], lies in one level of $S$, and has empty interior in $U$: a nonempty open subset of that image would make $S$ constant on an open set, contradicting $dS=\mu \omega \mathrm{\ne }0$. Thus the image is a closed nowhere-dense subset of $U$. Enumerate the finite-word/rational-box pairs by the finite-level coding in [F5]; for an admissible box whose compact image has empty interior record that image, and otherwise record the empty set. Include the singleton $\{q\}$ for the empty word. This sequence $(K_j)$ of closed nowhere-dense sets covers $\mathcal{O}(q)$, since every duration tuple admits the small box just constructed. No countable atlas or choice of first integrals is needed for the enumeration.

Let $V$ be any nonempty open subset of $U$. By [F5], choose an initial rational open ball $B_{-1}$ with $\overline{B_{-1}}\subset V$. Recursively, for each $j\ge 0$, choose the first rational ball $B_j=B(c_j,r_j)$ in the fixed enumeration such that $\overline{B_j}\subset B_{j-1}\setminus K_j$ and $0<r_j<2^{-j}$. Such a ball exists: $K_j$ is closed with empty interior, so $B_{j-1}\setminus K_j$ is a nonempty open set, which contains a rational ball with closed ball inside it and arbitrarily small radius by [F5]. For $k>j$, the later centers lie in $B_j$, so $\mathrm{\mid }{c}_k-c_j\mathrm{\mid }<r_j<2^{-j}$; hence $(c_j)$ is Cauchy. By [F7] it has a limit $p$, and each tail of the sequence lies in the closed ball $\overline{B_j}$, so $p\in \overline{B_j}$ for every $j$. These closed balls lie in $V$ and satisfy $\overline{B_j}\cap K_j=\mathrm{\varnothing }$, so $p\in V\setminus {\bigcup }_j{K}_j$. Each selection is the least natural-number index satisfying explicit conditions, so it uses no choice axiom. Since the $K_j$ cover $\mathcal{O}(q)$, step 2.1 shows $p$ is not horizontally reachable from $q$ even by a path in $U$, and therefore not by one in $V$. This proves the asserted conclusion for every nonempty open $V$, using no global first integral or choice axiom.