einstein_symmetric
plain-language theorem explainer
The Einstein tensor inherits symmetry from the Ricci tensor under the assumption of a torsion-free connection. Researchers deriving the Einstein field equations from the Einstein-Hilbert action cite this identity. The proof is a direct algebraic reduction that unfolds the Einstein tensor definition and applies the supplied Ricci symmetry together with metric symmetry.
Claim. If the Ricci tensor satisfies $R_{mu nu}=R_{nu mu}$, then the Einstein tensor $G_{mu nu}=R_{mu nu}-(1/2)Rg_{mu nu}$ (with scalar curvature $R=g^{alpha beta}R_{alpha beta}$) satisfies $G_{mu nu}=G_{nu mu}$.
background
The RicciTensor module constructs the Einstein tensor from the Ricci tensor and metric via $G_{mu nu}=R_{mu nu}-(1/2) R g_{mu nu}$. MetricTensor is a symmetric bilinear form on Idx=Fin 4; InverseMetric supplies its inverse. The hypothesis h_ricci_sym encodes Ricci symmetry, which the declaration comment states holds for torsion-free connections. The module proves the structural identities required for coordinate expressions of the Einstein field equations.
proof idea
One-line term-mode wrapper. It applies simp to unfold einstein_tensor, then rewrites using the Ricci symmetry hypothesis and the metric symmetry property.
why it matters
This result is invoked inside HilbertVariationCert (EinsteinHilbertAction module) to certify that the variation of the Einstein-Hilbert action produces the Einstein tensor. It supplies one of the symmetry identities needed to equate the action principle with the vacuum field equations. The declaration comment ties the symmetry to torsion-free connections, closing a prerequisite for the structural form of the Einstein equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.