Koszul formula

koszul_formula

Submitter: Kim Morrison.

Notes: §38 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the Riemannian-geometry section; the boxed main theorem is Levi-Civita). The Koszul formula: 2⟨∇_X Y, Z⟩ equals the cyclic sum of directional derivatives X·⟨Y,Z⟩ + Y·⟨X,Z⟩ − Z·⟨X,Y⟩ minus the Lie-bracket cyclic sum ⟨X,[Y,Z]⟩ + ⟨Y,[X,Z]⟩ − ⟨Z,[X,Y]⟩. The identity that forces uniqueness of the Levi-Civita connection. Mathlib has the covariant-derivative / Riemannian-bundle / Lie-bracket machinery but no metric-compatibility predicate and no Koszul formula. The Challenge ships one helper (IsMetricCompatible).

Source: J.-L. Koszul (course notes, 1950s); cf. do Carmo, Riemannian Geometry. Listed as §38 additional statement in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Direct algebraic manipulation from metric compatibility and torsion-freeness. Metric compatibility gives X·g(Y,Z) = g(∇_X Y, Z) + g(Y, ∇_X Z), and cyclic permutations Y·g(Z,X) and Z·g(X,Y). Torsion-freeness gives ∇_X Y − ∇_Y X = [X,Y] (and permutations). Form the linear combination X·g(Y,Z) + Y·g(X,Z) − Z·g(X,Y); expand each term via metric compatibility; substitute the torsion-free identities to convert ∇_X Z − ∇_Z X, ∇_Y Z − ∇_Z Y, and ∇_X Y − ∇_Y X into Lie brackets. The cross-terms ±g(∇_Y X, Z), ±g(∇_X Z, Y), ±g(∇_Y Z, X) collapse pairwise except for 2·g(∇_X Y, Z), yielding the formula.

theorem declaration uses `sorry`koszul_formula {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
      [FiniteDimensional ℝ E] [CompleteSpace E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
      [IsManifold I ∞ M]
    [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)]
    (cov : CovariantDerivative I E (TangentSpace I (M := M)))
    [ContMDiffCovariantDerivative cov ∞]
    (_htor : cov.torsion = 0) (_hmet : LeanEval.Geometry.KoszulFormula.IsMetricCompatible cov)
    (X Y Z : Π x : M, TangentSpace I x)
    (_hX : CMDiff ∞ (T% X)) (_hY : CMDiff ∞ (T% Y)) (_hZ : CMDiff ∞ (T% Z))
    (x : M) :
    2 * inner ℝ (cov Y x (X x)) (Z x) =
      extDerivFun (fun y : M => inner ℝ (Y y) (Z y)) x (X x)
      + extDerivFun (fun y : M => inner ℝ (X y) (Z y)) x (Y x)
      - extDerivFun (fun y : M => inner ℝ (X y) (Y y)) x (Z x)
      - inner ℝ (X x) (mlieBracket I Y Z x)
      - inner ℝ (Y x) (mlieBracket I X Z x)
      + inner ℝ (Z x) (mlieBracket I X Y x) := byE:Type u_1inst✝¹⁰:NormedAddCommGroup Einst✝⁹:NormedSpace ℝ Einst✝⁸:FiniteDimensional ℝ Einst✝⁷:CompleteSpace EH:Type u_2inst✝⁶:TopologicalSpace HI:ModelWithCorners ℝ E HM:Type u_3inst✝⁵:TopologicalSpace Minst✝⁴:ChartedSpace H Minst✝³:IsManifold I ∞ Minst✝²:RiemannianBundle fun x => TangentSpace I xinst✝¹:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I xcov:CovariantDerivative I E (TangentSpace I)inst✝:cov.ContMDiffCovariantDerivative ∞_htor:cov.torsion = 0_hmet:IsMetricCompatible covX:(x : M) → TangentSpace I xY:(x : M) → TangentSpace I xZ:(x : M) → TangentSpace I x_hX:ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ fun x => ⟨x, X x⟩_hY:ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ fun x => ⟨x, Y x⟩_hZ:ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ fun x => ⟨x, Z x⟩x:M⊢ 2 * Inner.inner ℝ ((↑cov Y x) (X x)) (Z x) =
  (extDerivFun (fun y => Inner.inner ℝ (Y y) (Z y)) x) (X x) +
            (extDerivFun (fun y => Inner.inner ℝ (X y) (Z y)) x) (Y x) -
          (extDerivFun (fun y => Inner.inner ℝ (X y) (Y y)) x) (Z x) -
        Inner.inner ℝ (X x) (mlieBracket I Y Z x) -
      Inner.inner ℝ (Y x) (mlieBracket I X Z x) +
    Inner.inner ℝ (Z x) (mlieBracket I X Y x)
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 25, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 26, 2026

• @rishistyping with Stealth Model on May 26, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 28, 2026