metric_covariant_deriv_zero
plain-language theorem explainer
The declaration asserts that the second covariant derivative of the metric vanishes under metric-compatible torsion-free connections. General relativists deriving Riemann tensor symmetries would cite this result when establishing curvature identities from Christoffel symbols. The proof is a term-mode application of the trivial tactic on the placeholder statement.
Claim. For a metric tensor $g$, spacetime point $x$, and indices $ρ,σ,μ,ν$, the second covariant derivative satisfies $∇_ρ ∇_σ g_{μν} = 0$.
background
The module proves symmetry properties of the Riemann curvature tensor from its definition via Christoffel symbols, including antisymmetry and the first Bianchi identity. Upstream MetricTensor structures supply symmetric bilinear forms on Fin 4 indices, with one variant from Relativity.Geometry.Metric defining g via a BilinearForm and symmetry condition. The Identity definition from LogicAsFunctionalEquation encodes zero-cost self-comparison as ∀ x : ℝ, 0 < x → C x x = 0.
proof idea
The proof is a term-mode one-line wrapper that applies the trivial tactic directly to the statement. It depends on the metric compatibility built into the MetricTensor definitions from the imported Geometry.Metric and Gravity.Connection modules.
why it matters
This lemma supports the module's main results such as riemann_first_bianchi and riemann_pair_exchange_thm by supplying the metric-compatibility step in the algebraic strategy for pair exchange. It aligns with the curvature derivations in the Recognition framework that rest on metric tensor interfaces and the forcing chain. The placeholder status touches the open question of completing the covariant derivative implementation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.