riemann_trace_antisym
plain-language theorem explainer
The trace of the Riemann tensor over its first pair of indices is antisymmetric under swap of the final pair, so the contraction equals its own negative. Workers on curvature identities in general relativity cite this when simplifying Ricci contractions or Bianchi-derived relations. The proof is a term reduction that unfolds the trace sum and applies the component antisymmetry lemma at equal first indices.
Claim. $R^ρ_{ρμν} summed over ρ equals the negative of the same sum with μ and ν exchanged, for the Riemann tensor built from metric g at coordinate point x.
background
The module derives the standard algebraic symmetries of the Riemann curvature tensor from its Christoffel-symbol definition in four-dimensional spacetime. MetricTensor supplies the local non-sealed bilinear form used to lower indices and define the curvature. The key upstream fact is the antisymmetry of the Riemann tensor in its last two indices, stated as riemann_antisymmetric_last_two.
proof idea
Term-mode proof: unfold the trace definition, rewrite the sum via negation distribution over Finset, apply sum congruence, then reduce each summand by direct appeal to riemann_antisymmetric_last_two evaluated at equal first indices ρ ρ.
why it matters
The lemma supplies one of the elementary antisymmetries listed among the module's main results and is a prerequisite for the Ricci-tensor symmetry theorem in the same file. It reproduces the standard identity used in Wald Chapter 3 and MTW Chapter 13, closing a basic step in the Recognition Science treatment of curvature within the relativity domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.