ricci_tensor_symmetric_thm
plain-language theorem explainer
Ricci symmetry follows once the Riemann trace vanishes. Workers in general relativity invoke this when simplifying the Einstein equations or verifying curvature properties in four-dimensional spacetime. The argument reduces the difference of Ricci components to the trace via an auxiliary lemma then applies linear arithmetic after the trace is shown to vanish.
Claim. For a metric tensor $g$ and point $x$ in four-dimensional space, if the Riemann trace vanishes at indices $μ,ν$ then the Ricci tensor satisfies $R_{μν}(g,x) = R_{νμ}(g,x)$.
background
The RiemannSymmetries module derives standard curvature identities from the Christoffel-symbol definition of the Riemann tensor on a four-dimensional manifold. The MetricTensor structure supplies the local bilinear metric form. The Ricci tensor arises by contracting one index pair of the Riemann tensor. Upstream lemmas establish that the antisymmetric part of the Ricci tensor equals the Riemann trace and that this trace vanishes for the torsion-free Levi-Civita connection, matching the reference in Wald Section 3.2.
proof idea
The proof applies the lemma ricci_minus_transpose_eq_trace to equate the difference of Ricci components with the trace. It then invokes riemann_trace_vanishes under the supplied hypothesis to set the trace to zero. Linear arithmetic finishes the equality.
why it matters
This result completes the symmetry list in the module (antisymmetry in pairs, first Bianchi identity, pair exchange) and is used by the curvature module's antisymmetry theorem together with the wrapper ricci_tensor_symmetric_proof. It supplies the standard GR property needed for Einstein-equation simplifications and aligns with the Recognition Science derivation of spacetime geometry from the forcing chain. The proof is closed with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.