KoszulIdentity
plain-language theorem explainer
The Koszul identity equates the metric-contracted Christoffel symbols to the partial derivative of the metric components. Researchers proving the fundamental theorem of pseudo-Riemannian geometry cite it to establish metric compatibility of the Levi-Civita connection. The declaration directly encodes this algebraic relation as a proposition obtained by expanding the Christoffel formula and contracting indices.
Claim. For a metric tensor $g$ at a spacetime point $x$, the identity asserts that for all indices $ρ, μ, ν$, $∑_σ Γ^σ_{ρμ} g_{σν} + ∑_σ Γ^σ_{ρν} g_{μσ} = ∂_ρ g_{μν}$, where $Γ$ denotes the Christoffel symbols of $g$.
background
The module establishes the Fundamental Theorem of Pseudo-Riemannian Geometry: on any pseudo-Riemannian manifold there exists a unique torsion-free, metric-compatible connection whose coefficients are the Christoffel symbols. A MetricTensor supplies the local bilinear form $g$ on four-dimensional coordinates. The partial derivative operator acts as a placeholder for coordinate differentiation of metric components. Upstream, the Christoffel definition expands the standard formula involving first derivatives of $g$, while the metric structure enforces symmetry.
proof idea
As a definition the body directly states the forall equality. The summed contractions of Christoffel symbols with metric components are set equal to the coordinate derivative of the metric, matching the algebraic expansion described in the declaration comment.
why it matters
This definition supplies the hypothesis required by metric_compatible_of_koszul and levi_civita_metric_compatible, which together establish that the Christoffel connection satisfies ∇g = 0. It therefore completes the metric-compatibility leg of FundamentalTheoremExistence, realizing the existence half of the Fundamental Theorem of Pseudo-Riemannian Geometry (Wald, Theorem 3.1.1). In the Recognition framework it anchors the geometric structures used by the relativity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.