2 Curvature
For a covariant derivative \(\nabla \) on the tangent bundle of \(M\),
\(R(X,Y)Z = -R(Y,X)Z\).
Immediate from \([Y,X] = -[X,Y]\) and linearity of \(\nabla _{(-)} Z\) in the direction slot.
For a torsion-free connection, \(R(X,Y)Z + R(Y,Z)X + R(Z,X)Y = 0\).
Proved, for a \(C^1\) connection and \(C^2\) vector fields, with every differentiability side condition discharged.
Regroup the cyclic sum using torsion-freeness on each pair,
apply torsion-freeness once more to each difference to obtain \([X,[Y,Z]] + [Y,[Z,X]] + [Z,[X,Y]]\), and close with Jacobi (VectorField.leibniz_identity_mlieBracket_apply).
Both ingredients are in Mathlib as of August 2026. The \(C^2\) hypotheses are essential rather than cosmetic: torsion_eq_zero_iff gives \(\nabla _X Y - \nabla _Y X = [X,Y]\) only for MDiffAt fields, and the second application is to the pair \((X, [Y,Z])\), so the bracket itself must be differentiable.
(An earlier version of this blueprint claimed the identity was blocked on \(Z\)-slot tensoriality and mkHom\(_3\). Those are prerequisites for packaging curvature as a tensor, not for the operator identity stated here.)
For a torsion-free connection, \((\nabla _X R)(Y,Z)W + (\nabla _Y R)(Z,X)W + (\nabla _Z R)(X,Y)W = 0\), where \((\nabla _X R)(Y,Z)W = \nabla _X(R(Y,Z)W) - R(\nabla _X Y, Z)W - R(Y, \nabla _X Z)W - R(Y,Z)\nabla _X W\) (CovariantDerivative.covCurvature).
Proved, for a \(C^2\) connection, \(C^2\) fields \(X, Y, Z\) and a \(C^3\) field \(W\), with every differentiability side condition discharged. No metric is involved.
Expand everything in iterated covariant derivatives of \(W\). The twelve third-order terms \(\nabla \nabla \nabla W\) cancel in pairs, as do the six terms \(\nabla _X \nabla _{[Y,Z]} W\) and \(\nabla _{[Y,Z]} \nabla _X W\) once torsion-freeness has turned \(\nabla _{\nabla _X Y} - \nabla _{\nabla _Y X}\) into \(\nabla _{[X,Y]}\) in the direction slot and \(\nabla _Z \nabla _{\nabla _X Y} W - \nabla _Z \nabla _{\nabla _Y X} W\) into \(\nabla _Z \nabla _{[X,Y]} W\) as sections. What survives is \(\nabla _W\) applied to \([[X,Y],Z] + [[Y,Z],X] + [[Z,X],Y]\), which is Jacobi.
The regularity is what makes the sections differentiable: a \(C^2\) connection sends the \(C^3\) section \(W\) to a \(C^2\) section \(\nabla _Z W\) (contMDiff_cov_apply), so \(\nabla _Y \nabla _Z W\) is differentiable and \(\nabla _X\) of it is meaningful. As for the first identity, brackets of \(C^2\) fields are differentiable, which the second application of torsion-freeness needs.
\([V,W]f = V(Wf) - W(Vf)\), for \(f\) of class \(C^2\) at the point and \(V,W\) differentiable there, on any manifold — boundary and corners allowed.
Absent from Mathlib in both the vector-space and the manifold setting. Over a vector space the two second-derivative terms cancel by symmetry of the second derivative, leaving exactly the bracket. Transporting to a manifold turns on one observation: \(\mathrm{d}f\) at a nearby point \(y\) is defined through the chart at \(y\), so one first re-expresses it through the single chart at \(x\), uniformly over that chart’s source. The outer derivative is then an ordinary fderivWithin and the vector-space identity transports verbatim, with \(\mathrm{range}\, I\) supplying the side conditions the Within calculus needs. No manifold-level second-derivative symmetry is required.
\(R\) is \(C^\infty (M)\)-linear in each slot.
First slot: expanding \(\nabla _{fX}Z = f\, \nabla _X Z\) leaves a \((Yf)\, \nabla _X Z\) term from Leibniz, and \([fX,Y] = f[X,Y] - (Yf)X\) leaves a matching one from the bracket, with opposite sign; they cancel. The second slot follows by antisymmetry. The third leaves a residue \([\, X(Yf) - Y(Xf) - [X,Y]f\, ]\, Z\), which vanishes by Lemma 5.