Regular first-class constraints admit local symplectic reduction

For $w\in T_{z}N$, [F1] gives $d{\chi }_a(w)=0$, hence $\omega (X_{{\chi }_a},w)=0$ and each $X_{{\chi }_a}\in (T_{z}N{)}^{\omega }$. The $d{\chi }_a$ are independent, so their images under the isomorphism ${\omega }^{\mathrm{♭}}$ are independent; therefore these $r$ vectors are independent. The level has codimension $r$, and [F4] gives $\dim (T_{z}N{)}^{\omega }=r$, so they span the symplectic orthogonal.

On $N$, $d{\chi }_b(X_{{\chi }_a})=\{{\chi }_b,{\chi }_a\}=0$ by first-classness and [F7], so each $X_{{\chi }_a}$ is tangent. Their independence from step 1.1 implies $r\le \dim N=2n-r$, hence $r\le n$. The radical of the restricted form is $T_{z}N\cap (T_{z}N{)}^{\omega }$; since the orthogonal is already spanned by tangent $X_{{\chi }_a}$, this intersection is exactly that span.

For smooth kernel fields $U,V$ and any tangent field $W$, apply $d{\omega }_N=0$ to $(U,V,W)$. All terms containing contractions with $U$ or $V$ vanish, leaving ${\omega }_N([U,V],W)=0$. Thus ([U,V]) is again in the kernel and the distribution is involutive.

The Frobenius frame proof solves a transverse linear matrix ODE to straighten a local frame. Its coefficients are smooth, so [F5] gives a smooth local solution in transverse coordinates; the initial matrix is identity, so its determinant remains nonzero after shrinking the coordinate neighborhood. The resulting frame is involutive and [F6] supplies local $(s,y)$ coordinates. This explicitly supplies the parameter dependence needed in that construction.

Since every ${\omega }_N$-kernel vector is tangent to the $s$-leaves, the contraction of ${\omega }_N$ with ${\mathrm{\partial }}_{s^a}$ vanishes. Therefore its coordinate expression has no $d{s}^a$ factor.

In the Frobenius chart, step 5.1 writes ${\omega }_N=\frac{1}{2}{\sum }_{i,j}{\omega }_{ij}(s,y)d{y}^i\wedge d{y}^j$. Since $d{\omega }_N=0$, the coefficient of each independent form $d{s}^a\wedge d{y}^i\wedge d{y}^j$ with $i<j$ is ${\mathrm{\partial }}_{s^a}{\omega }_{ij}=0$. If the $y$-space has dimension less than two, the displayed two-form is zero and is already independent of $s$. Thus the coefficients define a form ${\omega }_{\mathrm{r}\mathrm{e}\mathrm{d}}$ on the local $y$-space, and the coordinate projection pulls it back to ${\omega }_N$; the remaining $dy$-components of $d{\omega }_N=0$ show $d{\omega }_{\mathrm{r}\mathrm{e}\mathrm{d}}=0$. Its kernel would lift to a vector in $TN$ orthogonal to all of $TN$, hence to the already-quotiented kernel, so ${\omega }_{\mathrm{r}\mathrm{e}\mathrm{d}}$ is nondegenerate.