ricci_minus_transpose_eq_trace
plain-language theorem explainer
The lemma equates the difference between a Ricci tensor component and its transpose to the contracted Riemann trace over the first and third indices. General relativists cite it when deriving Ricci symmetry from the first Bianchi identity. The proof unfolds the tensor definitions, rewrites the difference as a sum, applies congruence over the contraction index, substitutes the Bianchi identity at equal indices together with antisymmetry on the final pair, and closes with linear arithmetic.
Claim. Let $g$ be a metric tensor and $x$ a spacetime point. For indices $μ,ν$, the difference $R_{μν}-R_{νμ}$ equals the Riemann trace $∑_ρ R^ρ_{ρμν}$, where $R_{μν}$ is the Ricci tensor obtained by contracting the Riemann curvature tensor on its first and third indices.
background
The module establishes algebraic symmetries of the Riemann tensor defined from the Christoffel connection of a metric. MetricTensor supplies the local bilinear form $g_{αβ}(x)$. The Ricci tensor is the contraction $R_{μν}=R^ρ_{μρν}$ and the trace $riemann_trace$ is the further contraction $∑ρ R^ρ{ρμν}$. The first Bianchi identity $R^ρ_{σμν}+R^ρ_{μνσ}+R^ρ_{νσμ}=0$ and the antisymmetry $R^ρ_{μνσ}=-R^ρ_{μσν}$ are the immediate upstream lemmas.
proof idea
Unfold the definitions of ricci_tensor and riemann_trace. Simplify the index-selection functions with simp. Rewrite the left-hand side as a difference of two Finset sums. Apply sum_congr to reduce to a pointwise identity. Invoke riemann_first_bianchi at equal first indices and riemann_antisymmetric_last_two on the last pair. Conclude with linarith.
why it matters
The result supplies the algebraic identity required by ricci_tensor_symmetric_thm, which then invokes the separate vanishing of the trace to conclude $R_{μν}=R_{νμ}$. It therefore completes the standard derivation of Ricci symmetry from the first Bianchi identity, placing the Recognition Science geometry inside the classical GR framework referenced in Wald Section 3.2 and MTW Chapter 13.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.