metric_compatibility
Metric compatibility encodes the condition that the covariant derivative of the metric tensor vanishes identically. Researchers formalizing Levi-Civita connections in coordinate patches within the Recognition Science gravity sector cite this definition when linking torsion-free symmetry to geodesic preservation. The implementation is a direct equational definition that subtracts the two index contractions with Christoffel symbols from the supplied partial-derivative function and requires the difference to be zero for every triple of indices.
claimFor a metric tensor with components $g$ and Christoffel symbols with components $Gamma$, the condition $partial_lambda g_{mu nu} - Gamma^rho_{lambda mu} g_{rho nu} - Gamma^rho_{lambda nu} g_{mu rho} = 0$ holds for all indices $lambda, mu, nu$ in the four-dimensional index set.
background
The Gravity.Connection module works in local coordinate patches on a four-dimensional spacetime, with indices drawn from the abbreviation Idx := Fin 4. MetricTensor is the structure supplying a symmetric bilinear form g : Idx → Idx → ℝ at each point. ChristoffelData supplies the symbols gamma : Idx → Idx → Idx → ℝ, whose explicit construction from the metric and its first derivatives appears in the sibling definition christoffel_from_metric.
proof idea
This is a definition whose body is the universal quantification over lambda, mu, nu of the stated linear combination of dg and the two summed contractions with gamma. No lemmas or tactics are invoked; the expression is the primitive statement of nabla g = 0.
why it matters in Recognition Science
The definition supplies the metric-compatibility axiom required for the Levi-Civita connection, complementing the symmetry property christoffel_symmetric in the same module. It is used by the theorem metric_compatibility in Relativity.Geometry.Connection, which unfolds the covariant derivative and reduces to this condition. In the Recognition framework it anchors the gravity sector, ensuring consistency with the Hamiltonian MetricTensor interface and the eight-tick octave structure of spatial dimensions.
scope and limits
- Does not prove existence or uniqueness of a connection satisfying the condition.
- Does not extend beyond four-dimensional coordinate patches.
- Does not incorporate torsion or non-metric connections.
- Does not evaluate the condition for concrete metric functions.
formal statement (Lean)
106def metric_compatibility (met : MetricTensor) (ch : ChristoffelData)
107 (dg : Idx → Idx → Idx → ℝ) : Prop :=
proof body
Definition body.
108 ∀ lambda mu nu : Idx,
109 dg lambda mu nu -
110 ∑ rho : Idx, (ch.gamma rho lambda mu * met.g rho nu) -
111 ∑ rho : Idx, (ch.gamma rho lambda nu * met.g mu rho) = 0
112
113/-- For flat spacetime (Minkowski metric with constant components),
114 all Christoffel symbols vanish. -/