[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$.[/step]

[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: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.[/step]

[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: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$.[/step]

[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: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]