IsMetricCompatible
A connection on 4D spacetime is metric-compatible with a metric tensor when its covariant derivative annihilates every component of the metric. Workers on the fundamental theorem of pseudo-Riemannian geometry cite the definition to isolate the metric-compatibility half of the Levi-Civita statement. The declaration is a direct abbreviation that equates the condition to the vanishing of the pre-defined cov_deriv_metric operator.
claimA connection coefficients object $Γ$ is metric-compatible with metric tensor $g$ precisely when the covariant derivative satisfies $∇_ρ g_{μν}(x) = 0$ for every spacetime point $x$ and all indices $ρ, μ, ν$.
background
ConnectionCoeffs is the type of connection coefficients on 4D spacetime, mapping a point together with three indices to a real number and thereby encoding $Γ^ρ_{μν}$. MetricTensor supplies the local bilinear form $g$ used throughout the module. The operator cov_deriv_metric assembles the standard expression for the covariant derivative of the metric from partial derivatives of $g$ and contractions against the connection symbols.
proof idea
This declaration is the definition itself. It directly encodes the condition that the covariant derivative of the metric vanishes identically, using the already-defined cov_deriv_metric operator on the connection and metric.
why it matters in Recognition Science
The definition is invoked by the downstream theorem levi_civita_metric_compatible, which establishes that the Christoffel connection satisfies the condition once the Koszul identity is assumed. It supplies one of the three pillars of the Fundamental Theorem of Pseudo-Riemannian Geometry recorded in the module documentation, alongside torsion-freeness and uniqueness. In the Recognition Science setting the definition anchors the relativistic geometry layer that follows from the phi-ladder and the eight-tick octave.
scope and limits
- Does not prove that the Christoffel symbols satisfy the condition.
- Does not incorporate torsion-freeness into the stated property.
- Does not address existence or uniqueness of the connection.
- Does not fix the metric signature or spacetime dimension.
Lean usage
example (g : MetricTensor) (h : ∀ x, KoszulIdentity g x) : IsMetricCompatible (christoffel g) g := levi_civita_metric_compatible g hformal statement (Lean)
56def IsMetricCompatible (Γ : ConnectionCoeffs) (g : MetricTensor) : Prop :=
proof body
Definition body.
57 ∀ x ρ μ ν, cov_deriv_metric Γ g x ρ μ ν = 0
58
59/-! ## §2 Christoffel Symbols Are Torsion-Free -/
60
61/-- `Curvature.christoffel` is torsion-free.
62 This is already proved as `christoffel_symmetric`. -/