metric_compatibility
plain-language theorem explainer
The theorem asserts that the covariant derivative of the metric tensor vanishes identically under the placeholder definitions. Developers extending the Recognition Science relativity scaffolding toward a Levi-Civita connection would cite it when assembling connection properties. The proof reduces directly to unfolding covariant_deriv_bilinear (defined to return zero) followed by reflexivity.
Claim. For a metric tensor $g$, the covariant derivative satisfies $∇_ρ g_{μν}(x) = 0$ for all indices, where the bilinear covariant derivative is the zero map.
background
This module supplies placeholder Christoffel symbols and covariant derivatives that default to zero. The MetricTensor structure (from Relativity.Geometry.Metric) carries a bilinear form $g$ together with a symmetry condition on its components. The covariant_deriv_bilinear definition (line 50) is noncomputable and returns the constant zero function for any metric, bilinear form, and index.
proof idea
Term-mode proof: introduce the four indices, unfold covariant_deriv_bilinear, then apply rfl to match the zero value.
why it matters
Supplies the metric-compatibility clause required by the downstream Gravity.Connection.metric_compatibility definition, which states that the Levi-Civita connection is the unique torsion-free, metric-compatible connection. It occupies a placeholder slot in the relativity geometry layer; the module documentation explicitly marks the file as outside the verified certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.