cov_deriv_metric
plain-language theorem explainer
This definition supplies the explicit formula for the covariant derivative of the metric tensor ∇_ρ g_{μν} in terms of partial derivatives and connection coefficients on 4-dimensional spacetime. General relativists cite it when verifying that the Levi-Civita connection is metric-compatible. It is realized as a direct algebraic expression that subtracts the two index contractions from the partial derivative of the metric component.
Claim. The covariant derivative of the metric is defined by $∇_ρ g_{μν}(x) = ∂_ρ g_{μν}(x) - ∑_σ Γ^σ_{ρμ}(x) g_{σν}(x) - ∑_σ Γ^σ_{ρν}(x) g_{μσ}(x)$, where Γ denotes the connection coefficients.
background
The module establishes the Fundamental Theorem of Pseudo-Riemannian Geometry on 4D spacetime: existence of a unique torsion-free metric-compatible connection whose coefficients are the Christoffel symbols. ConnectionCoeffs is the type of maps sending a point x ∈ ℝ^4 and indices ρ,μ,ν to Γ^ρ_{μν}(x). MetricTensor is the structure supplying the local bilinear form g. The partial derivative is accessed via the placeholder partialDeriv_v2. The local setting is the standard statement that any torsion-free metric-compatible connection equals the Christoffel connection, as in Wald Theorem 3.1.1.
proof idea
This is a direct definition. It evaluates the partial derivative of the μν-component of the metric with respect to coordinate ρ, then subtracts the two contractions of the connection coefficients with the metric components.
why it matters
The definition is invoked inside IsMetricCompatible to express the condition ∇g = 0 and inside FundamentalTheoremExistence to assert that the Christoffel connection satisfies metric compatibility. It thereby supplies the metric-compatibility half of the Fundamental Theorem of Pseudo-Riemannian Geometry. In the broader framework it anchors the geometric structure required for the forcing chain and the phi-ladder by guaranteeing that the connection preserves the metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.