metric_compatibility
plain-language theorem explainer
The theorem states that the covariant derivative of the metric tensor vanishes identically in all directions and index positions. It would be cited when assembling the Levi-Civita connection inside the Recognition Science geometry layer. The proof is a one-line term wrapper that unfolds the bilinear covariant derivative definition and closes by reflexivity.
Claim. For any metric tensor $g$, the covariant derivative satisfies $nabla_rho g_{mu nu} = 0$ for all directions $rho$ and index pairs $(mu, nu)$.
background
The module supplies placeholder structures for the metric and its derivatives in the relativity geometry layer. MetricTensor is a record containing a bilinear form $g$ together with a symmetry axiom on its components. covariant_deriv_bilinear is defined to return the zero bilinear form for every input, independent of the metric or the direction index.
proof idea
The term proof introduces the four quantifiers, unfolds covariant_deriv_bilinear (which is hard-coded to the constant zero function), and applies reflexivity.
why it matters
It supplies the metric-compatibility half of the definition used by IndisputableMonolith.Gravity.Connection.metric_compatibility, which characterises the Levi-Civita connection as the unique torsion-free metric-compatible connection. The result therefore closes the placeholder step that lets the Recognition framework move from the metric to the connection, although the entire module is flagged as scaffolding outside the verified certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.