[proofplan]
The polarisation $E \subset TM$ is Lagrangian and involutive, so by the [Frobenius Theorem](/theorems/???) it integrates to a foliation, and by Lagrangianness $E = E^{\perp_\omega}$. The symplectic form $\omega$ gives a bundle isomorphism $\alpha : TM \to T^*M$; restricting target to $E^*$ yields a surjection $\beta : TM \to E^*$ whose kernel we compute to be exactly $E$. Using any local lift to transport covectors, we define $\nabla_X \xi := \beta([X, \tilde\xi])$ for $X \in \Gamma(E)$; involutivity of $E$ makes the lift choice irrelevant. The Jacobi identity for $[\cdot, \cdot]$ yields vanishing curvature, and a Cartan-formula computation exploiting Lagrangianness and $d\omega = 0$ yields vanishing torsion on each leaf.
[/proofplan]
[step:Build the bundle map $\beta : TM \to E^*$ and identify its kernel with $E$]
Define the musical isomorphism induced by $\omega$
\begin{align*}
\alpha : TM &\to T^*M \\
x_p &\mapsto \omega_p(x_p, \cdot).
\end{align*}
By the non-degeneracy of $\omega$, $\alpha$ is a bundle isomorphism. Composing with the pointwise restriction of covectors from $T_pM$ to $E_p$ gives the bundle map
\begin{align*}
\beta : TM &\to E^* \\
x_p &\mapsto \omega_p(x_p, \cdot)\big|_{E_p}.
\end{align*}
Since $\alpha$ is an isomorphism and restriction $T^*M \to E^*$ is fibrewise surjective (any functional on $E_p$ extends to $T_pM$), $\beta$ is surjective.
To identify $\ker \beta$, note $x_p \in \ker \beta_p$ iff $\omega_p(x_p, y) = 0$ for all $y \in E_p$, i.e.\ $x_p \in E_p^{\perp_\omega}$. Because $E$ is a [polarisation](/page/Polarisation), it is Lagrangian: $E_p = E_p^{\perp_\omega}$. Hence $\ker \beta = E$. By rank counting, $\mathrm{rk}(TM) = 2n$ and $\mathrm{rk}(E^*) = n$, so $\mathrm{rk}(\ker\beta) = n = \mathrm{rk}(E)$, consistent with $\ker \beta = E$.
[/step]
[step:Define $\nabla_X \xi$ via lift-and-bracket and check well-definedness]
Fix a local leaf $L \subset M$ of the foliation integrating $E$; on $L$ we have $TL = E|_L$. For $X \in \Gamma(E|_L)$ and $\xi \in \Omega^0(E^*|_L)$, choose any smooth lift $\tilde\xi \in \Gamma(TM|_L)$ with $\beta(\tilde\xi) = \xi$ (exists since $\beta$ is a surjection of vector bundles). Define
\begin{align*}
\nabla : \Gamma(E|_L) \times \Omega^0(E^*|_L) &\to \Omega^0(E^*|_L) \\
(X, \xi) &\mapsto \nabla_X \xi := \beta\bigl([X, \tilde\xi]\bigr).
\end{align*}
We verify this is independent of the lift. If $\tilde\xi'$ is another lift, then $\tilde\xi' - \tilde\xi \in \Gamma(\ker\beta|_L) = \Gamma(E|_L)$ by the previous step. Since $E$ is involutive by the polarisation axioms, $[X, \tilde\xi' - \tilde\xi] \in \Gamma(E|_L) = \Gamma(\ker\beta|_L)$ for $X \in \Gamma(E|_L)$. Therefore
\begin{align*}
\beta([X, \tilde\xi']) - \beta([X, \tilde\xi]) = \beta([X, \tilde\xi' - \tilde\xi]) = 0,
\end{align*}
so $\nabla_X \xi$ does not depend on the lift.
$\mathbb R$-linearity in $\xi$ and in $X$ is immediate from $\mathbb R$-bilinearity of the Lie bracket and $\mathbb R$-linearity of $\beta$. For the Leibniz rule in $\xi$, let $f \in C^\infty(L)$ and choose the lift $\widetilde{f\xi} := f\tilde\xi$:
\begin{align*}
\nabla_X(f\xi) &= \beta([X, f\tilde\xi]) = \beta\bigl(f[X, \tilde\xi] + (X\cdot f)\tilde\xi\bigr) \\
&= f\,\beta([X, \tilde\xi]) + (X\cdot f)\,\beta(\tilde\xi) = f\,\nabla_X\xi + (X\cdot f)\,\xi.
\end{align*}
For $C^\infty$-linearity in $X$, let $g \in C^\infty(L)$:
\begin{align*}
\nabla_{gX}\xi = \beta([gX, \tilde\xi]) = \beta\bigl(g[X, \tilde\xi] - (\tilde\xi \cdot g)X\bigr) = g\,\nabla_X\xi - (\tilde\xi \cdot g)\,\beta(X) = g\,\nabla_X\xi,
\end{align*}
since $X \in \Gamma(E|_L) = \Gamma(\ker\beta|_L)$ gives $\beta(X) = 0$. Thus $\nabla$ is an [affine connection](/page/Affine%20Connection) on the bundle $E^*|_L \to L$.
[guided]
The strategy is to exploit the fact that $E = \ker\beta$ to turn a map into $TM$ into a map into $E^*$ in a way that is insensitive to the ambiguity in lifting. The recipe is: lift $\xi$ to some $\tilde\xi \in \Gamma(TM)$, bracket with $X$, and project back with $\beta$.
Why is this well-defined? Two lifts $\tilde\xi, \tilde\xi'$ of the same $\xi$ differ by a section of $\ker\beta = E$, and bracketing $X \in \Gamma(E)$ with a section of $E$ lands inside $\Gamma(E) = \Gamma(\ker\beta)$ provided $E$ is involutive. Hence the $\beta$-projection erases the ambiguity. This is the whole point of the Lagrangian/involutive hypothesis: it makes the lift-and-bracket recipe robust.
For the Leibniz rule, the key computation is
\begin{align*}
[X, f\tilde\xi] = f[X, \tilde\xi] + (X\cdot f)\tilde\xi,
\end{align*}
a standard Lie bracket identity. Since $\beta(\tilde\xi) = \xi$, applying $\beta$ gives $\nabla_X(f\xi) = f\nabla_X\xi + (X\cdot f)\xi$ as claimed.
For $C^\infty$-linearity in $X$, the dual identity
\begin{align*}
[gX, \tilde\xi] = g[X, \tilde\xi] - (\tilde\xi \cdot g)X
\end{align*}
would normally produce a non-tensorial derivation term $-(\tilde\xi \cdot g)X$, which would break linearity. It doesn't here because $X \in \Gamma(E)$ and $\beta$ kills $E$: $\beta(X) = 0$. The Lagrangian hypothesis thus does double duty — it makes lifts irrelevant *and* makes $X$-linearity hold.
[/guided]
[/step]
[step:Compute curvature via Jacobi identity]
Recall that for a connection $\nabla$ on a bundle, the [curvature tensor](/page/Curvature) is
\begin{align*}
F(X, Y)\xi := \nabla_X \nabla_Y \xi - \nabla_Y \nabla_X \xi - \nabla_{[X,Y]}\xi, \qquad X, Y \in \Gamma(E|_L),\ \xi \in \Omega^0(E^*|_L).
\end{align*}
Pick any lift $\tilde\xi$ of $\xi$. Since $\beta([Y, \tilde\xi])$ is the expression $\nabla_Y \xi$, and since any lift of $\nabla_Y \xi$ may be used to compute $\nabla_X \nabla_Y \xi$, we choose the lift $[Y, \tilde\xi] \in \Gamma(TM|_L)$ (which satisfies $\beta([Y, \tilde\xi]) = \nabla_Y \xi$ by definition). Therefore
\begin{align*}
\nabla_X \nabla_Y \xi = \beta\bigl([X, [Y, \tilde\xi]]\bigr).
\end{align*}
Similarly $\nabla_Y \nabla_X \xi = \beta([Y, [X, \tilde\xi]])$ and $\nabla_{[X,Y]}\xi = \beta([[X,Y], \tilde\xi])$. Summing with signs,
\begin{align*}
F(X,Y)\xi &= \beta\bigl([X,[Y,\tilde\xi]] - [Y,[X,\tilde\xi]] - [[X,Y],\tilde\xi]\bigr) \\
&= \beta\bigl([X,[Y,\tilde\xi]] + [Y,[\tilde\xi,X]] + [\tilde\xi,[X,Y]]\bigr),
\end{align*}
where we used anti-symmetry $[A,B] = -[B,A]$ to rewrite the last two terms. The expression inside $\beta$ is exactly the [Jacobi identity](/page/Jacobi%20Identity) sum for the Lie bracket of vector fields, which vanishes identically. Hence $F(X,Y)\xi = \beta(0) = 0$, so the curvature vanishes.
[guided]
We want to show the curvature two-form $F(X,Y)$ vanishes. The definition involves three pieces: $\nabla_X \nabla_Y \xi$, $\nabla_Y \nabla_X \xi$, and $\nabla_{[X,Y]}\xi$. Each of these is of the form $\beta$ of some iterated Lie bracket.
The trick is to choose lifts consistently so that all three terms can be rewritten as $\beta$ applied to iterated brackets of a single lift $\tilde\xi$ of $\xi$. To compute $\nabla_X(\nabla_Y \xi)$, we need a lift of $\nabla_Y \xi \in \Omega^0(E^*)$ — but the lift is arbitrary, and the natural choice is $[Y, \tilde\xi]$, which is a vector field on $L$ (not just on the leaf; we may take an extension) mapping to $\beta([Y, \tilde\xi]) = \nabla_Y \xi$ under $\beta$. So $\nabla_X\nabla_Y \xi = \beta([X, [Y, \tilde\xi]])$, and similarly for the other two terms.
Combining with signs and using anti-symmetry of the bracket,
\begin{align*}
F(X,Y)\xi = \beta\bigl([X,[Y,\tilde\xi]] + [Y,[\tilde\xi,X]] + [\tilde\xi,[X,Y]]\bigr).
\end{align*}
The expression in parentheses is precisely the LHS of the [Jacobi identity](/page/Jacobi%20Identity) for the Lie bracket of vector fields, which is identically zero. Hence $F(X,Y)\xi = \beta(0) = 0$ for every $X, Y, \xi$, i.e.\ the curvature vanishes identically on each leaf.
[/guided]
[/step]
[step:Compute torsion using Cartan's formula and Lagrangianness]
On a leaf $L$ we have $TL = E|_L$, so the torsion of $\nabla$ as a connection on $TL$ is
\begin{align*}
\tau(X, Y) := \nabla_X Y - \nabla_Y X - [X, Y], \qquad X, Y \in \Gamma(E|_L),
\end{align*}
viewed in $\Gamma(E|_L)$ via the identification of $E^*$ with $E$ given by $\beta$ (since $E$ is Lagrangian, $\beta|_E$ pulls back to an isomorphism $E^* \cong E$ once one fixes a representative; equivalently the torsion is tested by pairing with an arbitrary $\xi \in \Omega^0(E^*)$).
Pair with $\xi \in \Omega^0(E^*)$, using the Leibniz rule $X\cdot \xi(Y) = (\nabla_X \xi)(Y) + \xi(\nabla_X Y)$ and its $X \leftrightarrow Y$ swap:
\begin{align*}
\xi(\nabla_X Y - \nabla_Y X) &= X\cdot \xi(Y) - Y\cdot \xi(X) - (\nabla_X \xi)(Y) + (\nabla_Y \xi)(X).
\end{align*}
Next, evaluate $(\nabla_X \xi)(Y) - (\nabla_Y \xi)(X)$ using the defining formula $\nabla_X \xi = \beta([X, \tilde\xi])$ and the definition of $\beta$:
\begin{align*}
(\nabla_X \xi)(Y) = \omega([X, \tilde\xi], Y), \qquad (\nabla_Y \xi)(X) = \omega([Y, \tilde\xi], X).
\end{align*}
Hence
\begin{align*}
\xi(\nabla_X Y - \nabla_Y X) = X\cdot \xi(Y) - Y\cdot \xi(X) - \omega([X,\tilde\xi], Y) + \omega([Y,\tilde\xi], X).
\end{align*}
We now compute $(\mathcal L_{\tilde\xi} \omega)(X, Y)$ two ways. By [Cartan's magic formula](/theorems/???) and $d\omega = 0$,
\begin{align*}
\mathcal L_{\tilde\xi}\omega = \iota_{\tilde\xi}(d\omega) + d(\iota_{\tilde\xi}\omega) = d(\iota_{\tilde\xi}\omega).
\end{align*}
Since $\iota_{\tilde\xi}\omega = \omega(\tilde\xi, \cdot) = \alpha(\tilde\xi)$, which restricts on $E$ to $\beta(\tilde\xi) = \xi$, we have $\iota_{\tilde\xi}\omega|_E = \xi$ as one-forms on $L$, so
\begin{align*}
(\mathcal L_{\tilde\xi}\omega)(X, Y) = d\xi(X, Y) = X\cdot \xi(Y) - Y\cdot \xi(X) - \xi([X,Y]) \qquad (X, Y \in \Gamma(E|_L)).
\end{align*}
On the other hand, by the Leibniz rule for the Lie derivative acting on the $2$-form $\omega$,
\begin{align*}
(\mathcal L_{\tilde\xi}\omega)(X, Y) = \tilde\xi \cdot \omega(X, Y) - \omega([\tilde\xi, X], Y) - \omega(X, [\tilde\xi, Y]).
\end{align*}
Since $X, Y \in \Gamma(E|_L)$ and $E$ is Lagrangian, $\omega(X, Y) = 0$, so $\tilde\xi\cdot \omega(X,Y) = 0$. Using $[\tilde\xi, X] = -[X, \tilde\xi]$,
\begin{align*}
(\mathcal L_{\tilde\xi}\omega)(X, Y) = \omega([X, \tilde\xi], Y) - \omega(X, [\tilde\xi, Y]) = \omega([X, \tilde\xi], Y) + \omega([Y, \tilde\xi], X)\cdot(-1),
\end{align*}
where we used $\omega(X, [\tilde\xi, Y]) = -\omega([\tilde\xi, Y], X) = \omega([Y, \tilde\xi], X)$ by anti-symmetry of $\omega$ and anti-symmetry of $[\cdot,\cdot]$. Simplifying:
\begin{align*}
(\mathcal L_{\tilde\xi}\omega)(X, Y) = \omega([X, \tilde\xi], Y) - \omega([Y, \tilde\xi], X).
\end{align*}
Equating the two expressions for $(\mathcal L_{\tilde\xi}\omega)(X, Y)$ and substituting back,
\begin{align*}
\omega([X,\tilde\xi], Y) - \omega([Y,\tilde\xi], X) = X\cdot \xi(Y) - Y\cdot \xi(X) - \xi([X,Y]).
\end{align*}
Plugging this into the earlier formula for $\xi(\nabla_X Y - \nabla_Y X)$:
\begin{align*}
\xi(\nabla_X Y - \nabla_Y X) &= X\cdot \xi(Y) - Y\cdot \xi(X) - \bigl(X\cdot \xi(Y) - Y\cdot \xi(X) - \xi([X,Y])\bigr) \\
&= \xi([X,Y]).
\end{align*}
Therefore $\xi(\tau(X,Y)) = \xi(\nabla_X Y - \nabla_Y X - [X,Y]) = 0$ for every $\xi \in \Omega^0(E^*)$. Since $E^*$ separates points of $E$, $\tau(X, Y) = 0$.
[guided]
The torsion computation is the technical heart of the proof and deploys three ingredients in tandem:
1. The Leibniz rule for $\nabla$ (established earlier).
2. Lagrangianness: $\omega(X, Y) = 0$ for $X, Y \in \Gamma(E)$.
3. Closedness: $d\omega = 0$, which trivialises $\mathcal L_{\tilde\xi}\omega$ via Cartan's magic formula to $d(\iota_{\tilde\xi}\omega)$, and $\iota_{\tilde\xi}\omega$ is precisely $\alpha(\tilde\xi)$, restricting to $\xi$ on $E$.
The strategy is to test $\tau(X,Y)$ by pairing with an arbitrary $\xi \in \Omega^0(E^*)$ and express everything in terms of brackets. The Leibniz rule turns $\xi(\nabla_X Y)$ into $X\cdot \xi(Y) - (\nabla_X \xi)(Y)$, and the same for $X\leftrightarrow Y$, leaving two unknowns: $X\cdot \xi(Y) - Y\cdot \xi(X)$ and $(\nabla_X\xi)(Y) - (\nabla_Y\xi)(X)$.
The second combination we unwind via the definition $\nabla_X \xi = \beta([X, \tilde\xi]) = \omega([X,\tilde\xi], \cdot)|_E$. So it becomes $\omega([X,\tilde\xi], Y) - \omega([Y,\tilde\xi], X)$. This is tantalisingly close to $\mathcal L_{\tilde\xi}\omega$ evaluated on $(X, Y)$.
Computing $\mathcal L_{\tilde\xi}\omega$ two ways is the punch line:
- By Cartan, $\mathcal L_{\tilde\xi}\omega = d(\iota_{\tilde\xi}\omega)$ since $d\omega = 0$, and $\iota_{\tilde\xi}\omega|_E = \xi$, so evaluating on $(X,Y) \in \Gamma(E)^2$ gives $d\xi(X,Y) = X\cdot\xi(Y) - Y\cdot\xi(X) - \xi([X,Y])$.
- By the Leibniz rule for $\mathcal L$ on $\omega$, $(\mathcal L_{\tilde\xi}\omega)(X,Y) = \tilde\xi\cdot\omega(X,Y) - \omega([\tilde\xi,X],Y) - \omega(X,[\tilde\xi,Y])$. The first term dies by Lagrangianness.
Equating the two yields the crucial identity
\begin{align*}
\omega([X,\tilde\xi], Y) - \omega([Y,\tilde\xi], X) = X\cdot \xi(Y) - Y\cdot \xi(X) - \xi([X,Y]).
\end{align*}
Plugging back, the $X\cdot \xi(Y) - Y\cdot \xi(X)$ pieces cancel and we are left with exactly $\xi([X,Y])$, giving $\xi(\nabla_X Y - \nabla_Y X) = \xi([X,Y])$, i.e.\ $\xi(\tau(X,Y)) = 0$. Arbitrariness of $\xi$ finishes the argument.
[/guided]
[/step]
[step:Assemble the result]
The operator $d_{E^*}$ is the first-order differential operator $\xi \mapsto (X \mapsto \nabla_X \xi)$ for $X \in \Gamma(E)$, valued in $\Omega^0(E^* \otimes E^*)$; by the $C^\infty$-linearity in $X$ and the Leibniz rule in $\xi$ established above, it is a bona fide affine connection on each leaf $L$ of the foliation integrating $E$. The previous two steps establish that its curvature $F \equiv 0$ and its torsion $\tau \equiv 0$. This completes the proof.
[/step]
