ricci_tensor_symmetric_proof
plain-language theorem explainer
The Ricci tensor is symmetric in its indices for any four-dimensional metric whose Riemann tensor satisfies the trace-vanishing condition. General-relativity calculations and curvature axiom verifications cite the result to guarantee that the Einstein tensor is well-defined and symmetric. The proof is a one-line functional abstraction that supplies the trace hypothesis to the core symmetry theorem.
Claim. Let $g$ be a metric tensor on four-dimensional spacetime and let $x$ be a point. Assume the Riemann tensor trace vanishes for every index pair. Then the Ricci tensor satisfies $R_{ab}(g,x)=R_{ba}(g,x)$ for all indices $a,b$.
background
The module establishes the algebraic symmetries of the Riemann curvature tensor once it is expressed through Christoffel symbols. MetricTensor supplies the local non-sealed bilinear form $g:(Fin 4→ℝ)→(Fin 4→ℝ)→(Fin 2→Fin 4)→ℝ$. The Ricci tensor itself is defined in the Gravity.RicciTensor module; the present declaration merely discharges the symmetry interface that the original axiom expected. Mixed partial symmetry of scalar functions (Schwarz theorem) is treated as an external hypothesis and is used to close both the explicit Riemann expression and the trace-vanishing condition.
proof idea
The term proof is a one-line wrapper: it abstracts over the two free indices and directly invokes the core symmetry theorem, passing the supplied trace-vanishing hypothesis instance for those indices. No additional rewriting or case analysis is required.
why it matters
The result supplies the Ricci symmetry required by the Einstein-tensor definition and by the curvature-axioms theorem that closes the module. It completes the list of standard Riemann symmetries (antisymmetry in each pair, first Bianchi identity, pair exchange) that the module derives from the Christoffel definition, matching the classical statements in Wald Chapter 3 and MTW Chapter 13. Within the Recognition framework the symmetry is needed before the Einstein tensor can be formed and before the eight-tick octave and three-dimensional spatial reduction can be applied to the curvature sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.