metric_compatible_of_koszul
plain-language theorem explainer
The Koszul identity for a metric tensor g at point x implies that the covariant derivative of g vanishes in every component under the Christoffel connection. Relativists cite this step when verifying metric compatibility of the Levi-Civita connection on a 4-dimensional pseudo-Riemannian manifold. The proof is a direct reduction: it unfolds the covariant derivative, instantiates the Koszul identity, and concludes zero by linear arithmetic.
Claim. If the Koszul identity holds for metric tensor $g$ at point $x$, that is $g_{σν}Γ^σ_{ρμ} + g_{μσ}Γ^σ_{ρν} = ∂_ρ g_{μν}$, then the covariant derivative of the metric with respect to the Christoffel connection satisfies $∇_ρ g_{μν} = 0$ for all indices $ρ, μ, ν$.
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 a local bilinear form on Fin 4 → ℝ. The KoszulIdentity is the algebraic relation that encodes metric compatibility: the contraction of the Christoffel symbols with the metric equals the partial derivative of the metric components. This theorem operates inside the standard 4-dimensional setting with either positive-definite or Lorentzian signature, referencing Wald Theorem 3.1.1 and do Carmo Theorem 2.3.
proof idea
The term proof introduces the three indices, unfolds cov_deriv_metric to expose the combination of Christoffel symbols and metric derivatives, obtains the corresponding instance of the Koszul identity, and applies linarith to reach zero.
why it matters
The declaration is invoked inside fundamental_theorem_existence to populate the metric_compatible field and inside levi_civita_metric_compatible to establish IsMetricCompatible. It supplies the metric-compatibility half of the Fundamental Theorem of Pseudo-Riemannian Geometry, completing the existence and uniqueness of the Levi-Civita connection. Within Recognition Science it anchors the geometric layer that supports the forcing chain from T0 to T8 and the derivation of constants from the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.