riemann_trace_vanishes_of_smooth
plain-language theorem explainer
The Riemann curvature trace over the first two indices vanishes for metrics whose components admit symmetric mixed partial derivatives. Differential geometers simplifying contracted curvature identities in the Einstein equations would cite this identity. The proof splits the trace into linear Christoffel derivative terms that cancel by the supplied partial-symmetry hypothesis and quadratic terms that vanish by a prior lemma, then closes both sums with linarith.
Claim. Let $g$ be a metric tensor on four-dimensional space. For indices $μ,ν$, if the metric satisfies symmetric mixed partials and the summed partial derivatives of the Christoffel symbols obey $∑_ρ ∂_μ Γ^ρ_{νρ} = ∑_ρ ∂_ν Γ^ρ_{μρ}$, then the Riemann trace vanishes: $∑_ρ R^ρ_{ρμν} = 0$.
background
MetricSmooth encodes the condition that every pair of mixed partial derivatives of the metric components commute. The module establishes algebraic symmetries of the Riemann tensor once it is expressed through Christoffel symbols of a MetricTensor. Upstream results supply the Christoffel definition, the partial-derivative placeholder, and the quadratic-vanishing lemma used in the trace calculation.
proof idea
The tactic proof first unfolds the trace and tensor definitions, then applies christoffel_quadratic_trace_vanishes to kill the quadratic Christoffel products. It reassociates the remaining expression with ring, splits the derivative sum via sum_sub_distrib, invokes the supplied hypothesis to obtain zero by linarith, and finally combines the two zero sums again with linarith.
why it matters
The result supplies the trace-vanishing step required by downstream curvature identities such as riemann_antisymmetric_last_two. It closes the compatibility layer between the explicit Christoffel definition and the Riemann symmetries listed in the module, supporting the pair-exchange and Ricci-symmetry theorems that feed the Einstein tensor construction in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.