metric_compatibility
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.