riemann_trace
plain-language theorem explainer
The riemann_trace definition computes the contraction Σ_ρ R^ρ_ρμν of the Riemann curvature tensor. Researchers deriving Ricci symmetry or contracted Bianchi identities in general relativity cite this contraction when relating curvature traces to metric compatibility. It is realized as a direct finite sum over the index ρ that reindexes the riemann_tensor call.
Claim. The contraction $R^ρ_{ρμν} := ∑_ρ R^ρ_{ρμν}$ of the Riemann tensor $R^ρ_{σμν}$ built from the metric tensor $g$ at coordinate point $x ∈ ℝ^4$.
background
The RiemannSymmetries module derives the standard algebraic identities of the Riemann tensor from its expression in Christoffel symbols of a torsion-free, metric-compatible connection. The MetricTensor structure supplies the local bilinear form g(x)(a,b) on Fin 4 indices. The riemann_tensor function (imported from Curvature) returns the (1,3) tensor components at each point x.
proof idea
One-line definition that applies Finset.univ.sum to riemann_tensor after constructing the index tuple (ρ, μ, ν) via the supplied lambda maps. No tactics or lemmas are invoked inside the body.
why it matters
The contraction feeds directly into ricci_minus_transpose_eq_trace, which equates the antisymmetric part of the Ricci tensor to the trace, and into riemann_trace_vanishes, which asserts vanishing for the Levi-Civita connection. It thereby closes the algebraic step from the first Bianchi identity to Ricci symmetry, consistent with the module's references to Wald Chapter 3 and MTW Chapter 13. In the broader Recognition framework the same contraction supports curvature definitions built on the phi-ladder and ledger factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.